Loogle!
Result
Found 8 declarations mentioning tsum and ENat.
- contDiff_tsum π Mathlib.Analysis.Calculus.SmoothSeries
{Ξ± : Type u_1} {π : Type u_3} {E : Type u_4} {F : Type u_5} [NontriviallyNormedField π] [IsRCLikeNormedField π] [NormedAddCommGroup E] [NormedSpace π E] [NormedAddCommGroup F] [CompleteSpace F] [NormedSpace π F] {f : Ξ± β E β F} {v : β β Ξ± β β} {N : ββ} (hf : β (i : Ξ±), ContDiff π (βN) (f i)) (hv : β (k : β), βk β€ N β Summable (v k)) (h'f : β (k : β) (i : Ξ±) (x : E), βk β€ N β βiteratedFDeriv π k (f i) xβ β€ v k i) : ContDiff π βN fun x => β' (i : Ξ±), f i x - contDiff_tsum_of_eventually π Mathlib.Analysis.Calculus.SmoothSeries
{Ξ± : Type u_1} {π : Type u_3} {E : Type u_4} {F : Type u_5} [NontriviallyNormedField π] [IsRCLikeNormedField π] [NormedAddCommGroup E] [NormedSpace π E] [NormedAddCommGroup F] [CompleteSpace F] [NormedSpace π F] {f : Ξ± β E β F} {v : β β Ξ± β β} {N : ββ} (hf : β (i : Ξ±), ContDiff π (βN) (f i)) (hv : β (k : β), βk β€ N β Summable (v k)) (h'f : β (k : β), βk β€ N β βαΆ (i : Ξ±) in Filter.cofinite, β (x : E), βiteratedFDeriv π k (f i) xβ β€ v k i) : ContDiff π βN fun x => β' (i : Ξ±), f i x - iteratedFDeriv_tsum π Mathlib.Analysis.Calculus.SmoothSeries
{Ξ± : Type u_1} {π : Type u_3} {E : Type u_4} {F : Type u_5} [NontriviallyNormedField π] [IsRCLikeNormedField π] [NormedAddCommGroup E] [NormedSpace π E] [NormedAddCommGroup F] [CompleteSpace F] [NormedSpace π F] {f : Ξ± β E β F} {v : β β Ξ± β β} {N : ββ} (hf : β (i : Ξ±), ContDiff π (βN) (f i)) (hv : β (k : β), βk β€ N β Summable (v k)) (h'f : β (k : β) (i : Ξ±) (x : E), βk β€ N β βiteratedFDeriv π k (f i) xβ β€ v k i) {k : β} (hk : βk β€ N) : (iteratedFDeriv π k fun y => β' (n : Ξ±), f n y) = fun x => β' (n : Ξ±), iteratedFDeriv π k (f n) x - iteratedFDeriv_tsum_apply π Mathlib.Analysis.Calculus.SmoothSeries
{Ξ± : Type u_1} {π : Type u_3} {E : Type u_4} {F : Type u_5} [NontriviallyNormedField π] [IsRCLikeNormedField π] [NormedAddCommGroup E] [NormedSpace π E] [NormedAddCommGroup F] [CompleteSpace F] [NormedSpace π F] {f : Ξ± β E β F} {v : β β Ξ± β β} {N : ββ} (hf : β (i : Ξ±), ContDiff π (βN) (f i)) (hv : β (k : β), βk β€ N β Summable (v k)) (h'f : β (k : β) (i : Ξ±) (x : E), βk β€ N β βiteratedFDeriv π k (f i) xβ β€ v k i) {k : β} (hk : βk β€ N) (x : E) : iteratedFDeriv π k (fun y => β' (n : Ξ±), f n y) x = β' (n : Ξ±), iteratedFDeriv π k (f n) x - ContMDiff.sum_section_of_locallyFinite π Mathlib.Geometry.Manifold.VectorBundle.SmoothSection
{π : Type u_1} [NontriviallyNormedField π] {E : Type u_2} [NormedAddCommGroup E] [NormedSpace π E] {H : Type u_3} [TopologicalSpace H] {I : ModelWithCorners π E H} {M : Type u_4} [TopologicalSpace M] [ChartedSpace H M] {F : Type u_5} [NormedAddCommGroup F] [NormedSpace π F] {n : WithTop ββ} {V : M β Type u_6} [TopologicalSpace (Bundle.TotalSpace F V)] [(x : M) β TopologicalSpace (V x)] [FiberBundle F V] [(x : M) β AddCommGroup (V x)] [(x : M) β Module π (V x)] [VectorBundle π F V] {ΞΉ : Type u_7} {t : ΞΉ β (x : M) β V x} (ht : LocallyFinite fun i => {x | t i x β 0}) (ht' : β (i : ΞΉ), ContMDiff I (I.prod (modelWithCornersSelf π F)) n fun x => Bundle.TotalSpace.mk' F x (t i x)) : ContMDiff I (I.prod (modelWithCornersSelf π F)) n fun x => Bundle.TotalSpace.mk' F x (β' (i : ΞΉ), t i x) - ContMDiffAt.sum_section_of_locallyFinite π Mathlib.Geometry.Manifold.VectorBundle.SmoothSection
{π : Type u_1} [NontriviallyNormedField π] {E : Type u_2} [NormedAddCommGroup E] [NormedSpace π E] {H : Type u_3} [TopologicalSpace H] {I : ModelWithCorners π E H} {M : Type u_4} [TopologicalSpace M] [ChartedSpace H M] {F : Type u_5} [NormedAddCommGroup F] [NormedSpace π F] {n : WithTop ββ} {V : M β Type u_6} [TopologicalSpace (Bundle.TotalSpace F V)] [(x : M) β TopologicalSpace (V x)] [FiberBundle F V] [(x : M) β AddCommGroup (V x)] [(x : M) β Module π (V x)] [VectorBundle π F V] {xβ : M} {ΞΉ : Type u_7} {t : ΞΉ β (x : M) β V x} (ht : LocallyFinite fun i => {x | t i x β 0}) (ht' : β (i : ΞΉ), ContMDiffAt I (I.prod (modelWithCornersSelf π F)) n (fun x => Bundle.TotalSpace.mk' F x (t i x)) xβ) : ContMDiffAt I (I.prod (modelWithCornersSelf π F)) n (fun x => Bundle.TotalSpace.mk' F x (β' (i : ΞΉ), t i x)) xβ - ContMDiffOn.sum_section_of_locallyFinite π Mathlib.Geometry.Manifold.VectorBundle.SmoothSection
{π : Type u_1} [NontriviallyNormedField π] {E : Type u_2} [NormedAddCommGroup E] [NormedSpace π E] {H : Type u_3} [TopologicalSpace H] {I : ModelWithCorners π E H} {M : Type u_4} [TopologicalSpace M] [ChartedSpace H M] {F : Type u_5} [NormedAddCommGroup F] [NormedSpace π F] {n : WithTop ββ} {V : M β Type u_6} [TopologicalSpace (Bundle.TotalSpace F V)] [(x : M) β TopologicalSpace (V x)] [FiberBundle F V] [(x : M) β AddCommGroup (V x)] [(x : M) β Module π (V x)] [VectorBundle π F V] {u : Set M} {ΞΉ : Type u_7} {t : ΞΉ β (x : M) β V x} (ht : LocallyFinite fun i => {x | t i x β 0}) (ht' : β (i : ΞΉ), ContMDiffOn I (I.prod (modelWithCornersSelf π F)) n (fun x => Bundle.TotalSpace.mk' F x (t i x)) u) : ContMDiffOn I (I.prod (modelWithCornersSelf π F)) n (fun x => Bundle.TotalSpace.mk' F x (β' (i : ΞΉ), t i x)) u - ContMDiffWithinAt.sum_section_of_locallyFinite π Mathlib.Geometry.Manifold.VectorBundle.SmoothSection
{π : Type u_1} [NontriviallyNormedField π] {E : Type u_2} [NormedAddCommGroup E] [NormedSpace π E] {H : Type u_3} [TopologicalSpace H] {I : ModelWithCorners π E H} {M : Type u_4} [TopologicalSpace M] [ChartedSpace H M] {F : Type u_5} [NormedAddCommGroup F] [NormedSpace π F] {n : WithTop ββ} {V : M β Type u_6} [TopologicalSpace (Bundle.TotalSpace F V)] [(x : M) β TopologicalSpace (V x)] [FiberBundle F V] [(x : M) β AddCommGroup (V x)] [(x : M) β Module π (V x)] [VectorBundle π F V] {u : Set M} {xβ : M} {ΞΉ : Type u_7} {t : ΞΉ β (x : M) β V x} (ht : LocallyFinite fun i => {x | t i x β 0}) (ht' : β (i : ΞΉ), ContMDiffWithinAt I (I.prod (modelWithCornersSelf π F)) n (fun x => Bundle.TotalSpace.mk' F x (t i x)) u xβ) : ContMDiffWithinAt I (I.prod (modelWithCornersSelf π F)) n (fun x => Bundle.TotalSpace.mk' F x (β' (i : ΞΉ), t i x)) u xβ
About
Loogle searches Lean and Mathlib definitions and theorems.
You can use Loogle from within the Lean4 VSCode language extension
using (by default) Ctrl-K Ctrl-S. You can also try the
#loogle
command from LeanSearchClient,
the CLI version, the Loogle
VS Code extension, the lean.nvim
integration or the Zulip bot.
Usage
Loogle finds definitions and lemmas in various ways:
By constant:
πReal.sin
finds all lemmas whose statement somehow mentions the sine function.By lemma name substring:
π"differ"
finds all lemmas that have"differ"
somewhere in their lemma name.By subexpression:
π_ * (_ ^ _)
finds all lemmas whose statements somewhere include a product where the second argument is raised to some power.The pattern can also be non-linear, as in
πReal.sqrt ?a * Real.sqrt ?a
If the pattern has parameters, they are matched in any order. Both of these will find
List.map
:
π(?a -> ?b) -> List ?a -> List ?b
πList ?a -> (?a -> ?b) -> List ?b
By main conclusion:
π|- tsum _ = _ * tsum _
finds all lemmas where the conclusion (the subexpression to the right of allβ
andβ
) has the given shape.As before, if the pattern has parameters, they are matched against the hypotheses of the lemma in any order; for example,
π|- _ < _ β tsum _ < tsum _
will findtsum_lt_tsum
even though the hypothesisf i < g i
is not the last.
If you pass more than one such search filter, separated by commas
Loogle will return lemmas which match all of them. The
search
π Real.sin, "two", tsum, _ * _, _ ^ _, |- _ < _ β _
would find all lemmas which mention the constants Real.sin
and tsum
, have "two"
as a substring of the
lemma name, include a product and a power somewhere in the type,
and have a hypothesis of the form _ < _
(if
there were any such lemmas). Metavariables (?a
) are
assigned independently in each filter.
The #lucky
button will directly send you to the
documentation of the first hit.
Source code
You can find the source code for this service at https://github.com/nomeata/loogle. The https://loogle.lean-lang.org/ service is provided by the Lean FRO.
This is Loogle revision 06e7f72
serving mathlib revision 3df560d