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

theorem MeasureTheory.laverage_mono_ae {α : Type u_1} {m : MeasurableSpace α} {μ : MeasureTheory.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 α} {μ : MeasureTheory.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 α} {μ : MeasureTheory.Measure α} {s : Set α} {c : ENNReal} : ⨍⁻ (_x : α) in s, c ∂μ ≤ c

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

@[simp]

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

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

theorem HasCompactSupport.memℒp_of_isBounded {E : Type u_1} {X : Type u_2} [NormedAddCommGroup E] [TopologicalSpace X] [MeasurableSpace X] {μ : MeasureTheory.Measure X} [MeasureTheory.IsFiniteMeasureOnCompacts μ] {f : X → E} (hf : HasCompactSupport f) (h2f : Bornology.IsBounded (Set.range f)) (h3f : MeasureTheory.AEStronglyMeasurable f μ) {p : ENNReal} : MeasureTheory.Memℒp f p μ

EquivalenceOn

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

An equivalence relation on the set s.

• refl : ∀ 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