Loogle!

Result

Found 133 declarations mentioning HAdd.hAdd and tsum. Of these, 133 match your pattern(s).

• tsum_bool 📋 Mathlib.Topology.Algebra.InfiniteSum.Basic
  {α : Type u_1} [AddCommMonoid α] [TopologicalSpace α] (f : Bool → α) : ∑' (i : Bool), f i = f false + f true
• Summable.tsum_add 📋 Mathlib.Topology.Algebra.InfiniteSum.Basic
  {α : Type u_1} {β : Type u_2} [AddCommMonoid α] [TopologicalSpace α] {f g : β → α} {L : SummationFilter β} [T2Space α] [ContinuousAdd α] [L.NeBot] (hf : Summable f L) (hg : Summable g L) : ∑'[L] (b : β), (f b + g b) = ∑'[L] (b : β), f b + ∑'[L] (b : β), g b
• Summable.tsum_eq_add_tsum_ite' 📋 Mathlib.Topology.Algebra.InfiniteSum.Basic
  {α : Type u_1} {β : Type u_2} [AddCommMonoid α] [TopologicalSpace α] {L : SummationFilter β} [T2Space α] [ContinuousAdd α] [DecidableEq β] [L.LeAtTop] [L.NeBot] {f : β → α} (b : β) (hf : Summable (Function.update f b 0) L) : ∑'[L] (x : β), f x = f b + ∑'[L] (x : β), if x = b then 0 else f x
• Summable.tsum_add_tsum_compl 📋 Mathlib.Topology.Algebra.InfiniteSum.Basic
  {α : Type u_1} {β : Type u_2} [AddCommMonoid α] [TopologicalSpace α] {f : β → α} [T2Space α] [ContinuousAdd α] {s : Set β} (hs : Summable (f ∘ Subtype.val)) (hsc : Summable (f ∘ Subtype.val)) : ∑' (x : ↑s), f ↑x + ∑' (x : ↑sᶜ), f ↑x = ∑' (x : β), f x
• Summable.tsum_union_disjoint 📋 Mathlib.Topology.Algebra.InfiniteSum.Basic
  {α : Type u_1} {β : Type u_2} [AddCommMonoid α] [TopologicalSpace α] {f : β → α} [T2Space α] [ContinuousAdd α] {s t : Set β} (hd : Disjoint s t) (hs : Summable (f ∘ Subtype.val)) (ht : Summable (f ∘ Subtype.val)) : ∑' (x : ↑(s ∪ t)), f ↑x = ∑' (x : ↑s), f ↑x + ∑' (x : ↑t), f ↑x
• Summable.tsum_eq_add_tsum_ite 📋 Mathlib.Topology.Algebra.InfiniteSum.Group
  {α : Type u_1} {β : Type u_2} [AddCommGroup α] [TopologicalSpace α] [IsTopologicalAddGroup α] {f : β → α} [T2Space α] [DecidableEq β] (hf : Summable f) (b : β) : ∑' (n : β), f n = f b + ∑' (n : β), if n = b then 0 else f n
• Summable.sum_add_tsum_compl 📋 Mathlib.Topology.Algebra.InfiniteSum.Group
  {α : Type u_1} {β : Type u_2} [AddCommGroup α] [TopologicalSpace α] [IsTopologicalAddGroup α] {f : β → α} [T2Space α] {s : Finset β} (hf : Summable f) : ∑ x ∈ s, f x + ∑' (x : ↑(↑s)ᶜ), f ↑x = ∑' (x : β), f x
• Summable.tsum_subtype_add_tsum_subtype_compl 📋 Mathlib.Topology.Algebra.InfiniteSum.Group
  {α : Type u_1} {β : Type u_2} [UniformSpace α] [AddCommGroup α] [IsUniformAddGroup α] [CompleteSpace α] [T2Space α] {f : β → α} (hf : Summable f) (s : Set β) : ∑' (x : ↑s), f ↑x + ∑' (x : ↑sᶜ), f ↑x = ∑' (x : β), f x
• Summable.sum_add_tsum_subtype_compl 📋 Mathlib.Topology.Algebra.InfiniteSum.Group
  {α : Type u_1} {β : Type u_2} [UniformSpace α] [AddCommGroup α] [IsUniformAddGroup α] [CompleteSpace α] [T2Space α] {f : β → α} (hf : Summable f) (s : Finset β) : ∑ x ∈ s, f x + ∑' (x : { x // x ∉ s }), f ↑x = ∑' (x : β), f x
• tsum_pnat_eq_tsum_succ 📋 Mathlib.Topology.Algebra.InfiniteSum.NatInt
  {M : Type u_1} [AddCommMonoid M] [TopologicalSpace M] {f : ℕ → M} : ∑' (n : ℕ+), f ↑n = ∑' (n : ℕ), f (n + 1)
