Introduction to Measure Theory, Chapter 0: Notation

A companion to Chapter 0 of the book "An introduction to Measure Theory".

We use existing Mathlib constructions, such as Set.indicator, EuclideanSpace, ENNReal, and tsum to describe the concepts defined in Chapter 0.

@[reducible, inline]

noncomputable abbrev Set.indicator' {X : Type u_1} (E : Set X) (x : X) : ℝ

A version of Set.indicator suitable for this text.

Equations

• E.indicator' = E.indicator fun (x : X) => 1

theorem Set.indicator'_apply {X : Type u_1} (E : Set X) (x : X) [Decidable (x ∈ E)] : E.indicator' x = if x ∈ E then 1 else 0

theorem Set.indicator'_of_mem {X : Type u_1} {E : Set X} {x : X} (h : x ∈ E) : E.indicator' x = 1

theorem Set.indicator'_of_notMem {X : Type u_1} {E : Set X} {x : X} (h : x ∉ E) : E.indicator' x = 0

@[reducible, inline]

noncomputable abbrev EuclideanSpace' (n : ℕ) : Type

A version of EuclideanSpace suitable for this text.

Equations

• EuclideanSpace' n = EuclideanSpace ℝ (Fin n)

@[reducible, inline]

abbrev EuclideanSpace'.equiv_Real : EuclideanSpace' 1 ≃ ℝ

Equations

• One or more equations did not get rendered due to their size.

@[reducible, inline]

abbrev Real.equiv_EuclideanSpace' : ℝ ≃ EuclideanSpace' 1

Equations

• Real.equiv_EuclideanSpace' = EuclideanSpace'.equiv_Real.symm

instance EuclideanSpace'.inst_coeReal : Coe ℝ (EuclideanSpace' 1)

Equations

• EuclideanSpace'.inst_coeReal = { coe := ⇑Real.equiv_EuclideanSpace' }

theorem EuclideanSpace'.norm_eq {n : ℕ} (x : EuclideanSpace' n) : ‖x‖ = √(∑ i : Fin n, x i ^ 2)

theorem EuclideanSpace'.coord_le_norm {d : ℕ} (x : EuclideanSpace' d) (i : Fin d) : |x i| ≤ ‖x‖

Each coordinate of a Euclidean vector is bounded by its norm.

def «term_⬝_» : Lean.TrailingParserDescr

Equations

• «term_⬝_» = Lean.ParserDescr.trailingNode `«term_⬝_» 100 101 (Lean.ParserDescr.binary `andthen (Lean.ParserDescr.symbol " ⬝ ") (Lean.ParserDescr.cat `term 101))

theorem EuclideanSpace'.dot_apply {n : ℕ} (x y : EuclideanSpace' n) : inner ℝ x y = ∑ i : Fin n, x i * y i

def EuclideanSpace'.prod_equiv (d₁ d₂ : ℕ) : EuclideanSpace' (d₁ + d₂) ≃ EuclideanSpace' d₁ × EuclideanSpace' d₂

Equations

• One or more equations did not get rendered due to their size.

def EuclideanSpace'.prod {d₁ d₂ : ℕ} (E₁ : Set (EuclideanSpace' d₁)) (E₂ : Set (EuclideanSpace' d₂)) : Set (EuclideanSpace' (d₁ + d₂))

Equations

• EuclideanSpace'.prod E₁ E₂ = ⇑(EuclideanSpace'.prod_equiv d₁ d₂).symm '' E₁ ×ˢ E₂

theorem ENNReal.upward_continuous {x y : ℕ → ENNReal} (hx : Monotone x) (hy : Monotone y) {x₀ y₀ : ENNReal} (hx_lim : Filter.Tendsto x Filter.atTop (nhds x₀)) (hy_lim : Filter.Tendsto y Filter.atTop (nhds y₀)) : Filter.Tendsto (fun (n : ℕ) => x n * y n) Filter.atTop (nhds (x₀ * y₀))

theorem ENNReal.tsum_of_tsum (x : ℕ → ℕ → ENNReal) : ∑' (p : ℕ × ℕ), x p.1 p.2 = ∑' (n : ℕ) (m : ℕ), x n m

Theorem 0.0.2 (Tonelli's theorem for series)

theorem ENNReal.tsum_of_tsum' (x : ℕ → ℕ → ENNReal) : ∑' (p : ℕ × ℕ), x p.1 p.2 = ∑' (m : ℕ) (n : ℕ), x n m

Theorem 0.0.2

noncomputable instance EReal.inst_posPart : PosPart EReal

Equations

• EReal.inst_posPart = { posPart := fun (x : EReal) => if x ≥ 0 then x else 0 }

noncomputable instance EReal.inst_negPart : NegPart EReal

Equations

• EReal.inst_negPart = { negPart := fun (x : EReal) => if x ≤ 0 then -x else 0 }

noncomputable def Set.choose {A : Type u_1} {E : A → Type u_2} (hE : ∀ (n : A), Nonempty (E n)) (n : A) : E n

Axiom 0.0.4 (Axiom of choice)

Equations

• Set.choose hE n = ⋯.some

noncomputable def Countable.choose {E : ℕ → Type u_1} (hE : ∀ (n : ℕ), Nonempty (E n)) (n : ℕ) : E n

Corollary 0.0.5 (Axiom of countable choice)

Equations

• Countable.choose hE = Set.choose hE