LeanMachineLearning exposition

MeasureTheory.measurable_sum_Icc_of_le🔗

Minimal Lean file

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)