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

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.ennreal_toReal {α : Type u_1} {m : MeasurableSpace α} {μ : Measure α} {u : α → ENNReal} (hu : AEStronglyMeasurable u μ) : AEStronglyMeasurable (fun (x : α) => (u x).toReal) μ

theorem MeasureTheory.laverage_mono_ae {α : Type u_1} {m : MeasurableSpace α} {μ : Measure α} {f g : α → ENNReal} (h : ∀ᵐ (a : α) ∂μ, f a ≤ g a) : ⨍⁻ (a : α), f a ∂μ ≤ ⨍⁻ (a : α), g a ∂μ

theorem MeasureTheory.setLAverage_mono_ae {α : Type u_1} {m : MeasurableSpace α} {μ : Measure α} {s : Set α} {f g : α → ENNReal} (h : ∀ᵐ (a : α) ∂μ, f a ≤ g a) : ⨍⁻ (a : α) in s, f a ∂μ ≤ ⨍⁻ (a : α) in s, g a ∂μ

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

@[simp]

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

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

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

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 Nat.ceil_lt_add_one_of_nonneg {x : ℝ} (hx : 0 ≤ x) : ↑⌈x⌉₊ < x + 1

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 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_exp_I_mul_ofReal (x : ℝ) : ‖Complex.exp (Complex.I * ↑x)‖ = 1

theorem enorm_exp_I_mul_ofReal (x : ℝ) : ‖Complex.exp (Complex.I * ↑x)‖ₑ = 1

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

theorem norm_exp_I_mul_ofReal_sub_one {x : ℝ} : ‖Complex.exp (Complex.I * ↑x) - 1‖ = ‖2 * Real.sin (x / 2)‖

theorem norm_exp_I_mul_ofReal_sub_one_le {x : ℝ} : ‖Complex.exp (Complex.I * ↑x) - 1‖ ≤ ‖x‖

theorem enorm_exp_I_mul_ofReal_sub_one_le {x : ℝ} : ‖Complex.exp (Complex.I * ↑x) - 1‖ₑ ≤ ‖x‖ₑ

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 MeasureTheory.average_smul_const {X : Type u_4} {E : Type u_5} [MeasurableSpace X] {μ : Measure X} [NormedAddCommGroup E] [NormedSpace ℝ E] {𝕜 : Type u_6} [RCLike 𝕜] [NormedSpace 𝕜 E] [CompleteSpace E] (f : X → 𝕜) (c : E) : ⨍ (x : X), f x • c ∂μ = (⨍ (x : X), f x ∂μ) • c

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