Miscellaneous additions to mathlib, to be sorted

• This file can import all ToMathlib files.
• If adding more than a few results, please put them in a more appropriate file in ToMathlib.

Upstreaming status: need to split up this file (according to the lemmas' future location) Most lemmas look ready to be upstreamed; some will require small tweaks.

theorem Real.le_pow_natCeil_logb {b x : ℝ} (hb : 1 < b) (hx : 0 < x) : x ≤ b ^ ⌈logb b x⌉₊

theorem tsum_one_eq' {α : Type u_1} (s : Set α) : ∑' (x : ↑s), 1 = ↑s.encard

theorem ENNReal.tsum_const_eq' {α : Type u_1} (s : Set α) (c : ENNReal) : ∑' (x : ↑s), c = ↑s.encard * c

ENNReal manipulation lemmas

theorem ENNReal.sum_geometric_two_pow_toNNReal {k : ℕ} (hk : k > 0) : ∑' (n : ℕ), 2 ^ (-↑k * ↑n) = ↑(1 / (1 - 1 / 2 ^ k)).toNNReal

theorem ENNReal.sum_geometric_two_pow_neg_one : ∑' (n : ℕ), 2 ^ (-↑n) = 2

theorem ENNReal.sum_geometric_two_pow_neg_two : ∑' (n : ℕ), 2 ^ (-2 * ↑n) = ↑(4 / 3).toNNReal

theorem tsum_geometric_ite_eq_tsum_geometric {k c : ℕ} : (∑' (n : ℕ), if k ≤ n then 2 ^ (-↑c * (↑n - ↑k)) else 0) = ∑' (n : ℕ), 2 ^ (-↑c * ↑n)

theorem ENNReal.toReal_zpow (x : ENNReal) (z : ℤ) : x.toReal ^ z = (x ^ z).toReal

theorem iSup_rpow {ι : Sort u_1} {f : ι → ENNReal} {p : ℝ} (hp : 0 < p) : (⨆ (n : ι), f n) ^ p = ⨆ (n : ι), f n ^ p

@[simp]

theorem ENNReal.nnorm_toReal {x : ENNReal} : ‖x.toReal‖₊ = x.toNNReal

theorem Function.support_rpow_of_pos {α : Type u_1} {f : α → ENNReal} {p : ℝ} (p_pos : 0 < p) : (support fun (x : α) => f x ^ p) = support f

theorem Function.support_rpow_of_neg {α : Type u_1} {f : α → ENNReal} {p : ℝ} (p_neg : p < 0) : (support fun (x : α) => f x ^ p) = {x : α | f x ≠ ⊤}

@[simp]

theorem Function.support_ofNNReal : support ENNReal.ofNNReal = Set.Ioi 0

theorem AEMeasurable.piecewise {α : Type u_1} {β : Type u_2} {s : Set α} {f g : α → β} {m : MeasurableSpace α} {mβ : MeasurableSpace β} {μ : MeasureTheory.Measure α} {d : DecidablePred fun (x : α) => x ∈ s} (hs : MeasurableSet s) (hf : AEMeasurable f μ) (hg : AEMeasurable g μ) : AEMeasurable (s.piecewise f g) μ

theorem AEMeasurable.ite {α : Type u_1} {β : Type u_2} {p : α → Prop} {f g : α → β} {m : MeasurableSpace α} {mβ : MeasurableSpace β} {μ : MeasureTheory.Measure α} {d : DecidablePred p} (hp : MeasurableSet {a : α | p a}) (hf : AEMeasurable f μ) (hg : AEMeasurable g μ) : AEMeasurable (fun (x : α) => if p x then f x else g x) μ

Partitioning an interval

theorem MeasureTheory.lintegral_Ioc_partition {a b : ℕ} {c : ℝ} {f : ℝ → ENNReal} (hc : 0 ≤ c) : ∫⁻ (t : ℝ) in Set.Ioc (↑a * c) (↑b * c), f t = ∑ l ∈ Finset.Ico a b, ∫⁻ (t : ℝ) in Set.Ioc (↑l * c) (↑(l + 1) * c), f t

Averaging

theorem MeasureTheory.laverage_add_left {α : Type u_1} {m0 : MeasurableSpace α} {μ : Measure α} {f g : α → ENNReal} (hf : AEMeasurable f μ) : ⨍⁻ (x : α), f x + g x ∂μ = ⨍⁻ (x : α), f x ∂μ + ⨍⁻ (x : α), g x ∂μ

theorem MeasureTheory.laverage_mono {α : Type u_1} {m0 : MeasurableSpace α} {μ : Measure α} {f g : α → ENNReal} (h : ∀ (x : α), f x ≤ g x) : ⨍⁻ (x : α), f x ∂μ ≤ ⨍⁻ (x : α), g x ∂μ

theorem MeasureTheory.laverage_const_mul {α : Type u_1} {m0 : MeasurableSpace α} {μ : Measure α} {f : α → ENNReal} {c : ENNReal} (hc : c ≠ ⊤) : c * ⨍⁻ (x : α), f x ∂μ = ⨍⁻ (x : α), c * f x ∂μ

theorem MeasureTheory.setLaverage_add_left' {α : Type u_1} {m0 : MeasurableSpace α} {μ : Measure α} {s : Set α} {f g : α → ENNReal} (hf : AEMeasurable f μ) : ⨍⁻ (x : α) in s, f x + g x ∂μ = ⨍⁻ (x : α) in s, f x ∂μ + ⨍⁻ (x : α) in s, g x ∂μ

theorem MeasureTheory.setLaverage_mono' {α : Type u_1} {m0 : MeasurableSpace α} {μ : Measure α} {s : Set α} (hs : MeasurableSet s) {f g : α → ENNReal} (h : ∀ x ∈ s, f x ≤ g x) : ⨍⁻ (x : α) in s, f x ∂μ ≤ ⨍⁻ (x : α) in s, g x ∂μ

theorem MeasureTheory.AEStronglyMeasurable_continuousMap_coe {X : Type u_1} {Y : Type u_2} [TopologicalSpace X] [TopologicalSpace Y] [MeasurableSpace X] [OpensMeasurableSpace X] [TopologicalSpace.PseudoMetrizableSpace Y] [SecondCountableTopologyEither X Y] (f : C(X, Y)) : StronglyMeasurable ⇑f

theorem MeasureTheory.measure_mono_ae' {α : Type u_1} {m : MeasurableSpace α} {μ : Measure α} {A B : Set α} (h : μ (B \ A) = 0) : μ B ≤ μ A

theorem MeasureTheory.AEStronglyMeasurable.ennreal_toReal {α : Type u_1} {m : MeasurableSpace α} {μ : Measure α} {u : α → ENNReal} (hu : AEStronglyMeasurable u μ) : AEStronglyMeasurable (fun (x : α) => (u x).toReal) μ

theorem MeasureTheory.toReal_ofReal_preimage' {s : Set ENNReal} : ENNReal.toReal ⁻¹' ENNReal.ofReal ⁻¹' s = if ⊤ ∈ s ↔ 0 ∈ s then s else if 0 ∈ s then s ∪ {⊤} else s \ {⊤}

theorem MeasureTheory.toReal_ofReal_preimage {s : Set ENNReal} : s = if ⊤ ∈ s ↔ 0 ∈ s then ENNReal.toReal ⁻¹' ENNReal.ofReal ⁻¹' s else if 0 ∈ s then ENNReal.toReal ⁻¹' ENNReal.ofReal ⁻¹' s \ {⊤} else ENNReal.toReal ⁻¹' ENNReal.ofReal ⁻¹' s ∪ {⊤}

theorem MeasureTheory.aestronglyMeasurable_ennreal_toReal_iff {α : Type u_1} {m : MeasurableSpace α} {μ : Measure α} {f : α → ENNReal} (hf : NullMeasurableSet (f ⁻¹' {⊤}) μ) : AEStronglyMeasurable (ENNReal.toReal ∘ f) μ ↔ AEStronglyMeasurable f μ

theorem MeasureTheory.setLaverage_const_le {α : Type u_1} {m : MeasurableSpace α} {μ : Measure α} {s : Set α} {c : ENNReal} : ⨍⁻ (_x : α) in s, c ∂μ ≤ c

theorem MeasureTheory.eLpNormEssSup_lt_top_of_ae_ennnorm_bound {α : Type u_1} {m : MeasurableSpace α} {μ : Measure α} {F : Type u_2} [NormedAddCommGroup F] {f : α → F} {C : ENNReal} (hfC : ∀ᵐ (x : α) ∂μ, ↑‖f x‖₊ ≤ C) : eLpNormEssSup f μ ≤ C

theorem MeasureTheory.restrict_absolutelyContinuous {α : Type u_1} {m : MeasurableSpace α} {μ : Measure α} {s : Set α} : (μ.restrict s).AbsolutelyContinuous μ

theorem MeasureTheory.eLpNormEssSup_toReal_le {α : Type u_1} {m : MeasurableSpace α} {μ : Measure α} {f : α → ENNReal} : eLpNormEssSup (ENNReal.toReal ∘ f) μ ≤ eLpNormEssSup f μ

theorem MeasureTheory.eLpNormEssSup_toReal_eq {α : Type u_1} {m : MeasurableSpace α} {μ : Measure α} {f : α → ENNReal} (hf : ∀ᵐ (x : α) ∂μ, f x ≠ ⊤) : eLpNormEssSup (ENNReal.toReal ∘ f) μ = eLpNormEssSup f μ

theorem MeasureTheory.eLpNorm'_toReal_le {α : Type u_1} {m : MeasurableSpace α} {μ : Measure α} {f : α → ENNReal} {p : ℝ} (hp : 0 ≤ p) : eLpNorm' (ENNReal.toReal ∘ f) p μ ≤ eLpNorm' f p μ

theorem MeasureTheory.eLpNorm'_toReal_eq {α : Type u_1} {m : MeasurableSpace α} {μ : Measure α} {f : α → ENNReal} {p : ℝ} (hf : ∀ᵐ (x : α) ∂μ, f x ≠ ⊤) : eLpNorm' (ENNReal.toReal ∘ f) p μ = eLpNorm' f p μ

theorem MeasureTheory.eLpNorm_toReal_le {α : Type u_1} {m : MeasurableSpace α} {μ : Measure α} {p : ENNReal} {f : α → ENNReal} : eLpNorm (ENNReal.toReal ∘ f) p μ ≤ eLpNorm f p μ

theorem MeasureTheory.eLpNorm_toReal_eq {α : Type u_1} {m : MeasurableSpace α} {μ : Measure α} {p : ENNReal} {f : α → ENNReal} (hf : ∀ᵐ (x : α) ∂μ, f x ≠ ⊤) : eLpNorm (ENNReal.toReal ∘ f) p μ = eLpNorm f p μ

theorem MeasureTheory.sq_eLpNorm_two {α : Type u_1} {m : MeasurableSpace α} {μ : Measure α} {ε : Type u_3} [ENorm ε] [TopologicalSpace ε] {f : α → ε} (hf : AEStronglyMeasurable f μ) : eLpNorm f 2 μ ^ 2 = ∫⁻ (x : α), ‖f x‖ₑ ^ 2 ∂μ

theorem MeasureTheory.eLpNorm_two_eq_enorm_integral_mul_conj {α : Type u_1} {m : MeasurableSpace α} {μ : Measure α} {f : α → ℂ} (lpf : MemLp f 2 μ) : eLpNorm f 2 μ ^ 2 = ‖∫ (x : α), f x * (starRingEnd ℂ) (f x) ∂μ‖ₑ

One of the very few cases where a norm can be moved out of an integral.

theorem MeasureTheory.MemLp.toReal {α : Type u_1} {m : MeasurableSpace α} {μ : Measure α} {p : ENNReal} {f : α → ENNReal} (hf : MemLp f p μ) : MemLp (fun (x : α) => (f x).toReal) p μ

theorem MeasureTheory.Integrable.toReal {α : Type u_1} {m : MeasurableSpace α} {μ : Measure α} {f : α → ENNReal} (hf : Integrable f μ) : Integrable (fun (x : α) => (f x).toReal) μ

EquivalenceOn

structure EquivalenceOn {α : Type u_1} (r : α → α → Prop) (s : Set α) : Prop

An equivalence relation on the set s.

• refl (x : α) : x ∈ s → r x x

  An equivalence relation is reflexive: x ~ x

• symm {x y : α} : x ∈ s → y ∈ s → r x y → r y x

  An equivalence relation is symmetric: x ~ y implies y ~ x

• trans {x y z : α} : x ∈ s → y ∈ s → z ∈ s → r x y → r y z → r x z

  An equivalence relation is transitive: x ~ y and y ~ z implies x ~ z

def EquivalenceOn.setoid {α : Type u_1} {r : α → α → Prop} {s : Set α} (hr : EquivalenceOn r s) : Setoid ↑s

The setoid defined from an equivalence relation on a set.

Equations

• hr.setoid = { r := fun (x y : ↑s) => r ↑x ↑y, iseqv := ⋯ }

theorem EquivalenceOn.exists_rep {α : Type u_1} {r : α → α → Prop} {s : Set α} {hr : EquivalenceOn r s} (x : α) : ∃ (y : α), x ∈ s → y ∈ s ∧ r x y

noncomputable def EquivalenceOn.out {α : Type u_1} {r : α → α → Prop} {s : Set α} (hr : EquivalenceOn r s) (x : α) : α

An arbitrary representative of x w.r.t. the equivalence relation r.

Equations

• hr.out x = if hx : x ∈ s then ↑⟦⟨x, hx⟩⟧.out else x

theorem EquivalenceOn.out_mem {α : Type u_1} {r : α → α → Prop} {s : Set α} {hr : EquivalenceOn r s} {x : α} (hx : x ∈ s) : hr.out x ∈ s

@[simp]

theorem EquivalenceOn.out_mem_iff {α : Type u_1} {r : α → α → Prop} {s : Set α} {hr : EquivalenceOn r s} {x : α} : hr.out x ∈ s ↔ x ∈ s

theorem EquivalenceOn.out_rel {α : Type u_1} {r : α → α → Prop} {s : Set α} {hr : EquivalenceOn r s} {x : α} (hx : x ∈ s) : r (hr.out x) x

theorem EquivalenceOn.rel_out {α : Type u_1} {r : α → α → Prop} {s : Set α} {hr : EquivalenceOn r s} {x : α} (hx : x ∈ s) : r x (hr.out x)

theorem EquivalenceOn.out_inj {α : Type u_1} {r : α → α → Prop} {s : Set α} {hr : EquivalenceOn r s} {x y : α} (hx : x ∈ s) (hy : y ∈ s) (h : r x y) : hr.out x = hr.out y

theorem EquivalenceOn.out_inj' {α : Type u_1} {r : α → α → Prop} {s : Set α} {hr : EquivalenceOn r s} {x y : α} (hx : x ∈ s) (hy : y ∈ s) (h : r (hr.out x) (hr.out y)) : hr.out x = hr.out y

noncomputable def EquivalenceOn.reprs {α : Type u_1} {r : α → α → Prop} {s : Set α} (hr : EquivalenceOn r s) : Set α

The set of representatives of an equivalence relation on a set.

Equations

• hr.reprs = hr.out '' s

theorem EquivalenceOn.out_mem_reprs {α : Type u_1} {r : α → α → Prop} {s : Set α} {hr : EquivalenceOn r s} {x : α} (hx : x ∈ s) : hr.out x ∈ hr.reprs

theorem EquivalenceOn.reprs_subset {α : Type u_1} {r : α → α → Prop} {s : Set α} {hr : EquivalenceOn r s} : hr.reprs ⊆ s

theorem EquivalenceOn.reprs_inj {α : Type u_1} {r : α → α → Prop} {s : Set α} {hr : EquivalenceOn r s} {x y : α} (hx : x ∈ hr.reprs) (hy : y ∈ hr.reprs) (h : r x y) : x = y

theorem Set.Finite.biSup_eq {α : Type u_1} {ι : Type u_2} [CompleteLinearOrder α] {s : Set ι} (hs : s.Finite) (hs' : s.Nonempty) (f : ι → α) : ∃ i ∈ s, ⨆ j ∈ s, f j = f i

theorem Real.self_lt_two_rpow (x : ℝ) : x < 2 ^ x

theorem Complex.measurable_starRingEnd : Measurable ⇑(starRingEnd ℂ)

theorem ENNReal.rpow_le_rpow_of_nonpos {x y : ENNReal} {z : ℝ} (hz : z ≤ 0) (h : x ≤ y) : y ^ z ≤ x ^ z

theorem ENNReal.rpow_lt_rpow_of_neg {x y : ENNReal} {z : ℝ} (hz : z < 0) (h : x < y) : y ^ z < x ^ z

theorem ENNReal.rpow_lt_rpow_iff_of_neg {x y : ENNReal} {z : ℝ} (hz : z < 0) : x ^ z < y ^ z ↔ y < x

theorem ENNReal.rpow_le_rpow_iff_of_neg {x y : ENNReal} {z : ℝ} (hz : z < 0) : x ^ z ≤ y ^ z ↔ y ≤ x

theorem ENNReal.rpow_le_self_of_one_le {x : ENNReal} {y : ℝ} (hx : 1 ≤ x) (hy : y ≤ 1) : x ^ y ≤ x

theorem Set.indicator_eq_indicator' {α : Type u_1} {M : Type u_2} [Zero M] {s : Set α} {f g : α → M} (h : ∀ x ∈ s, f x = g x) : s.indicator f = s.indicator g

theorem Set.indicator_eq_indicator_one_mul {ι : Type u_1} {M : Type u_2} [MulZeroOneClass M] (s : Set ι) (f : ι → M) (x : ι) : s.indicator f x = s.indicator 1 x * f x

theorem Set.conj_indicator {α : Type u_1} {𝕜 : Type u_2} [RCLike 𝕜] {f : α → 𝕜} (s : Set α) (x : α) : (starRingEnd 𝕜) (s.indicator f x) = s.indicator ((starRingEnd (α → 𝕜)) f) x

theorem Set.eq_indicator_one_mul_of_norm_le {X : Type u_1} {F : Set X} {f : X → ℂ} (hf : ∀ (x : X), ‖f x‖ ≤ F.indicator 1 x) : f = F.indicator 1 * f

theorem Set.indicator_one_le_one {X : Type u_1} {G : Set X} (x : X) : G.indicator 1 x ≤ 1

theorem norm_indicator_one_le {α : Type u_1} {E : Type u_2} [SeminormedAddCommGroup E] [One E] [NormOneClass E] {s : Set α} (x : α) : ‖s.indicator 1 x‖ ≤ 1

theorem norm_one_sub_exp_neg_I_mul_ofReal (x : ℝ) : ‖1 - Complex.exp (-(Complex.I * ↑x))‖ = ‖1 - Complex.exp (Complex.I * ↑x)‖

theorem exp_I_mul_eq_one_iff_of_lt_of_lt (x : ℝ) (hx : -(2 * Real.pi) < x) (h'x : x < 2 * Real.pi) : Complex.exp (Complex.I * ↑x) = 1 ↔ x = 0

@[simp]

theorem BddAbove.range_const {ι : Type u_1} {M : Type u_4} [Preorder M] {c : M} : BddAbove (Set.range fun (x : ι) => c)

@[simp]

theorem BddAbove.range_one {ι : Type u_1} {M : Type u_4} [Preorder M] [One M] : BddAbove (Set.range 1)

@[simp]

theorem BddAbove.range_zero {ι : Type u_1} {M : Type u_4} [Preorder M] [Zero M] : BddAbove (Set.range 0)

theorem BddAbove.range_finsetSum {ι : Type u_1} {ι' : Type u_2} {M : Type u_4} [Preorder M] [AddCommMonoid M] [AddLeftMono M] [AddRightMono M] {s : Finset ι} {f : ι → ι' → M} (hf : ∀ i ∈ s, BddAbove (Set.range (f i))) : BddAbove (Set.range fun (x : ι') => ∑ i ∈ s, f i x)

theorem isBounded_iff_bddAbove_norm' {E : Type u_5} [SeminormedCommGroup E] {s : Set E} : Bornology.IsBounded s ↔ BddAbove (norm '' s)

theorem isBounded_iff_bddAbove_norm {E : Type u_5} [SeminormedAddCommGroup E] {s : Set E} : Bornology.IsBounded s ↔ BddAbove (norm '' s)

theorem isBounded_range_iff_bddAbove_norm' {ι : Sort u_5} {E : Type u_6} [SeminormedAddCommGroup E] {f : ι → E} : Bornology.IsBounded (Set.range f) ↔ BddAbove (Set.range fun (x : ι) => ‖f x‖)

theorem isBounded_image_iff_bddAbove_norm' {ι : Type u_5} {E : Type u_6} [SeminormedAddCommGroup E] {f : ι → E} {s : Set ι} : Bornology.IsBounded (f '' s) ↔ BddAbove ((fun (x : ι) => ‖f x‖) '' s)

theorem MeasureTheory.HasCompactSupport.of_support_subset_closedBall {X : Type u_2} {α : Type u_3} [Zero α] {f : X → α} [PseudoMetricSpace X] [ProperSpace X] {x : X} {r : ℝ} (hf : Function.support f ⊆ Metric.closedBall x r) : HasCompactSupport f

theorem MeasureTheory.HasCompactSupport.of_support_subset_isBounded {X : Type u_2} {α : Type u_3} [Zero α] {f : X → α} [PseudoMetricSpace X] [ProperSpace X] {s : Set X} (hs : Bornology.IsBounded s) (hf : Function.support f ⊆ s) : HasCompactSupport f

theorem MeasureTheory.Integrable.indicator_const {X : Type u_2} [MeasureSpace X] {c : ℝ} {s : Set X} (hs : MeasurableSet s) (h2s : volume s < ⊤) : Integrable (s.indicator fun (x : X) => c) volume

theorem MeasureTheory.setIntegral_biUnion_le_sum_setIntegral {X : Type u_4} {ι : Type u_5} [MeasurableSpace X] {f : X → ℝ} (s : Finset ι) {S : ι → Set X} {μ : Measure X} (f_ae_nonneg : ∀ᵐ (x : X) ∂μ.restrict (⋃ i ∈ s, S i), 0 ≤ f x) (int_f : IntegrableOn f (⋃ i ∈ s, S i) μ) : ∫ (x : X) in ⋃ i ∈ s, S i, f x ∂μ ≤ ∑ i ∈ s, ∫ (x : X) in S i, f x ∂μ

theorem ENNReal.lintegral_Lp_smul {α : Type u_1} [MeasurableSpace α] {μ : MeasureTheory.Measure α} {f : α → ENNReal} (hf : AEMeasurable f μ) {p : ℝ} (hp : p > 0) (c : NNReal) : (∫⁻ (x : α), (c • f) x ^ p ∂μ) ^ (1 / p) = c • (∫⁻ (x : α), f x ^ p ∂μ) ^ (1 / p)

theorem ENNReal.ofReal_zpow {p : ℝ} (hp : 0 < p) (n : ℤ) : ENNReal.ofReal (p ^ n) = ENNReal.ofReal p ^ n

@[simp]

theorem prod_attach_insert {α : Type u_1} {β : Type u_2} {s : Finset α} {a : α} [DecidableEq α] [CommMonoid β] {f : ↥(insert a s) → β} (ha : a ∉ s) : ∏ x ∈ (insert a s).attach, f x = f ⟨a, ⋯⟩ * ∏ x ∈ s.attach, f ⟨↑x, ⋯⟩

@[simp]

theorem sum_attach_insert {α : Type u_1} {β : Type u_2} {s : Finset α} {a : α} [DecidableEq α] [AddCommMonoid β] {f : ↥(insert a s) → β} (ha : a ∉ s) : ∑ x ∈ (insert a s).attach, f x = f ⟨a, ⋯⟩ + ∑ x ∈ s.attach, f ⟨↑x, ⋯⟩

theorem Finset.prod_finset_product_filter_right {α : Type u_1} {β : Type u_2} {γ : Type u_3} {s : Finset α} {t : Finset β} {p : α → Prop} {q : α → β → Prop} [DecidablePred p] [DecidableRel q] [DecidablePred fun (r : α × β) => p r.1 ∧ q r.1 r.2] {f : α → β → γ} [CommMonoid γ] : ∏ x ∈ s with p x, ∏ y ∈ t with q x y, f x y = ∏ r ∈ s ×ˢ t with p r.1 ∧ q r.1 r.2, f r.1 r.2

theorem Finset.sum_finset_product_filter_right {α : Type u_1} {β : Type u_2} {γ : Type u_3} {s : Finset α} {t : Finset β} {p : α → Prop} {q : α → β → Prop} [DecidablePred p] [DecidableRel q] [DecidablePred fun (r : α × β) => p r.1 ∧ q r.1 r.2] {f : α → β → γ} [AddCommMonoid γ] : ∑ x ∈ s with p x, ∑ y ∈ t with q x y, f x y = ∑ r ∈ s ×ˢ t with p r.1 ∧ q r.1 r.2, f r.1 r.2

theorem Finset.sum_range_mul_conj_sum_range {α : Type u_1} {s : Finset α} {f : α → ℂ} : ∑ j ∈ s, f j * (starRingEnd ℂ) (f j) + ∑ j ∈ s, ∑ j' ∈ s with j ≠ j', f j * (starRingEnd ℂ) (f j') = (∑ j ∈ s, f j) * (starRingEnd ℂ) (∑ j' ∈ s, f j')

theorem Finset.pow_sum_comm {ι : Type u_1} {R : Type u_2} [Semiring R] {s : Finset ι} {f : ι → R} (hf : ∀ i ∈ s, ∀ j ∈ s, i ≠ j → f i * f j = 0) {n : ℕ} (hn : 1 ≤ n) : (∑ i ∈ s, f i) ^ n = ∑ i ∈ s, f i ^ n

theorem MeasureTheory.sum_sq_eLpNorm_indicator_le_of_pairwiseDisjoint {α : Type u_1} {ι : Type u_2} {F : Type u_3} [MeasurableSpace α] [NormedAddCommGroup F] {μ : Measure α} {s : Finset ι} {f : α → F} {t : ι → Set α} (meast : ∀ (i : ι), MeasurableSet (t i)) (hpd : (↑s).PairwiseDisjoint t) : ∑ i ∈ s, eLpNorm ((t i).indicator f) 2 μ ^ 2 ≤ eLpNorm f 2 μ ^ 2

theorem MeasureTheory.measurable_measure_ball {α : Type u_1} [PseudoMetricSpace α] [SecondCountableTopology α] [MeasurableSpace α] [OpensMeasurableSpace α] {μ : Measure α} [SFinite μ] : Measurable fun (x : α × ℝ) => match x with | (a, r) => μ (Metric.ball a r)