LeanMachineLearning

Bandits.ArrayModel.indepFun_fst_add_one_auxπŸ”—

Lemma

No docstring.

πŸ”—theorem
Bandits.ArrayModel.indepFun_fst_add_one_aux.{u_1, u_2} {𝓐 : Type u_1}
  {R : Type u_2} {m𝓐 : MeasurableSpace 𝓐} {mR : MeasurableSpace R}
  (Ξ½ : ProbabilityTheory.Kernel 𝓐 R)
  [ProbabilityTheory.IsMarkovKernel Ξ½] (n : β„•) :
  ProbabilityTheory.IndepFun (fun Ο‰ => Prod.fst Ο‰ (n + 1))
    (fun Ο‰ => (fun i => Prod.fst Ο‰ ↑i, Prod.snd Ο‰)) (arrayMeasure Ξ½)
Bandits.ArrayModel.indepFun_fst_add_one_aux.{u_1,
    u_2}
  {𝓐 : Type u_1} {R : Type u_2}
  {m𝓐 : MeasurableSpace 𝓐}
  {mR : MeasurableSpace R}
  (Ξ½ : ProbabilityTheory.Kernel 𝓐 R)
  [ProbabilityTheory.IsMarkovKernel Ξ½]
  (n : β„•) :
  ProbabilityTheory.IndepFun
    (fun Ο‰ => Prod.fst Ο‰ (n + 1))
    (fun Ο‰ =>
      (fun i => Prod.fst Ο‰ ↑i,
        Prod.snd Ο‰))
    (arrayMeasure Ξ½)

Code

lemma indepFun_fst_add_one_aux (Ξ½ : Kernel 𝓐 R) [IsMarkovKernel Ξ½] (n : β„•) :
    (fun Ο‰ ↦ Ο‰.1 (n + 1)) βŸ‚α΅’[arrayMeasure Ξ½] (fun Ο‰ ↦ (fun (i : Iic n) ↦ Ο‰.1 i, Ο‰.2))
Proof
by
  let μ₁ : Measure (β„• β†’ I) := Measure.infinitePi fun _ ↦ volume
  let ΞΌβ‚‚ : Measure (β„• β†’ 𝓐 β†’ R) := streamMeasure Ξ½
  -- Coordinates of μ₁ are independent
  have h_indep : iIndepFun (fun i (Ο‰ : β„• β†’ I) ↦ Ο‰ i) μ₁ :=
    iIndepFun_infinitePi (fun _ ↦ measurable_id)
  have h_indep_n : IndepFun (fun Ο‰ ↦ Ο‰ (n + 1)) (fun Ο‰ ↦ fun i : Iic n ↦ Ο‰ i) μ₁ := by
    have h := h_indep.indepFun_finsetβ‚€ {n + 1} (Iic n) (by simp)
      (fun i ↦ (measurable_pi_apply i).aemeasurable)
    convert h.comp (measurable_pi_apply ⟨n + 1, by simp⟩) measurable_id using 1
    Β· rfl
    Β· rfl
  rw [indepFun_iff_measure_inter_preimage_eq_mul]
  intro s t hs ht
  let X : (β„• β†’ I) Γ— (β„• β†’ 𝓐 β†’ R) β†’ I := fun Ο‰ ↦ Ο‰.1 (n + 1)
  let Y : (β„• β†’ I) Γ— (β„• β†’ 𝓐 β†’ R) β†’ (Iic n β†’ I) Γ— (β„• β†’ 𝓐 β†’ R) := fun Ο‰ ↦ (fun i ↦ Ο‰.1 i, Ο‰.2)
  change (μ₁.prod ΞΌβ‚‚) (X ⁻¹' s ∩ Y ⁻¹' t) = (μ₁.prod ΞΌβ‚‚) (X ⁻¹' s) * (μ₁.prod ΞΌβ‚‚) (Y ⁻¹' t)
  -- Rewrite using Fubini
  rw [Measure.prod_apply (hs.preimage (by fun_prop : Measurable X)),
    Measure.prod_apply (ht.preimage (by fun_prop : Measurable Y)),
    Measure.prod_apply ((hs.preimage (by fun_prop : Measurable X)).inter
      (ht.preimage (by fun_prop : Measurable Y)))]
  -- Compute fibers
  have hX_fst ω₁ : ΞΌβ‚‚ (Prod.mk ω₁ ⁻¹' (X ⁻¹' s)) = s.indicator 1 (ω₁ (n + 1)) := by
    simp only [X, Set.preimage_preimage]
    by_cases h : ω₁ (n + 1) ∈ s <;> simp [h]
  have hY_fst ω₁ : ΞΌβ‚‚ (Prod.mk ω₁ ⁻¹' (Y ⁻¹' t)) = ΞΌβ‚‚ {y | ((fun i : Iic n ↦ ω₁ i), y) ∈ t} := rfl
  have hXY ω₁ : ΞΌβ‚‚ (Prod.mk ω₁ ⁻¹' (X ⁻¹' s ∩ Y ⁻¹' t)) =
      s.indicator 1 (ω₁ (n + 1)) * ΞΌβ‚‚ {y | ((fun i : Iic n ↦ ω₁ i), y) ∈ t} := by
    simp only [X, Y, Set.preimage_inter, Set.preimage_preimage]
    by_cases h : ω₁ (n + 1) ∈ s
    Β· simp [h]
      congr
    Β· simp [h]
  simp_rw [hY_fst, hX_fst, hXY]
  -- Factor the integral using independence
  let g : (Iic n β†’ I) β†’ ENNReal := fun x ↦ ΞΌβ‚‚ {y | (x, y) ∈ t}
  have hg_meas : Measurable g := measurable_measure_prodMk_left ht
  have hf_meas : Measurable (fun ω₁ : β„• β†’ I ↦ s.indicator (1 : I β†’ ENNReal) (ω₁ (n + 1))) :=
    (measurable_one.indicator hs).comp (measurable_pi_apply _)
  have hindep_fg : IndepFun (fun ω₁ ↦ s.indicator (1 : I β†’ ENNReal) (ω₁ (n + 1)))
      (fun ω₁ ↦ g (fun i ↦ ω₁ i)) μ₁ :=
    h_indep_n.comp (measurable_one.indicator hs) hg_meas
  have h_eq (ω₁ : β„• β†’ I) : ΞΌβ‚‚ {y | ((fun i : Iic n ↦ ω₁ i), y) ∈ t} = g (fun i ↦ ω₁ i) := rfl
  simp_rw [h_eq]
  exact lintegral_mul_eq_lintegral_mul_lintegral_of_indepFun hf_meas (by fun_prop) hindep_fg

Actions: Source Β· Open Issue

Meaning last changed in v4.34.0-rc2-1-g439785b (2026-08-23), the 5th recorded change.

Self-contained, with its dependencies inlined and proofs replaced by sorry: download the raw file Β· open it in the Lean web editor.

Dependency graph

Audit surface: 4 project declarations, 54 external constants

βœ“ Proved: no sorry anywhere in its closure

This is the tool's own reading of one build's recorded axioms, and it is not robust against an author who wants it to pass. Checking meant to be relied on should go through Comparator, which replays the proof through the kernel from an export against an explicit list of permitted axioms.