theorem Metric.dense_iff_iUnion_ball {X : Type u_1} [PseudoMetricSpace X] (s : Set X) : Dense s ↔ ∀ r > 0, ⋃ c ∈ s, Metric.ball c r = Set.univ

theorem PseudoMetricSpace.dist_eq_of_dist_zero {X : Type u_1} [PseudoMetricSpace X] (x : X) {y : X} {y' : X} (hyy' : dist y y' = 0) : dist x y = dist x y'

theorem IsTop.isMax_iff {α : Type u_1} [PartialOrder α] {i : α} {j : α} (h : IsTop i) : IsMax j ↔ j = i

theorem Int.floor_le_iff (c : ℝ) (z : ℤ) : ⌊c⌋ ≤ z ↔ c < ↑z + 1

theorem Int.le_ceil_iff (c : ℝ) (z : ℤ) : z ≤ ⌈c⌉ ↔ ↑z - 1 < c

theorem Int.Icc_of_eq_sub_1 {a : ℤ} {b : ℤ} (h : a = b - 1) : Finset.Icc a b = {a, b}

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)

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 : α → ENNReal} {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 : α → ENNReal} {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 : α → ENNReal} {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 : α → ENNReal} {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 : α → ENNReal} {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 : α → ENNReal} {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

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

theorem EquivalenceOn.refl {α : Type u_1} {r : α → α → Prop} {s : Set α} (self : EquivalenceOn r s) (x : α) : x ∈ s → r x x

An equivalence relation is reflexive: x ~ x

theorem EquivalenceOn.symm {α : Type u_1} {r : α → α → Prop} {s : Set α} (self : EquivalenceOn r s) {x : α} {y : α} : x ∈ s → y ∈ s → r x y → r y x

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

theorem EquivalenceOn.trans {α : Type u_1} {r : α → α → Prop} {s : Set α} (self : EquivalenceOn r s) {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

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.

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