LeanMachineLearning exposition

1.2. ForMathlib.MeasureTheory.Measurable🔗

Measurability lemmas

Module LeanMachineLearning.ForMathlib.MeasureTheory.Measurable contains 5 exposed declarations.

measurable_comp_comap🔗

LemmaMeasureTheory.measurable_comp_comap
Details

No docstring.

🔗theorem
MeasureTheory.measurable_comp_comap.{u_1, u_2, u_3} {α : Type u_1}
  {β : Type u_2} {γ : Type u_3} {mβ : MeasurableSpace β}
  {mγ : MeasurableSpace γ} (f : α → β) {g : β → γ} (hg : Measurable g) :
  Measurable (g ∘ f)
MeasureTheory.measurable_comp_comap.{u_1,
    u_2, u_3}
  {α : Type u_1} {β : Type u_2}
  {γ : Type u_3} {mβ : MeasurableSpace β}
  {mγ : MeasurableSpace γ} (f : α → β)
  {g : β → γ} (hg : Measurable g) :
  Measurable (g ∘ f)

Code

lemma measurable_comp_comap (f : α → β) {g : β → γ} (hg : Measurable g) :
    Measurable[mβ.comap f] (g ∘ f)
Used by (10)

Actions: Source · Open Issue

Proof
by
  rw [measurable_iff_comap_le, ← MeasurableSpace.comap_comp]
  exact MeasurableSpace.comap_mono hg.comap_le

coe_nat_enat🔗

LemmaMeasureTheory.Measurable.coe_nat_enat
Details

No docstring.

🔗theorem
MeasureTheory.Measurable.coe_nat_enat.{u_1} {α : Type u_1}
  {mα : MeasurableSpace α} {f : α → ℕ} (hf : Measurable f) :
  Measurable fun a => ↑(f a)
MeasureTheory.Measurable.coe_nat_enat.{u_1}
  {α : Type u_1} {mα : MeasurableSpace α}
  {f : α → ℕ} (hf : Measurable f) :
  Measurable fun a => ↑(f a)

Code

lemma Measurable.coe_nat_enat {f : α → ℕ} (hf : Measurable f) :
    Measurable (fun a ↦ (f a : ℕ∞))
Used by (1)

Actions: Source · Open Issue

Proof
Measurable.comp (by fun_prop) hf

toNat🔗

LemmaMeasureTheory.Measurable.toNat
Details

No docstring.

🔗theorem
MeasureTheory.Measurable.toNat.{u_1} {α : Type u_1}
  {mα : MeasurableSpace α} {f : α → ℕ∞} (hf : Measurable f) :
  Measurable fun a => ENat.toNat (f a)
MeasureTheory.Measurable.toNat.{u_1}
  {α : Type u_1} {mα : MeasurableSpace α}
  {f : α → ℕ∞} (hf : Measurable f) :
  Measurable fun a => ENat.toNat (f a)

Code

lemma Measurable.toNat {f : α → ℕ∞} (hf : Measurable f) : Measurable (fun a ↦ (f a).toNat)
Used by (1)

Actions: Source · Open Issue

Proof
Measurable.comp (by fun_prop) hf

measurable_sum_range_of_le🔗

LemmaMeasureTheory.measurable_sum_range_of_le
Details

No docstring.

🔗theorem
MeasureTheory.measurable_sum_range_of_le.{u_1} {α : Type u_1}
  {mα : MeasurableSpace α} {f : ℕ → α → ℝ} {g : α → ℕ} {n : ℕ}
  (hg_le : ∀ (a : α), g a ≤ n) (hf : ∀ (i : ℕ), Measurable (f i))
  (hg : Measurable g) :
  Measurable fun a => ∑ i ∈ Finset.range (g a), f i a
MeasureTheory.measurable_sum_range_of_le.{u_1}
  {α : Type u_1} {mα : MeasurableSpace α}
  {f : ℕ → α → ℝ} {g : α → ℕ} {n : ℕ}
  (hg_le : ∀ (a : α), g a ≤ n)
  (hf : ∀ (i : ℕ), Measurable (f i))
  (hg : Measurable g) :
  Measurable fun a =>
    ∑ i ∈ Finset.range (g a), f i a

Code

lemma measurable_sum_range_of_le {f : ℕ → α → ℝ} {g : α → ℕ} {n : ℕ}
    (hg_le : ∀ a, g a ≤ n) (hf : ∀ i, Measurable (f i)) (hg : Measurable g) :
    Measurable (fun a ↦ ∑ i ∈ range (g a), f i a)

Actions: Source · Open Issue

Proof
by
  have h_eq : (fun a ↦ ∑ i ∈ range (g a), f i a)
      = fun a ↦ ∑ i ∈ range (n + 1), if g a = i then ∑ j ∈ range i, f j a else 0 := by
    ext ω
    rw [sum_ite_eq_of_mem]
    grind
  rw [h_eq]
  refine measurable_sum _ fun n hn ↦ ?_
  refine Measurable.ite ?_ (by fun_prop) (by fun_prop)
  exact (measurableSet_singleton _).preimage (by fun_prop)

measurable_sum_Icc_of_le🔗

LemmaMeasureTheory.measurable_sum_Icc_of_le
Details

No docstring.

🔗theorem
MeasureTheory.measurable_sum_Icc_of_le.{u_1} {α : Type u_1}
  {mα : MeasurableSpace α} {f : ℕ → α → ℝ} {g : α → ℕ} {n : ℕ}
  (hg_le : ∀ (a : α), g a ≤ n) (hf : ∀ (i : ℕ), Measurable (f i))
  (hg : Measurable g) :
  Measurable fun a => ∑ i ∈ Finset.Icc 1 (g a), f i a
MeasureTheory.measurable_sum_Icc_of_le.{u_1}
  {α : Type u_1} {mα : MeasurableSpace α}
  {f : ℕ → α → ℝ} {g : α → ℕ} {n : ℕ}
  (hg_le : ∀ (a : α), g a ≤ n)
  (hf : ∀ (i : ℕ), Measurable (f i))
  (hg : Measurable g) :
  Measurable fun a =>
    ∑ i ∈ Finset.Icc 1 (g a), f i a

Code

lemma measurable_sum_Icc_of_le {f : ℕ → α → ℝ} {g : α → ℕ} {n : ℕ}
    (hg_le : ∀ a, g a ≤ n) (hf : ∀ i, Measurable (f i)) (hg : Measurable g) :
    Measurable (fun a ↦ ∑ i ∈ Icc 1 (g a), f i a)

Actions: Source · Open Issue

Proof
by
  have h_eq : (fun a ↦ ∑ i ∈ Icc 1 (g a), f i a)
      = fun a ↦ ∑ i ∈ range (n + 1), if g a = i then ∑ j ∈ Icc 1 i, f j a else 0 := by
    ext ω
    rw [sum_ite_eq_of_mem]
    grind
  rw [h_eq]
  refine measurable_sum _ fun n hn ↦ ?_
  refine Measurable.ite ?_ (by fun_prop) (by fun_prop)
  exact (measurableSet_singleton _).preimage (by fun_prop)
  1. MeasureTheory.measurable_comp_comap
  2. MeasureTheory.Measurable.coe_nat_enat
  3. MeasureTheory.Measurable.toNat
  4. MeasureTheory.measurable_sum_range_of_le
  5. MeasureTheory.measurable_sum_Icc_of_le