• tendsto_sum_nat_add 📋 Mathlib.Topology.Algebra.InfiniteSum.NatInt
  {G : Type u_2} [AddCommGroup G] [TopologicalSpace G] [IsTopologicalAddGroup G] [T2Space G] (f : ℕ → G) : Filter.Tendsto (fun i => ∑' (k : ℕ), f (k + i)) Filter.atTop (nhds 0)
• tsum_nat_add_neg_add_one 📋 Mathlib.Topology.Algebra.InfiniteSum.NatInt
  {M : Type u_1} [AddCommMonoid M] [TopologicalSpace M] [T2Space M] {f : ℤ → M} (hf : Summable f) : ∑' (n : ℕ), (f ↑n + f (-(↑n + 1))) = ∑' (n : ℤ), f n
• tsum_zero_pnat_eq_tsum_nat 📋 Mathlib.Topology.Algebra.InfiniteSum.NatInt
  {G : Type u_2} [AddCommGroup G] [TopologicalSpace G] [IsTopologicalAddGroup G] [T2Space G] {f : ℕ → G} (hf : Summable f) : f 0 + ∑' (n : ℕ+), f ↑n = ∑' (n : ℕ), f n
• Summable.tsum_eq_zero_add 📋 Mathlib.Topology.Algebra.InfiniteSum.NatInt
  {G : Type u_2} [AddCommGroup G] [TopologicalSpace G] [IsTopologicalAddGroup G] [T2Space G] {f : ℕ → G} (hf : Summable f) : ∑' (b : ℕ), f b = f 0 + ∑' (b : ℕ), f (b + 1)
• tsum_int_rec 📋 Mathlib.Topology.Algebra.InfiniteSum.NatInt
  {M : Type u_1} [AddCommMonoid M] [TopologicalSpace M] [ContinuousAdd M] [T2Space M] {f g : ℕ → M} (hf : Summable f) (hg : Summable g) : ∑' (n : ℤ), Int.rec f g n = ∑' (n : ℕ), f n + ∑' (n : ℕ), g n
• Summable.sum_add_tsum_nat_add 📋 Mathlib.Topology.Algebra.InfiniteSum.NatInt
  {G : Type u_2} [AddCommGroup G] [TopologicalSpace G] [IsTopologicalAddGroup G] [T2Space G] {f : ℕ → G} (k : ℕ) (h : Summable f) : ∑ i ∈ Finset.range k, f i + ∑' (i : ℕ), f (i + k) = ∑' (i : ℕ), f i
• Summable.sum_add_tsum_nat_add' 📋 Mathlib.Topology.Algebra.InfiniteSum.NatInt
  {M : Type u_1} [AddCommMonoid M] [TopologicalSpace M] [T2Space M] [ContinuousAdd M] {f : ℕ → M} {k : ℕ} (h : Summable fun n => f (n + k)) : ∑ i ∈ Finset.range k, f i + ∑' (i : ℕ), f (i + k) = ∑' (i : ℕ), f i
• tsum_eq_zero_add' 📋 Mathlib.Topology.Algebra.InfiniteSum.NatInt
  {M : Type u_1} [AddCommMonoid M] [TopologicalSpace M] [T2Space M] [ContinuousAdd M] {f : ℕ → M} (hf : Summable fun n => f (n + 1)) : ∑' (b : ℕ), f b = f 0 + ∑' (b : ℕ), f (b + 1)
• tsum_nat_add_neg 📋 Mathlib.Topology.Algebra.InfiniteSum.NatInt
  {M : Type u_1} [AddCommMonoid M] [TopologicalSpace M] [ContinuousAdd M] [T2Space M] {f : ℤ → M} (hf : Summable f) : ∑' (n : ℕ), (f ↑n + f (-↑n)) = ∑' (n : ℤ), f n + f 0
• tsum_int_eq_zero_add_two_mul_tsum_pnat 📋 Mathlib.Topology.Algebra.InfiniteSum.NatInt
  {G : Type u_2} [AddCommGroup G] [UniformSpace G] [IsUniformAddGroup G] [CompleteSpace G] [T2Space G] {f : ℤ → G} (hf : Function.Even f) (hf2 : Summable f) : ∑' (n : ℤ), f n = f 0 + 2 • ∑' (n : ℕ+), f ↑↑n
• rel_sup_add 📋 Mathlib.Topology.Algebra.InfiniteSum.NatInt
  {M : Type u_1} [AddCommMonoid M] [TopologicalSpace M] {α : Type u_3} [CompleteLattice α] (m : α → M) (m0 : m ⊥ = 0) (R : M → M → Prop) (m_iSup : ∀ (s : ℕ → α), R (m (⨆ i, s i)) (∑' (i : ℕ), m (s i))) (s₁ s₂ : α) : R (m (s₁ ⊔ s₂)) (m s₁ + m s₂)
• tsum_of_nat_of_neg_add_one 📋 Mathlib.Topology.Algebra.InfiniteSum.NatInt
  {M : Type u_1} [AddCommMonoid M] [TopologicalSpace M] [ContinuousAdd M] [T2Space M] {f : ℤ → M} (hf₁ : Summable fun n => f ↑n) (hf₂ : Summable fun n => f (-(↑n + 1))) : ∑' (n : ℤ), f n = ∑' (n : ℕ), f ↑n + ∑' (n : ℕ), f (-(↑n + 1))
• tsum_int_eq_zero_add_tsum_pnat 📋 Mathlib.Topology.Algebra.InfiniteSum.NatInt
  {G : Type u_2} [AddCommGroup G] [UniformSpace G] [IsUniformAddGroup G] [CompleteSpace G] [T2Space G] {f : ℤ → G} (hf2 : Summable f) : ∑' (n : ℤ), f n = f 0 + ∑' (n : ℕ+), f ↑↑n + ∑' (n : ℕ+), f (-↑↑n)
• Summable.tsum_of_nat_of_neg 📋 Mathlib.Topology.Algebra.InfiniteSum.NatInt
  {G : Type u_2} [AddCommGroup G] [TopologicalSpace G] [IsTopologicalAddGroup G] [T2Space G] {f : ℤ → G} (hf₁ : Summable fun n => f ↑n) (hf₂ : Summable fun n => f (-↑n)) : ∑' (n : ℤ), f n = ∑' (n : ℕ), f ↑n + ∑' (n : ℕ), f (-↑n) - f 0
• tsum_even_add_odd 📋 Mathlib.Topology.Algebra.InfiniteSum.NatInt
  {M : Type u_1} [AddCommMonoid M] [TopologicalSpace M] [T2Space M] [ContinuousAdd M] {f : ℕ → M} (he : Summable fun k => f (2 * k)) (ho : Summable fun k => f (2 * k + 1)) : ∑' (k : ℕ), f (2 * k) + ∑' (k : ℕ), f (2 * k + 1) = ∑' (k : ℕ), f k
• tsum_of_add_one_of_neg_add_one 📋 Mathlib.Topology.Algebra.InfiniteSum.NatInt
  {M : Type u_1} [AddCommMonoid M] [TopologicalSpace M] [ContinuousAdd M] [T2Space M] {f : ℤ → M} (hf₁ : Summable fun n => f (↑n + 1)) (hf₂ : Summable fun n => f (-(↑n + 1))) : ∑' (n : ℤ), f n = ∑' (n : ℕ), f (↑n + 1) + f 0 + ∑' (n : ℕ), f (-(↑n + 1))
• Summable.tsum_sum 📋 Mathlib.Topology.Algebra.InfiniteSum.Constructions
  {α : Type u_4} {β : Type u_5} {M : Type u_6} [AddCommMonoid M] [TopologicalSpace M] [ContinuousAdd M] [T2Space M] {f : α ⊕ β → M} (h₁ : Summable (f ∘ Sum.inl)) (h₂ : Summable (f ∘ Sum.inr)) : ∑' (i : α ⊕ β), f i = ∑' (i : α), f (Sum.inl i) + ∑' (i : β), f (Sum.inr i)
• tprod_one_add 📋 Mathlib.Topology.Algebra.InfiniteSum.Ring
  {ι : Type u_1} {α : Type u_3} [CommSemiring α] [TopologicalSpace α] {f : ι → α} [T2Space α] (h : Summable fun x => ∏ i ∈ x, f i) : ∏' (i : ι), (1 + f i) = ∑' (s : Finset ι), ∏ i ∈ s, f i
• Summable.tsum_mul_tsum_eq_tsum_sum_range 📋 Mathlib.Topology.Algebra.InfiniteSum.Ring
  {α : Type u_3} [TopologicalSpace α] [NonUnitalNonAssocSemiring α] {f g : ℕ → α} [T3Space α] [IsTopologicalSemiring α] (hf : Summable f) (hg : Summable g) (hfg : Summable fun x => f x.1 * g x.2) : (∑' (n : ℕ), f n) * ∑' (n : ℕ), g n = ∑' (n : ℕ), ∑ k ∈ Finset.range (n + 1), f k * g (n - k)
• tprod_one_add_ordered 📋 Mathlib.Topology.Algebra.InfiniteSum.Ring
  {ι : Type u_1} {α : Type u_3} [CommSemiring α] [TopologicalSpace α] {f : ι → α} [LinearOrder ι] [LocallyFiniteOrderBot ι] [T2Space α] [ContinuousAdd α] (hsum : Summable fun i => f i * ∏ j < i, (1 + f j)) (hprod : Multipliable fun x => 1 + f x) : ∏' (i : ι), (1 + f i) = 1 + ∑' (i : ι), f i * ∏ j < i, (1 + f j)
• NNReal.sum_add_tsum_nat_add 📋 Mathlib.Topology.Instances.NNReal.Lemmas
  {f : ℕ → NNReal} (k : ℕ) (hf : Summable f) : ∑' (i : ℕ), f i = ∑ i ∈ Finset.range k, f i + ∑' (i : ℕ), f (i + k)
• NNReal.tendsto_sum_nat_add 📋 Mathlib.Topology.Algebra.InfiniteSum.ENNReal
  (f : ℕ → NNReal) : Filter.Tendsto (fun i => ∑' (k : ℕ), f (k + i)) Filter.atTop (nhds 0)
• ENNReal.tendsto_sum_nat_add 📋 Mathlib.Topology.Algebra.InfiniteSum.ENNReal
  (f : ℕ → ENNReal) (hf : ∑' (i : ℕ), f i ≠ ⊤) : Filter.Tendsto (fun i => ∑' (k : ℕ), f (k + i)) Filter.atTop (nhds 0)
• ENNReal.tsum_eq_add_tsum_ite 📋 Mathlib.Topology.Algebra.InfiniteSum.ENNReal
  {β : Type u_2} {f : β → ENNReal} (b : β) : ∑' (x : β), f x = f b + ∑' (x : β), if x = b then 0 else f x
• ENNReal.tsum_add 📋 Mathlib.Topology.Algebra.InfiniteSum.ENNReal
  {α : Type u_1} {f g : α → ENNReal} : ∑' (a : α), (f a + g a) = ∑' (a : α), f a + ∑' (a : α), g a
• ENNReal.tsum_add_one_eq_top 📋 Mathlib.Topology.Algebra.InfiniteSum.ENNReal
  {f : ℕ → ENNReal} (hf : ∑' (n : ℕ), f n = ⊤) (hf0 : f 0 ≠ ⊤) : ∑' (n : ℕ), f (n + 1) = ⊤
• NNReal.tsum_eq_add_tsum_ite 📋 Mathlib.Topology.Algebra.InfiniteSum.ENNReal
  {α : Type u_1} {f : α → NNReal} (hf : Summable f) (i : α) : ∑' (x : α), f x = f i + ∑' (x : α), if x = i then 0 else f x
• edist_le_tsum_of_edist_le_of_tendsto 📋 Mathlib.Topology.Algebra.InfiniteSum.ENNReal
  {α : Type u_1} [PseudoEMetricSpace α] {f : ℕ → α} (d : ℕ → ENNReal) (hf : ∀ (n : ℕ), edist (f n) (f n.succ) ≤ d n) {a : α} (ha : Filter.Tendsto f Filter.atTop (nhds a)) (n : ℕ) : edist (f n) a ≤ ∑' (m : ℕ), d (n + m)
• ENNReal.sum_add_tsum_compl 📋 Mathlib.Topology.Algebra.InfiniteSum.ENNReal
  {ι : Type u_4} (s : Finset ι) (f : ι → ENNReal) : ∑ i ∈ s, f i + ∑' (i : ↑(↑s)ᶜ), f ↑i = ∑' (i : ι), f i
• ENNReal.tsum_union_le 📋 Mathlib.Topology.Algebra.InfiniteSum.ENNReal
  {α : Type u_1} (f : α → ENNReal) (s t : Set α) : ∑' (x : ↑(s ∪ t)), f ↑x ≤ ∑' (x : ↑s), f ↑x + ∑' (x : ↑t), f ↑x
• MeasureTheory.OuterMeasure.iUnion_nat_of_monotone_of_tsum_ne_top 📋 Mathlib.MeasureTheory.OuterMeasure.Basic
  {α : Type u_1} (m : MeasureTheory.OuterMeasure α) {s : ℕ → Set α} (h_mono : ∀ (n : ℕ), s n ⊆ s (n + 1)) (h0 : ∑' (k : ℕ), m (s (k + 1) \ s k) ≠ ⊤) : m (⋃ n, s n) = ⨆ n, m (s n)
• dist_le_tsum_of_dist_le_of_tendsto 📋 Mathlib.Topology.Algebra.InfiniteSum.Real
  {α : Type u_1} [PseudoMetricSpace α] {f : ℕ → α} (d : ℕ → ℝ) (hf : ∀ (n : ℕ), dist (f n) (f n.succ) ≤ d n) (hd : Summable d) {a : α} (ha : Filter.Tendsto f Filter.atTop (nhds a)) (n : ℕ) : dist (f n) a ≤ ∑' (m : ℕ), d (n + m)
• dist_le_tsum_dist_of_tendsto 📋 Mathlib.Topology.Algebra.InfiniteSum.Real
  {α : Type u_1} [PseudoMetricSpace α] {f : ℕ → α} {a : α} (h : Summable fun n => dist (f n) (f n.succ)) (ha : Filter.Tendsto f Filter.atTop (nhds a)) (n : ℕ) : dist (f n) a ≤ ∑' (m : ℕ), dist (f (n + m)) (f (n + m).succ)
• ENNReal.tsum_geometric_add_one 📋 Mathlib.Analysis.SpecificLimits.Basic
  (r : ENNReal) : ∑' (n : ℕ), r ^ (n + 1) = r * (1 - r)⁻¹
• MeasureTheory.inducedOuterMeasure_caratheodory 📋 Mathlib.MeasureTheory.OuterMeasure.Induced
  {α : Type u_1} {P : Set α → Prop} {m : (s : Set α) → P s → ENNReal} {P0 : P ∅} {m0 : m ∅ P0 = 0} (PU : ∀ ⦃f : ℕ → Set α⦄, (∀ (i : ℕ), P (f i)) → P (⋃ i, f i)) (msU : ∀ ⦃f : ℕ → Set α⦄ (hm : ∀ (i : ℕ), P (f i)), m (⋃ i, f i) ⋯ ≤ ∑' (i : ℕ), m (f i) ⋯) (m_mono : ∀ ⦃s₁ s₂ : Set α⦄ (hs₁ : P s₁) (hs₂ : P s₂), s₁ ⊆ s₂ → m s₁ hs₁ ≤ m s₂ hs₂) (s : Set α) : MeasurableSet s ↔ ∀ (t : Set α), P t → (MeasureTheory.inducedOuterMeasure m P0 m0) (t ∩ s) + (MeasureTheory.inducedOuterMeasure m P0 m0) (t \ s) ≤ (MeasureTheory.inducedOuterMeasure m P0 m0) t
• MeasureTheory.extend_union 📋 Mathlib.MeasureTheory.OuterMeasure.Induced
  {α : Type u_1} {P : Set α → Prop} {m : (s : Set α) → P s → ENNReal} (P0 : P ∅) (m0 : m ∅ P0 = 0) (PU : ∀ ⦃f : ℕ → Set α⦄, (∀ (i : ℕ), P (f i)) → P (⋃ i, f i)) (mU : ∀ ⦃f : ℕ → Set α⦄ (hm : ∀ (i : ℕ), P (f i)), Pairwise (Function.onFun Disjoint f) → m (⋃ i, f i) ⋯ = ∑' (i : ℕ), m (f i) ⋯) {s₁ s₂ : Set α} (hd : Disjoint s₁ s₂) (h₁ : P s₁) (h₂ : P s₂) : MeasureTheory.extend m (s₁ ∪ s₂) = MeasureTheory.extend m s₁ + MeasureTheory.extend m s₂
• MeasureTheory.inducedOuterMeasure_exists_set 📋 Mathlib.MeasureTheory.OuterMeasure.Induced
  {α : Type u_1} {P : Set α → Prop} {m : (s : Set α) → P s → ENNReal} {P0 : P ∅} {m0 : m ∅ P0 = 0} (PU : ∀ ⦃f : ℕ → Set α⦄, (∀ (i : ℕ), P (f i)) → P (⋃ i, f i)) (msU : ∀ ⦃f : ℕ → Set α⦄ (hm : ∀ (i : ℕ), P (f i)), m (⋃ i, f i) ⋯ ≤ ∑' (i : ℕ), m (f i) ⋯) (m_mono : ∀ ⦃s₁ s₂ : Set α⦄ (hs₁ : P s₁) (hs₂ : P s₂), s₁ ⊆ s₂ → m s₁ hs₁ ≤ m s₂ hs₂) {s : Set α} (hs : (MeasureTheory.inducedOuterMeasure m P0 m0) s ≠ ⊤) {ε : ENNReal} (hε : ε ≠ 0) : ∃ t, P t ∧ s ⊆ t ∧ (MeasureTheory.inducedOuterMeasure m P0 m0) t ≤ (MeasureTheory.inducedOuterMeasure m P0 m0) s + ε
• measure_eq_measure_preimage_add_measure_tsum_Ico_zpow 📋 Mathlib.MeasureTheory.Constructions.BorelSpace.Order
  {α : Type u_5} {mα : MeasurableSpace α} (μ : MeasureTheory.Measure α) {f : α → ENNReal} (hf : Measurable f) {s : Set α} (hs : MeasurableSet s) {t : NNReal} (ht : 1 < t) : μ s = μ (s ∩ f ⁻¹' {0}) + μ (s ∩ f ⁻¹' {⊤}) + ∑' (n : ℤ), μ (s ∩ f ⁻¹' Set.Ico (↑t ^ n) (↑t ^ (n + 1)))
• hasSum_sum_range_mul_of_summable_norm 📋 Mathlib.Analysis.Normed.Ring.InfiniteSum
  {R : Type u_1} [NormedRing R] [CompleteSpace R] {f g : ℕ → R} (hf : Summable fun x => ‖f x‖) (hg : Summable fun x => ‖g x‖) : HasSum (fun n => ∑ k ∈ Finset.range (n + 1), f k * g (n - k)) ((∑' (n : ℕ), f n) * ∑' (n : ℕ), g n)
• tsum_mul_tsum_eq_tsum_sum_range_of_summable_norm 📋 Mathlib.Analysis.Normed.Ring.InfiniteSum
  {R : Type u_1} [NormedRing R] [CompleteSpace R] {f g : ℕ → R} (hf : Summable fun x => ‖f x‖) (hg : Summable fun x => ‖g x‖) : (∑' (n : ℕ), f n) * ∑' (n : ℕ), g n = ∑' (n : ℕ), ∑ k ∈ Finset.range (n + 1), f k * g (n - k)
• hasSum_sum_range_mul_of_summable_norm' 📋 Mathlib.Analysis.Normed.Ring.InfiniteSum
  {R : Type u_1} [NormedRing R] {f g : ℕ → R} (hf : Summable fun x => ‖f x‖) (h'f : Summable f) (hg : Summable fun x => ‖g x‖) (h'g : Summable g) : HasSum (fun n => ∑ k ∈ Finset.range (n + 1), f k * g (n - k)) ((∑' (n : ℕ), f n) * ∑' (n : ℕ), g n)
• tsum_mul_tsum_eq_tsum_sum_range_of_summable_norm' 📋 Mathlib.Analysis.Normed.Ring.InfiniteSum
  {R : Type u_1} [NormedRing R] {f g : ℕ → R} (hf : Summable fun x => ‖f x‖) (h'f : Summable f) (hg : Summable fun x => ‖g x‖) (h'g : Summable g) : (∑' (n : ℕ), f n) * ∑' (n : ℕ), g n = ∑' (n : ℕ), ∑ k ∈ Finset.range (n + 1), f k * g (n - k)
• tsum_geometric_le_of_norm_lt_one 📋 Mathlib.Analysis.SpecificLimits.Normed
  {R : Type u_4} [NormedRing R] (x : R) (h : ‖x‖ < 1) : ‖∑' (n : ℕ), x ^ n‖ ≤ ‖1‖ - 1 + (1 - ‖x‖)⁻¹
• geom_series_mul_shift 📋 Mathlib.Analysis.SpecificLimits.Normed
  {R : Type u_4} [NormedRing R] [HasSummableGeomSeries R] (x : R) (h : ‖x‖ < 1) : x * ∑' (i : ℕ), x ^ i = ∑' (i : ℕ), x ^ (i + 1)
• geom_series_succ 📋 Mathlib.Analysis.SpecificLimits.Normed
  {R : Type u_4} [NormedRing R] [HasSummableGeomSeries R] (x : R) (h : ‖x‖ < 1) : ∑' (i : ℕ), x ^ (i + 1) = ∑' (i : ℕ), x ^ i - 1
• tsum_choose_mul_geometric_of_norm_lt_one' 📋 Mathlib.Analysis.SpecificLimits.Normed
  {R : Type u_4} [NormedRing R] [HasSummableGeomSeries R] (k : ℕ) {r : R} (hr : ‖r‖ < 1) : ∑' (n : ℕ), ↑((n + k).choose k) * r ^ n = Ring.inverse (1 - r) ^ (k + 1)
• tsum_choose_mul_geometric_of_norm_lt_one 📋 Mathlib.Analysis.SpecificLimits.Normed
  {𝕜 : Type u_5} [NormedDivisionRing 𝕜] (k : ℕ) {r : 𝕜} (hr : ‖r‖ < 1) : ∑' (n : ℕ), ↑((n + k).choose k) * r ^ n = 1 / (1 - r) ^ (k + 1)
• geom_series_mul_one_add 📋 Mathlib.Analysis.SpecificLimits.Normed
  {R : Type u_4} [NormedRing R] [HasSummableGeomSeries R] (x : R) (h : ‖x‖ < 1) : (1 + x) * ∑' (i : ℕ), x ^ i = 2 * ∑' (i : ℕ), x ^ i - 1
• tsum_descFactorial_mul_geometric_of_norm_lt_one' 📋 Mathlib.Analysis.SpecificLimits.Normed
  {R : Type u_4} [NormedRing R] [HasSummableGeomSeries R] (j : ℕ) {r : R} (h : ‖r‖ < 1) : ∑' (n : ℕ), ↑(n.descFactorial j) * r ^ n = ↑j.factorial * r ^ j * Ring.inverse (1 - r) ^ (j + 1)
• tsum_descFactorial_mul_geometric_of_norm_lt_one 📋 Mathlib.Analysis.SpecificLimits.Normed
  {𝕜 : Type u_5} [NormedDivisionRing 𝕜] (j : ℕ) {r : 𝕜} (hr : ‖r‖ < 1) : ∑' (n : ℕ), ↑(n.descFactorial j) * r ^ n = ↑j.factorial * r ^ j / (1 - r) ^ (j + 1)
• tsum_sq_mul_geometric_of_norm_lt_one' 📋 Mathlib.Analysis.SpecificLimits.Normed
  {R : Type u_4} [NormedRing R] [HasSummableGeomSeries R] {r : R} (h : ‖r‖ < 1) : ∑' (n : ℕ), ↑n ^ 2 * r ^ n = r * (1 + r) * Ring.inverse (1 - r) ^ 3
• tsum_sq_mul_geometric_of_norm_lt_one 📋 Mathlib.Analysis.SpecificLimits.Normed
  {𝕜 : Type u_5} [NormedDivisionRing 𝕜] {r : 𝕜} (hr : ‖r‖ < 1) : ∑' (n : ℕ), ↑n ^ 2 * r ^ n = r * (1 + r) / (1 - r) ^ 3
• tsum_pow_mul_geometric_of_norm_lt_one' 📋 Mathlib.Analysis.SpecificLimits.Normed
  {R : Type u_4} [NormedRing R] [HasSummableGeomSeries R] (k : ℕ) {r : R} (h : ‖r‖ < 1) : ∑' (n : ℕ), ↑n ^ k * r ^ n = ∑ j ∈ Finset.range (k + 1), ↑(k.stirlingSecond j) * ↑j.factorial * r ^ j * Ring.inverse (1 - r) ^ (j + 1)
• tsum_pow_mul_geometric_of_norm_lt_one 📋 Mathlib.Analysis.SpecificLimits.Normed
  {𝕜 : Type u_5} [NormedDivisionRing 𝕜] (k : ℕ) {r : 𝕜} (hr : ‖r‖ < 1) : ∑' (n : ℕ), ↑n ^ k * r ^ n = ∑ j ∈ Finset.range (k + 1), ↑(k.stirlingSecond j) * ↑j.factorial * r ^ j / (1 - r) ^ (j + 1)
• NNReal.Lp_add_le_tsum' 📋 Mathlib.Analysis.MeanInequalities
  {ι : Type u} {f g : ι → NNReal} {p : ℝ} (hp : 1 ≤ p) (hf : Summable fun i => f i ^ p) (hg : Summable fun i => g i ^ p) : (∑' (i : ι), (f i + g i) ^ p) ^ (1 / p) ≤ (∑' (i : ι), f i ^ p) ^ (1 / p) + (∑' (i : ι), g i ^ p) ^ (1 / p)
• Real.Lp_add_le_tsum_of_nonneg' 📋 Mathlib.Analysis.MeanInequalities
  {ι : Type u} {f g : ι → ℝ} {p : ℝ} (hp : 1 ≤ p) (hf : ∀ (i : ι), 0 ≤ f i) (hg : ∀ (i : ι), 0 ≤ g i) (hf_sum : Summable fun i => f i ^ p) (hg_sum : Summable fun i => g i ^ p) : (∑' (i : ι), (f i + g i) ^ p) ^ (1 / p) ≤ (∑' (i : ι), f i ^ p) ^ (1 / p) + (∑' (i : ι), g i ^ p) ^ (1 / p)
• NNReal.Lp_add_le_tsum 📋 Mathlib.Analysis.MeanInequalities
  {ι : Type u} {f g : ι → NNReal} {p : ℝ} (hp : 1 ≤ p) (hf : Summable fun i => f i ^ p) (hg : Summable fun i => g i ^ p) : (Summable fun i => (f i + g i) ^ p) ∧ (∑' (i : ι), (f i + g i) ^ p) ^ (1 / p) ≤ (∑' (i : ι), f i ^ p) ^ (1 / p) + (∑' (i : ι), g i ^ p) ^ (1 / p)
• Real.Lp_add_le_tsum_of_nonneg 📋 Mathlib.Analysis.MeanInequalities
  {ι : Type u} {f g : ι → ℝ} {p : ℝ} (hp : 1 ≤ p) (hf : ∀ (i : ι), 0 ≤ f i) (hg : ∀ (i : ι), 0 ≤ g i) (hf_sum : Summable fun i => f i ^ p) (hg_sum : Summable fun i => g i ^ p) : (Summable fun i => (f i + g i) ^ p) ∧ (∑' (i : ι), (f i + g i) ^ p) ^ (1 / p) ≤ (∑' (i : ι), f i ^ p) ^ (1 / p) + (∑' (i : ι), g i ^ p) ^ (1 / p)
• Nat.sumByResidueClasses 📋 Mathlib.Analysis.SumOverResidueClass
  {R : Type u_1} [AddCommGroup R] [UniformSpace R] [IsUniformAddGroup R] [CompleteSpace R] [T0Space R] {f : ℕ → R} (hf : Summable f) (N : ℕ) [NeZero N] : ∑' (n : ℕ), f n = ∑ j, ∑' (m : ℕ), f (j.val + N * m)
• ENNReal.le_tsum_condensed 📋 Mathlib.Analysis.PSeries
  {f : ℕ → ENNReal} (hf : ∀ ⦃m n : ℕ⦄, 0 < m → m ≤ n → f n ≤ f m) : ∑' (k : ℕ), f k ≤ f 0 + ∑' (k : ℕ), 2 ^ k * f (2 ^ k)
• ENNReal.le_tsum_schlomilch 📋 Mathlib.Analysis.PSeries
  {u : ℕ → ℕ} {f : ℕ → ENNReal} (hf : ∀ ⦃m n : ℕ⦄, 0 < m → m ≤ n → f n ≤ f m) (h_pos : ∀ (n : ℕ), 0 < u n) (hu : StrictMono u) : ∑' (k : ℕ), f k ≤ ∑ k ∈ Finset.range (u 0), f k + ∑' (k : ℕ), (↑(u (k + 1)) - ↑(u k)) * f (u k)
• ENNReal.tsum_condensed_le 📋 Mathlib.Analysis.PSeries
  {f : ℕ → ENNReal} (hf : ∀ ⦃m n : ℕ⦄, 1 < m → m ≤ n → f n ≤ f m) : ∑' (k : ℕ), 2 ^ k * f (2 ^ k) ≤ f 1 + 2 * ∑' (k : ℕ), f k
• ENNReal.tsum_schlomilch_le 📋 Mathlib.Analysis.PSeries
  {u : ℕ → ℕ} {f : ℕ → ENNReal} {C : ℕ} (hf : ∀ ⦃m n : ℕ⦄, 1 < m → m ≤ n → f n ≤ f m) (h_pos : ∀ (n : ℕ), 0 < u n) (h_nonneg : ∀ (n : ℕ), 0 ≤ f n) (hu : Monotone u) (h_succ_diff : SuccDiffBounded C u) : ∑' (k : ℕ), (↑(u (k + 1)) - ↑(u k)) * f (u k) ≤ (↑(u 1) - ↑(u 0)) * f (u 0) + ↑C * ∑' (k : ℕ), f k
• ZLattice.tsumNormRPowBound_spec 📋 Mathlib.Algebra.Module.ZLattice.Summable
  {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] [FiniteDimensional ℝ E] (L : Submodule ℤ E) [DiscreteTopology ↥L] (r : ℝ) (h : r < -↑(Module.finrank ℤ ↥L)) (s : Finset ↥L) : ∑ z ∈ s, ‖z‖ ^ r ≤ ZLattice.tsumNormRPowBound L ^ r * ∑' (k : ℕ), ↑k ^ (↑(Module.finrank ℤ ↥L) - 1 + r)
• ZLattice.tsum_norm_rpow_le 📋 Mathlib.Algebra.Module.ZLattice.Summable
  {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] [FiniteDimensional ℝ E] (L : Submodule ℤ E) [DiscreteTopology ↥L] (r : ℝ) (hr : r < -↑(Module.finrank ℤ ↥L)) : ∑' (z : ↥L), ‖z‖ ^ r ≤ ZLattice.tsumNormRPowBound L ^ r * ∑' (k : ℕ), ↑k ^ (↑(Module.finrank ℤ ↥L) - 1 + r)
• ZLattice.exists_finsetSum_norm_rpow_le_tsum 📋 Mathlib.Algebra.Module.ZLattice.Summable
  {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] [FiniteDimensional ℝ E] (L : Submodule ℤ E) [DiscreteTopology ↥L] : ∃ A > 0, ∀ r < -↑(Module.finrank ℤ ↥L), ∀ (s : Finset ↥L), ∑ z ∈ s, ‖z‖ ^ r ≤ A ^ r * ∑' (k : ℕ), ↑k ^ (↑(Module.finrank ℤ ↥L) - 1 + r)
• ZLattice.sum_piFinset_Icc_rpow_le 📋 Mathlib.Algebra.Module.ZLattice.Summable
  {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] [FiniteDimensional ℝ E] {L : Submodule ℤ E} [DiscreteTopology ↥L] {ι : Type u_3} [Fintype ι] [DecidableEq ι] (b : Module.Basis ι ℤ ↥L) {d : ℕ} (hd : d = Fintype.card ι) (n : ℕ) (r : ℝ) (hr : r < -↑d) : ∑ p ∈ Fintype.piFinset fun x => Finset.Icc (-↑n) ↑n, ‖∑ i, p i • b i‖ ^ r ≤ 2 * ↑d * 3 ^ (d - 1) * ZLattice.normBound b ^ r * ∑' (k : ℕ), ↑k ^ (↑d - 1 + r)
• FormalMultilinearSeries.nnnorm_changeOrigin_le 📋 Mathlib.Analysis.Analytic.ChangeOrigin
  {𝕜 : Type u_1} {E : Type u_2} {F : Type u_3} [NontriviallyNormedField 𝕜] [NormedAddCommGroup E] [NormedSpace 𝕜 E] [NormedAddCommGroup F] [NormedSpace 𝕜 F] (p : FormalMultilinearSeries 𝕜 E F) {x : E} (k : ℕ) (h : ↑‖x‖₊ < p.radius) : ‖p.changeOrigin x k‖₊ ≤ ∑' (s : (l : ℕ) × { s // s.card = l }), ‖p (k + s.fst)‖₊ * ‖x‖₊ ^ s.fst
• FormalMultilinearSeries.nnnorm_changeOriginSeries_apply_le_tsum 📋 Mathlib.Analysis.Analytic.ChangeOrigin
  {𝕜 : Type u_1} {E : Type u_2} {F : Type u_3} [NontriviallyNormedField 𝕜] [NormedAddCommGroup E] [NormedSpace 𝕜 E] [NormedAddCommGroup F] [NormedSpace 𝕜 F] (p : FormalMultilinearSeries 𝕜 E F) (k l : ℕ) (x : E) : ‖(p.changeOriginSeries k l) fun x_1 => x‖₊ ≤ ∑' (x_1 : { s // s.card = l }), ‖p (k + l)‖₊ * ‖x‖₊ ^ l
• FormalMultilinearSeries.nnnorm_changeOriginSeries_le_tsum 📋 Mathlib.Analysis.Analytic.ChangeOrigin
  {𝕜 : Type u_1} {E : Type u_2} {F : Type u_3} [NontriviallyNormedField 𝕜] [NormedAddCommGroup E] [NormedSpace 𝕜 E] [NormedAddCommGroup F] [NormedSpace 𝕜 F] (p : FormalMultilinearSeries 𝕜 E F) (k l : ℕ) : ‖p.changeOriginSeries k l‖₊ ≤ ∑' (x : { s // s.card = l }), ‖p (k + l)‖₊
• Besicovitch.exists_closedBall_covering_tsum_measure_le 📋 Mathlib.MeasureTheory.Covering.Besicovitch
  {α : Type u_1} [MetricSpace α] [SecondCountableTopology α] [MeasurableSpace α] [OpensMeasurableSpace α] [HasBesicovitchCovering α] (μ : MeasureTheory.Measure α) [MeasureTheory.SFinite μ] [μ.OuterRegular] {ε : ENNReal} (hε : ε ≠ 0) (f : α → Set ℝ) (s : Set α) (hf : ∀ x ∈ s, ∀ δ > 0, (f x ∩ Set.Ioo 0 δ).Nonempty) : ∃ t r, t.Countable ∧ t ⊆ s ∧ (∀ x ∈ t, r x ∈ f x) ∧ s ⊆ ⋃ x ∈ t, Metric.closedBall x (r x) ∧ ∑' (x : ↑t), μ (Metric.closedBall (↑x) (r ↑x)) ≤ μ s + ε
• Complex.abel_aux 📋 Mathlib.Analysis.Complex.AbelLimit
  {f : ℕ → ℂ} {l : ℂ} (h : Filter.Tendsto (fun n => ∑ i ∈ Finset.range n, f i) Filter.atTop (nhds l)) {z : ℂ} (hz : ‖z‖ < 1) : Filter.Tendsto (fun n => (1 - z) * ∑ i ∈ Finset.range n, (l - ∑ j ∈ Finset.range (i + 1), f j) * z ^ i) Filter.atTop (nhds (l - ∑' (n : ℕ), f n * z ^ n))
• Real.tsum_eq_tsum_fourier_of_rpow_decay_of_summable 📋 Mathlib.Analysis.Fourier.PoissonSummation
  {f : ℝ → ℂ} (hc : Continuous f) {b : ℝ} (hb : 1 < b) (hf : f =O[Filter.cocompact ℝ] fun x => |x| ^ (-b)) (hFf : Summable fun n => FourierTransform.fourier f ↑n) (x : ℝ) : ∑' (n : ℤ), f (x + ↑n) = ∑' (n : ℤ), FourierTransform.fourier f ↑n * (fourier n) ↑x
• Real.tsum_eq_tsum_fourier_of_rpow_decay 📋 Mathlib.Analysis.Fourier.PoissonSummation
  {f : ℝ → ℂ} (hc : Continuous f) {b : ℝ} (hb : 1 < b) (hf : f =O[Filter.cocompact ℝ] fun x => |x| ^ (-b)) (hFf : FourierTransform.fourier f =O[Filter.cocompact ℝ] fun x => |x| ^ (-b)) (x : ℝ) : ∑' (n : ℤ), f (x + ↑n) = ∑' (n : ℤ), FourierTransform.fourier f ↑n * (fourier n) ↑x
• SchwartzMap.tsum_eq_tsum_fourier 📋 Mathlib.Analysis.Fourier.PoissonSummation
  (f : SchwartzMap ℝ ℂ) (x : ℝ) : ∑' (n : ℤ), f (x + ↑n) = ∑' (n : ℤ), (FourierTransform.fourier f) ↑n * (fourier n) ↑x
• Real.tsum_eq_tsum_fourier 📋 Mathlib.Analysis.Fourier.PoissonSummation
  {f : C(ℝ, ℂ)} (h_norm : ∀ (K : TopologicalSpace.Compacts ℝ), Summable fun n => ‖ContinuousMap.restrict (↑K) (f.comp (ContinuousMap.addRight ↑n))‖) (h_sum : Summable fun n => FourierTransform.fourier ⇑f ↑n) (x : ℝ) : ∑' (n : ℤ), f (x + ↑n) = ∑' (n : ℤ), FourierTransform.fourier ⇑f ↑n * (fourier n) ↑x
• Real.sinh_eq_tsum 📋 Mathlib.Analysis.SpecialFunctions.Trigonometric.Series
  (r : ℝ) : Real.sinh r = ∑' (n : ℕ), r ^ (2 * n + 1) / ↑(2 * n + 1).factorial
• Complex.sinh_eq_tsum 📋 Mathlib.Analysis.SpecialFunctions.Trigonometric.Series
  (z : ℂ) : Complex.sinh z = ∑' (n : ℕ), z ^ (2 * n + 1) / ↑(2 * n + 1).factorial
• Complex.sin_eq_tsum' 📋 Mathlib.Analysis.SpecialFunctions.Trigonometric.Series
  (z : ℂ) : Complex.sin z = ∑' (n : ℕ), (z * Complex.I) ^ (2 * n + 1) / ↑(2 * n + 1).factorial / Complex.I
• Real.sin_eq_tsum 📋 Mathlib.Analysis.SpecialFunctions.Trigonometric.Series
  (r : ℝ) : Real.sin r = ∑' (n : ℕ), (-1) ^ n * r ^ (2 * n + 1) / ↑(2 * n + 1).factorial
• Complex.sin_eq_tsum 📋 Mathlib.Analysis.SpecialFunctions.Trigonometric.Series
  (z : ℂ) : Complex.sin z = ∑' (n : ℕ), (-1) ^ n * z ^ (2 * n + 1) / ↑(2 * n + 1).factorial
• Summable.hasSumUniformlyOn_log_one_add 📋 Mathlib.Analysis.Normed.Module.MultipliableUniformlyOn
  {α : Type u_1} {ι : Type u_2} {K : Set α} {u : ι → ℝ} {f : ι → α → ℂ} (hu : Summable u) (h : ∀ᶠ (i : ι) in Filter.cofinite, ∀ x ∈ K, ‖f i x‖ ≤ u i) : HasSumUniformlyOn (fun i x => Complex.log (1 + f i x)) (fun x => ∑' (i : ι), Complex.log (1 + f i x)) K
• Summable.tendstoUniformlyOn_tsum_nat_log_one_add 📋 Mathlib.Analysis.Normed.Module.MultipliableUniformlyOn
  {α : Type u_1} {K : Set α} {f : ℕ → α → ℂ} {u : ℕ → ℝ} (hu : Summable u) (h : ∀ᶠ (n : ℕ) in Filter.atTop, ∀ x ∈ K, ‖f n x‖ ≤ u n) : TendstoUniformlyOn (fun n x => ∑ m ∈ Finset.range n, Complex.log (1 + f m x)) (fun x => ∑' (n : ℕ), Complex.log (1 + f n x)) Filter.atTop K
• Complex.tsum_exp_neg_quadratic 📋 Mathlib.Analysis.SpecialFunctions.Gaussian.PoissonSummation
  {a : ℂ} (ha : 0 < a.re) (b : ℂ) : ∑' (n : ℤ), Complex.exp (-↑Real.pi * a * ↑n ^ 2 + 2 * ↑Real.pi * b * ↑n) = 1 / a ^ (1 / 2) * ∑' (n : ℤ), Complex.exp (-↑Real.pi / a * (↑n + Complex.I * b) ^ 2)
• cot_series_rep 📋 Mathlib.Analysis.SpecialFunctions.Trigonometric.Cotangent
  {x : ℂ} (hz : x ∈ Complex.integerComplement) : ↑Real.pi * (↑Real.pi * x).cot = 1 / x + ∑' (n : ℕ+), (1 / (x - ↑↑n) + 1 / (x + ↑↑n))
• cot_series_rep' 📋 Mathlib.Analysis.SpecialFunctions.Trigonometric.Cotangent
  {x : ℂ} (hz : x ∈ Complex.integerComplement) : ↑Real.pi * (↑Real.pi * x).cot - 1 / x = ∑' (n : ℕ), (1 / (x - (↑n + 1)) + 1 / (x + (↑n + 1)))
• iteratedDerivWithin_cot_pi_mul_eq_mul_tsum_zpow 📋 Mathlib.Analysis.SpecialFunctions.Trigonometric.Cotangent
  {k : ℕ} (hk : 1 ≤ k) {z : ℂ} (hz : z ∈ UpperHalfPlane.upperHalfPlaneSet) : iteratedDerivWithin k (fun x => ↑Real.pi * (↑Real.pi * x).cot) UpperHalfPlane.upperHalfPlaneSet z = (-1) ^ k * ↑k.factorial * ∑' (n : ℤ), (z + ↑n) ^ (-1 - ↑k)
• iteratedDerivWithin_cot_pi_mul_eq_mul_tsum_div_pow 📋 Mathlib.Analysis.SpecialFunctions.Trigonometric.Cotangent
  {k : ℕ} (hk : 1 ≤ k) {z : ℂ} (hz : z ∈ UpperHalfPlane.upperHalfPlaneSet) : iteratedDerivWithin k (fun x => ↑Real.pi * (↑Real.pi * x).cot) UpperHalfPlane.upperHalfPlaneSet z = (-1) ^ k * ↑k.factorial * ∑' (n : ℤ), 1 / (z + ↑n) ^ (k + 1)
• iteratedDerivWithin_cot_sub_inv_eq_add_mul_tsum 📋 Mathlib.Analysis.SpecialFunctions.Trigonometric.Cotangent
  {z : ℂ} {k : ℕ} (hk : 1 ≤ k) (hz : z ∈ UpperHalfPlane.upperHalfPlaneSet) : iteratedDerivWithin k (fun x => ↑Real.pi * (↑Real.pi * x).cot - 1 / x) UpperHalfPlane.upperHalfPlaneSet z = -(-1) ^ k * ↑k.factorial * z ^ (-1 - ↑k) + (-1) ^ k * ↑k.factorial * ∑' (n : ℤ), (z + ↑n) ^ (-1 - ↑k)
• AntitoneOn.integral_le_tsum_comp_add 📋 Mathlib.Analysis.SumIntegralComparisons
  {f : ℝ → ℝ} (N : ℕ) (anti : AntitoneOn f (Set.Ici ↑N)) (summable : Summable fun n => f ↑n) (nonneg : ∀ t ∈ Set.Ioi ↑N, 0 ≤ f t) : ∫ (x : ℝ) in Set.Ioi ↑N, f x ≤ ∑' (n : ℕ), f ↑(n + N)
• AntitoneOn.tsum_add_one_le_integral 📋 Mathlib.Analysis.SumIntegralComparisons
  {f : ℝ → ℝ} (anti : AntitoneOn f (Set.Ici 0)) (integrable : MeasureTheory.IntegrableOn f (Set.Ioi 0) MeasureTheory.volume) (nonneg : ∀ t ∈ Set.Ioi 0, 0 ≤ f t) : ∑' (n : ℕ), f ↑(n + 1) ≤ ∫ (x : ℝ) in Set.Ioi 0, f x
• AntitoneOn.tsum_comp_add_le_integral 📋 Mathlib.Analysis.SumIntegralComparisons
  {f : ℝ → ℝ} (N : ℕ) (anti : AntitoneOn f (Set.Ici ↑N)) (integrable : MeasureTheory.IntegrableOn f (Set.Ioi ↑N) MeasureTheory.volume) (nonneg : ∀ t ∈ Set.Ioi ↑N, 0 ≤ f t) : ∑' (n : ℕ), f ↑(n + N + 1) ≤ ∫ (x : ℝ) in Set.Ioi ↑N, f x
• AntitoneOn.tsum_le_integral 📋 Mathlib.Analysis.SumIntegralComparisons
  {f : ℝ → ℝ} (anti : AntitoneOn f (Set.Ici 0)) (integrable : MeasureTheory.IntegrableOn f (Set.Ioi 0) MeasureTheory.volume) (nonneg : ∀ t ∈ Set.Ioi 0, 0 ≤ f t) : ∑' (n : ℕ), f ↑n ≤ f 0 + ∫ (x : ℝ) in Set.Ioi 0, f x
• Nat.Partition.multipliable_genFun 📋 Mathlib.Combinatorics.Enumerative.Partition.GenFun
  {R : Type u_1} [CommSemiring R] [TopologicalSpace R] [T2Space R] (f : ℕ → ℕ → R) : Multipliable fun i => 1 + ∑' (j : ℕ), f (i + 1) (j + 1) • PowerSeries.X ^ ((i + 1) * (j + 1))
• Nat.Partition.hasProd_genFun 📋 Mathlib.Combinatorics.Enumerative.Partition.GenFun
  {R : Type u_1} [CommSemiring R] [TopologicalSpace R] [T2Space R] (f : ℕ → ℕ → R) : HasProd (fun i => 1 + ∑' (j : ℕ), f (i + 1) (j + 1) • PowerSeries.X ^ ((i + 1) * (j + 1))) (Nat.Partition.genFun f)
• Nat.Partition.genFun_eq_tprod 📋 Mathlib.Combinatorics.Enumerative.Partition.GenFun
  {R : Type u_1} [CommSemiring R] [TopologicalSpace R] [T2Space R] (f : ℕ → ℕ → R) : Nat.Partition.genFun f = ∏' (i : ℕ), (1 + ∑' (j : ℕ), f (i + 1) (j + 1) • PowerSeries.X ^ ((i + 1) * (j + 1)))
• Nat.Partition.multipliable_powerSeriesMk_card_restricted 📋 Mathlib.Combinatorics.Enumerative.Partition.Glaisher
  (R : Type u_1) [TopologicalSpace R] [T2Space R] [CommSemiring R] [IsTopologicalSemiring R] (p : ℕ → Prop) [DecidablePred p] : Multipliable fun i => if p (i + 1) then ∑' (j : ℕ), PowerSeries.X ^ ((i + 1) * j) else 1
• Nat.Partition.hasProd_powerSeriesMk_card_restricted 📋 Mathlib.Combinatorics.Enumerative.Partition.Glaisher
  (R : Type u_1) [TopologicalSpace R] [T2Space R] [CommSemiring R] [IsTopologicalSemiring R] (p : ℕ → Prop) [DecidablePred p] : HasProd (fun i => if p (i + 1) then ∑' (j : ℕ), PowerSeries.X ^ ((i + 1) * j) else 1) (PowerSeries.mk fun n => ↑(Nat.Partition.restricted n p).card)
• Nat.Partition.powerSeriesMk_card_restricted_eq_tprod 📋 Mathlib.Combinatorics.Enumerative.Partition.Glaisher
  (R : Type u_1) [TopologicalSpace R] [T2Space R] [CommSemiring R] [IsTopologicalSemiring R] (p : ℕ → Prop) [DecidablePred p] : (PowerSeries.mk fun n => ↑(Nat.Partition.restricted n p).card) = ∏' (i : ℕ), if p (i + 1) then ∑' (j : ℕ), PowerSeries.X ^ ((i + 1) * j) else 1
• Pentagonal.tprod_one_sub_pow 📋 Mathlib.Combinatorics.Enumerative.Pentagonal.Ring
  {R : Type u_1} [CommRing R] [TopologicalSpace R] [IsTopologicalRing R] [T2Space R] {x : R} (hx : IsTopologicallyNilpotent x) (hsum : ∀ (k : ℕ), Summable fun n => x ^ ((k + 1) * n) * ∏ i ∈ Finset.range (n + 1), (1 - x ^ (k + i + 1))) (hlhs : ∀ (k : ℕ), Multipliable fun n => 1 - x ^ (n + k + 1)) (hrhs : Summable fun k => (-1) ^ k * (x ^ pentagonal (-↑k) - x ^ pentagonal (↑k + 1))) (htail : Filter.Tendsto (fun k => (-1) ^ (k + 1) * x ^ ((k + 1) * (3 * k + 4) / 2) * ∑' (n : ℕ), x ^ ((k + 1) * n) * ∏ i ∈ Finset.range (n + 1), (1 - x ^ (k + i + 1))) Filter.atTop (nhds 0)) : ∏' (n : ℕ), (1 - x ^ (n + 1)) = ∑' (k : ℕ), (-1) ^ k * (x ^ pentagonal (-↑k) - x ^ pentagonal (↑k + 1))
• PowerSeries.WithPiTopology.pentagonalSeries_eq_tsum_pow_pentagonal_sub 📋 Mathlib.Combinatorics.Enumerative.Pentagonal.PowerSeries
  (R : Type u_1) [CommRing R] [TopologicalSpace R] [T2Space R] : PowerSeries.pentagonalSeries R = ∑' (k : ℕ), (-1) ^ k * (PowerSeries.X ^ pentagonal (-↑k) - PowerSeries.X ^ pentagonal (↑k + 1))
• eulerFunction_eq_tsum_pentagonal_pair 📋 Mathlib.Combinatorics.Enumerative.Pentagonal.EulerFunction
  {R : Type u_1} [NormedCommRing R] [NormOneClass R] [CompleteSpace R] {x : R} (hx : ‖x‖ < 1) : eulerFunction x = ∑' (k : ℕ), (-1) ^ k * (x ^ pentagonal (-↑k) - x ^ pentagonal (↑k + 1))
• tsum_eq_tsum_primes_of_support_subset_prime_powers 📋 Mathlib.NumberTheory.EulerProduct.Basic
  {α : Type u_1} [AddCommGroup α] [UniformSpace α] [IsUniformAddGroup α] [CompleteSpace α] [T0Space α] {f : ℕ → α} (hfm : Summable f) (hf : Function.support f ⊆ {n | IsPrimePow n}) : ∑' (n : ℕ), f n = ∑' (p : Nat.Primes) (k : ℕ), f (↑p ^ (k + 1))
• tsum_primes_pow_eq 📋 Mathlib.NumberTheory.EulerProduct.Basic
  {α : Type u_1} [AddCommGroup α] [UniformSpace α] [IsUniformAddGroup α] [CompleteSpace α] [T0Space α] {f : ℕ → α} (hf : Summable fun n => f ↑n) : ∑' (p : Nat.Primes) (n : ℕ), f (↑p ^ (n + 1)) = ∑' (n : { n // IsPrimePow n }), f ↑n
• tsum_eq_tsum_primes_add_tsum_primes_of_support_subset_prime_powers 📋 Mathlib.NumberTheory.EulerProduct.Basic
  {α : Type u_1} [AddCommGroup α] [UniformSpace α] [IsUniformAddGroup α] [CompleteSpace α] [T0Space α] {f : ℕ → α} (hfm : Summable f) (hf : Function.support f ⊆ {n | IsPrimePow n}) : ∑' (n : ℕ), f n = ∑' (p : Nat.Primes), f ↑p + ∑' (p : Nat.Primes) (k : ℕ), f (↑p ^ (k + 2))
• zeta_eq_tsum_one_div_nat_add_one_cpow 📋 Mathlib.NumberTheory.LSeries.RiemannZeta
  {s : ℂ} (hs : 1 < s.re) : riemannZeta s = ∑' (n : ℕ), 1 / (↑n + 1) ^ s
• ZetaAsymptotics.zeta_limit_aux1 📋 Mathlib.NumberTheory.Harmonic.ZetaAsymp
  {s : ℝ} (hs : 1 < s) : ∑' (n : ℕ), 1 / (↑n + 1) ^ s - 1 / (s - 1) = 1 - s * ZetaAsymptotics.termTSum s
• ZetaAsymptotics.termTSum_of_lt 📋 Mathlib.NumberTheory.Harmonic.ZetaAsymp
  {s : ℝ} (hs : 1 < s) : ZetaAsymptotics.termTSum s = 1 / (s - 1) - 1 / s * ∑' (n : ℕ), 1 / (↑n + 1) ^ s
• ZetaAsymptotics.term_tsum_of_lt 📋 Mathlib.NumberTheory.Harmonic.ZetaAsymp
  {s : ℝ} (hs : 1 < s) : ZetaAsymptotics.termTSum s = 1 / (s - 1) - 1 / s * ∑' (n : ℕ), 1 / (↑n + 1) ^ s
• EisensteinSeries.qExpansion_identity 📋 Mathlib.NumberTheory.ModularForms.EisensteinSeries.QExpansion
  {k : ℕ} (hk : 1 ≤ k) (z : UpperHalfPlane) : ∑' (n : ℤ), 1 / (↑z + ↑n) ^ (k + 1) = (-2 * ↑Real.pi * Complex.I) ^ (k + 1) / ↑k.factorial * ∑' (n : ℕ), ↑n ^ k * Complex.exp (2 * ↑Real.pi * Complex.I * ↑z) ^ n
• EisensteinSeries.qExpansion_identity_pnat 📋 Mathlib.NumberTheory.ModularForms.EisensteinSeries.QExpansion
  {k : ℕ} (hk : 1 ≤ k) (z : UpperHalfPlane) : ∑' (n : ℤ), 1 / (↑z + ↑n) ^ (k + 1) = (-2 * ↑Real.pi * Complex.I) ^ (k + 1) / ↑k.factorial * ∑' (n : ℕ+), ↑↑n ^ k * Complex.exp (2 * ↑Real.pi * Complex.I * ↑z) ^ ↑n
• tsum_eisSummand_eq_tsum_sigma_mul_cexp_pow 📋 Mathlib.NumberTheory.ModularForms.EisensteinSeries.QExpansion
  {k : ℕ} (hk : 3 ≤ k) (hk2 : Even k) (z : UpperHalfPlane) : ∑' (v : Fin 2 → ℤ), EisensteinSeries.eisSummand (↑k) v z = 2 * riemannZeta ↑k + 2 * ((-2 * ↑Real.pi * Complex.I) ^ k / ↑(k - 1).factorial) * ∑' (n : ℕ+), ↑((ArithmeticFunction.sigma (k - 1)) ↑n) * Complex.exp (2 * ↑Real.pi * Complex.I * ↑z) ^ ↑n
• EisensteinSeries.q_expansion_riemannZeta 📋 Mathlib.NumberTheory.ModularForms.EisensteinSeries.QExpansion
  {k : ℕ} (hk : 3 ≤ k) (hk2 : Even k) (z : UpperHalfPlane) : (ModularForm.E hk) z = 1 + (riemannZeta ↑k)⁻¹ * (-2 * ↑Real.pi * Complex.I) ^ k / ↑(k - 1).factorial * ∑' (n : ℕ+), ↑((ArithmeticFunction.sigma (k - 1)) ↑n) * Complex.exp (2 * ↑Real.pi * Complex.I * ↑z) ^ ↑↑n
• EisensteinSeries.tsum_symmetricIco_linear_sub_linear_add_one_eq_zero 📋 Mathlib.NumberTheory.ModularForms.EisensteinSeries.E2.Summable
  (z : UpperHalfPlane) (m : ℤ) : ∑'[SummationFilter.symmetricIco ℤ] (n : ℤ), (1 / (↑m * ↑z + ↑n) - 1 / (↑m * ↑z + ↑n + 1)) = 0
• EisensteinSeries.tsum_tsum_symmetricIco_sub_eq 📋 Mathlib.NumberTheory.ModularForms.EisensteinSeries.E2.Summable
  (z : UpperHalfPlane) : ∑' (m : ℤ), ∑'[SummationFilter.symmetricIco ℤ] (n : ℤ), (1 / (↑m * ↑z + ↑n) - 1 / (↑m * ↑z + ↑n + 1)) = 0
• EisensteinSeries.tsum_symmetricIco_tsum_sub_eq 📋 Mathlib.NumberTheory.ModularForms.EisensteinSeries.E2.Summable
  (z : UpperHalfPlane) : ∑'[SummationFilter.symmetricIco ℤ] (n : ℤ), ∑' (m : ℤ), (1 / (↑m * ↑z + ↑n) - 1 / (↑m * ↑z + ↑n + 1)) = -2 * ↑Real.pi * Complex.I / ↑z
• EisensteinSeries.tendsto_tsum_one_div_linear_sub_succ_eq 📋 Mathlib.NumberTheory.ModularForms.EisensteinSeries.E2.Summable
  (z : UpperHalfPlane) : Filter.Tendsto (fun N => ∑ n ∈ Finset.Ico (-↑↑N) ↑↑N, ∑' (m : ℤ), (1 / (↑m * ↑z + ↑n) - 1 / (↑m * ↑z + ↑n + 1))) Filter.atTop (nhds (-2 * ↑Real.pi * Complex.I / ↑z))
• EisensteinSeries.tsum_symmetricIco_tsum_eq_S_act 📋 Mathlib.NumberTheory.ModularForms.EisensteinSeries.E2.Summable
  (z : UpperHalfPlane) : ∑'[SummationFilter.symmetricIco ℤ] (n : ℤ), ∑' (m : ℤ), 1 / (↑m * ↑z + ↑n) ^ 2 = (↑z ^ 2)⁻¹ * EisensteinSeries.G2 (ModularGroup.S • z)
• EisensteinSeries.tendsto_double_sum_S_act 📋 Mathlib.NumberTheory.ModularForms.EisensteinSeries.E2.Summable
  (z : UpperHalfPlane) : Filter.Tendsto (fun N => ∑' (n : ℤ), ∑ m ∈ Finset.Ico (-↑N) ↑N, 1 / (↑n * ↑z + ↑m) ^ 2) Filter.atTop (nhds ((↑z ^ 2)⁻¹ * EisensteinSeries.G2 (ModularGroup.S • z)))
• ModularForm.tsum_logDeriv_eta_q 📋 Mathlib.NumberTheory.ModularForms.DedekindEta
  (z : ℂ) : ∑' (n : ℕ), logDeriv (fun x => 1 - ModularForm.eta_q n x) z = 2 * ↑Real.pi * Complex.I * ∑' (n : ℕ), (↑n + 1) * -ModularForm.eta_q n z / (1 - ModularForm.eta_q n z)
• jacobiTheta_eq_tsum_nat 📋 Mathlib.NumberTheory.ModularForms.JacobiTheta.OneVariable
  {τ : ℂ} (hτ : 0 < τ.im) : jacobiTheta τ = 1 + 2 * ∑' (n : ℕ), Complex.exp (↑Real.pi * Complex.I * (↑n + 1) ^ 2 * τ)
• ProbabilityTheory.lintegral_exp_mul_sq_norm_le_of_map_rotation_eq_self 📋 Mathlib.Probability.Distributions.Fernique
  {E : Type u_1} [SeminormedAddCommGroup E] [NormedSpace ℝ E] [SecondCountableTopology E] [MeasurableSpace E] [BorelSpace E] {μ : MeasureTheory.Measure E} {a : ℝ} [MeasureTheory.IsProbabilityMeasure μ] (h_rot : MeasureTheory.Measure.map (⇑(ContinuousLinearMap.rotation (-(Real.pi / 4)))) (μ.prod μ) = μ.prod μ) {c : ENNReal} (hc : c ≤ μ {x | ‖x‖ ≤ a}) (hc_gt : 2⁻¹ < c) : ∫⁻ (x : E), ENNReal.ofReal (Real.exp (ProbabilityTheory.Fernique.logRatio c * a⁻¹ ^ 2 * ‖x‖ ^ 2)) ∂μ ≤ ENNReal.ofReal (Real.exp (ProbabilityTheory.Fernique.logRatio c)) + ∑' (n : ℕ), ENNReal.ofReal (Real.exp (-2⁻¹ * Real.log (c / (1 - c)).toReal * 2 ^ n))
• ProbabilityTheory.Fernique.lintegral_exp_mul_sq_norm_le_mul 📋 Mathlib.Probability.Distributions.Fernique
  {E : Type u_1} [SeminormedAddCommGroup E] [NormedSpace ℝ E] [SecondCountableTopology E] [MeasurableSpace E] [BorelSpace E] {μ : MeasureTheory.Measure E} {a : ℝ} [MeasureTheory.IsProbabilityMeasure μ] (h_rot : MeasureTheory.Measure.map (⇑(ContinuousLinearMap.rotation (-(Real.pi / 4)))) (μ.prod μ) = μ.prod μ) (ha_pos : 0 < a) {c' : ENNReal} (hc' : c' ≤ μ {x | ‖x‖ ≤ a}) (hc'_gt : 2⁻¹ < c') : ∫⁻ (x : E), ENNReal.ofReal (Real.exp (ProbabilityTheory.Fernique.logRatio c' * a⁻¹ ^ 2 * ‖x‖ ^ 2)) ∂μ ≤ μ {x | ‖x‖ ≤ a} * (ENNReal.ofReal (Real.exp (ProbabilityTheory.Fernique.logRatio c')) + ∑' (n : ℕ), ENNReal.ofReal (Real.exp (-2⁻¹ * Real.log (c' / (1 - c')).toReal * 2 ^ n)))

About

Loogle searches Lean and Mathlib definitions and theorems.

You can use Loogle from within the Lean4 VSCode language extension using the Loogle command from the command palette. 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:

1. By constant:
   🔍 Real.sin
   finds all lemmas whose statement somehow mentions the sine function.

2. By lemma name substring:
   🔍 "differ"
   finds all lemmas that have "differ" somewhere in their lemma name.

3. 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

4. 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 find tsum_lt_tsum even though the hypothesis f i < g i is not the last.

5. You can filter for definitions vs theorems: Using ⊢ (_ : Type _) finds all definitions which provide data while ⊢ (_ : Prop) finds all theorems (and definitions of proofs).

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. Please review the Lean FRO Terms of Use and Privacy Policy.

This is Loogle revision 9f11169 serving mathlib revision 15fe1e4