LeanMachineLearning

Bandits.ArrayModel.indepFun_snd_apply_auxπŸ”—

Lemma

No docstring.

πŸ”—theorem
Bandits.ArrayModel.indepFun_snd_apply_aux.{u_1, u_2} {𝓐 : Type u_1}
  {R : Type u_2} {m𝓐 : MeasurableSpace 𝓐} {mR : MeasurableSpace R}
  [DecidableEq 𝓐] [Nonempty R] (Ξ½ : ProbabilityTheory.Kernel 𝓐 R)
  [ProbabilityTheory.IsMarkovKernel Ξ½] (a : 𝓐) (m : β„•) :
  ProbabilityTheory.IndepFun (fun Ο‰ => Prod.snd Ο‰ m a)
    (fun Ο‰ =>
      (Prod.fst Ο‰, fun k b =>
        if b = a then
          if m β‰  0 then Prod.snd Ο‰ (min k (m - 1)) b
          else Nonempty.some β‹―
        else Prod.snd Ο‰ k b))
    (arrayMeasure Ξ½)
Bandits.ArrayModel.indepFun_snd_apply_aux.{u_1,
    u_2}
  {𝓐 : Type u_1} {R : Type u_2}
  {m𝓐 : MeasurableSpace 𝓐}
  {mR : MeasurableSpace R} [DecidableEq 𝓐]
  [Nonempty R]
  (Ξ½ : ProbabilityTheory.Kernel 𝓐 R)
  [ProbabilityTheory.IsMarkovKernel Ξ½]
  (a : 𝓐) (m : β„•) :
  ProbabilityTheory.IndepFun
    (fun Ο‰ => Prod.snd Ο‰ m a)
    (fun Ο‰ =>
      (Prod.fst Ο‰, fun k b =>
        if b = a then
          if m β‰  0 then
            Prod.snd Ο‰ (min k (m - 1)) b
          else Nonempty.some β‹―
        else Prod.snd Ο‰ k b))
    (arrayMeasure Ξ½)

Code

lemma indepFun_snd_apply_aux (Ξ½ : Kernel 𝓐 R) [IsMarkovKernel Ξ½] (a : 𝓐) (m : β„•) :
    (fun Ο‰ ↦ Ο‰.2 m a) βŸ‚α΅’[arrayMeasure Ξ½]
      (fun Ο‰ ↦ (Ο‰.1, fun k b ↦ if b = a then if m β‰  0 then Ο‰.2 (min k (m - 1)) b
        else Nonempty.some inferInstance else Ο‰.2 k b))
Proof
by
  unfold arrayMeasure
  let μ₁ : Measure (β„• β†’ I) := Measure.infinitePi fun _ ↦ volume
  let ΞΌβ‚‚ : Measure (β„• β†’ 𝓐 β†’ R) := Measure.infinitePi fun _ ↦ Measure.infinitePi Ξ½
  -- Independence within ΞΌβ‚‚: coordinates Ο‰ i are independent
  have h_indepβ‚‚ : iIndepFun (fun i (Ο‰ : β„• β†’ 𝓐 β†’ R) ↦ Ο‰ i) ΞΌβ‚‚ :=
    iIndepFun_infinitePi (fun _ ↦ measurable_id)
  -- Independence within each infinitePi Ξ½: coordinates f b are independent
  have h_indep_inner : iIndepFun (fun (b : 𝓐) (f : 𝓐 β†’ R) ↦ f b) (Measure.infinitePi Ξ½) :=
    iIndepFun_infinitePi (fun _ ↦ measurable_id)
  rw [indepFun_iff_measure_inter_preimage_eq_mul]
  intro s t hs ht
  let X : (β„• β†’ I) Γ— (β„• β†’ 𝓐 β†’ R) β†’ R := fun Ο‰ ↦ Ο‰.2 m a
  let Y : (β„• β†’ I) Γ— (β„• β†’ 𝓐 β†’ R) β†’ (β„• β†’ I) Γ— (β„• β†’ 𝓐 β†’ R) :=
    fun Ο‰ ↦ (Ο‰.1, fun k b ↦ if b = a then if m β‰  0 then Ο‰.2 (min k (m - 1)) b
      else Nonempty.some inferInstance else Ο‰.2 k b)
  have hX_meas : Measurable X :=
    (measurable_pi_apply a).comp ((measurable_pi_apply m).comp measurable_snd)
  have hY_meas : Measurable Y := by
    change Measurable (fun Ο‰ : (β„• β†’ I) Γ— (β„• β†’ 𝓐 β†’ R) ↦
      (Ο‰.1, fun k b ↦ if b = a then if m β‰  0 then Ο‰.2 (min k (m - 1)) b
        else Nonempty.some inferInstance else Ο‰.2 k b))
    refine Measurable.prod measurable_fst ?_
    refine measurable_pi_lambda _ (fun k ↦ ?_)
    refine measurable_pi_lambda _ (fun b ↦ ?_)
    by_cases hb : b = a
    Β· simp only [hb, ↓reduceIte]
      by_cases hm : m β‰  0
      Β· simp only [ne_eq, hm, not_false_eq_true, ↓reduceIte]
        exact (measurable_pi_apply a).comp
          ((measurable_pi_apply (min k (m - 1))).comp measurable_snd)
      Β· simp only [hm, ↓reduceIte]
        exact measurable_const
    Β· simp only [hb, ↓reduceIte]
      exact (measurable_pi_apply b).comp ((measurable_pi_apply k).comp measurable_snd)
  change (μ₁.prod ΞΌβ‚‚) (X ⁻¹' s ∩ Y ⁻¹' t) = (μ₁.prod ΞΌβ‚‚) (X ⁻¹' s) * (μ₁.prod ΞΌβ‚‚) (Y ⁻¹' t)
  -- Use Fubini on μ₁.prod ΞΌβ‚‚
  rw [Measure.prod_apply (hs.preimage hX_meas),
    Measure.prod_apply (ht.preimage hY_meas),
    Measure.prod_apply ((hs.preimage hX_meas).inter (ht.preimage hY_meas))]
  -- X only depends on Ο‰β‚‚, so its fiber is constant in ω₁
  have hX_fst : βˆ€ ω₁, ΞΌβ‚‚ (Prod.mk ω₁ ⁻¹' (X ⁻¹' s)) = ΞΌβ‚‚ ((fun Ο‰β‚‚ ↦ Ο‰β‚‚ m a) ⁻¹' s) := fun _ ↦ rfl
  simp_rw [hX_fst]
  -- The LHS integral: fiber of X ∩ Y at ω₁
  -- Key: X depends only on Ο‰β‚‚ m a, while Y's dependence on Ο‰β‚‚ avoids (m, a)
  -- Define the "truncation" map on Ο‰β‚‚
  let trunc : (β„• β†’ 𝓐 β†’ R) β†’ (β„• β†’ 𝓐 β†’ R) :=
    fun Ο‰β‚‚ k b ↦ if b = a then if m β‰  0 then Ο‰β‚‚ (min k (m - 1)) b
      else Nonempty.some inferInstance else Ο‰β‚‚ k b
  -- The fiber of Y at ω₁ only depends on trunc(Ο‰β‚‚)
  have hY_fiber : βˆ€ ω₁, Prod.mk ω₁ ⁻¹' (Y ⁻¹' t) = (fun Ο‰β‚‚ ↦ (ω₁, trunc Ο‰β‚‚)) ⁻¹' t := fun _ ↦ rfl
  -- The fiber of X ∩ Y factors
  have hXY_fiber : βˆ€ ω₁, Prod.mk ω₁ ⁻¹' (X ⁻¹' s ∩ Y ⁻¹' t) =
      ((fun Ο‰β‚‚ ↦ Ο‰β‚‚ m a) ⁻¹' s) ∩ ((fun Ο‰β‚‚ ↦ (ω₁, trunc Ο‰β‚‚)) ⁻¹' t) := fun _ ↦ rfl
  simp_rw [hXY_fiber, hY_fiber]
  -- Now we use independence in ΞΌβ‚‚: (Ο‰β‚‚ m a) is independent of (trunc Ο‰β‚‚)
  -- because trunc only uses indices (k, a) with k < m, and (k, b) with b β‰  a
  have h_trunc_meas : Measurable trunc := by
    refine measurable_pi_lambda _ (fun k ↦ ?_)
    refine measurable_pi_lambda _ (fun b ↦ ?_)
    simp only [trunc]
    by_cases hb : b = a
    Β· simp only [hb, ↓reduceIte]
      by_cases hm : m = 0
      Β· simp only [hm]
        exact measurable_const
      Β· simp only [ne_eq, hm, not_false_eq_true, ↓reduceIte]
        exact (measurable_pi_apply a).comp (measurable_pi_apply (min k (m - 1)))
    Β· simp only [hb, ↓reduceIte]
      exact (measurable_pi_apply b).comp (measurable_pi_apply k)
  -- Key independence: (Ο‰β‚‚ m a) βŸ‚ trunc because trunc only uses coordinates β‰  (m, a)
  have h_indep_trunc : IndepFun (fun Ο‰β‚‚ ↦ Ο‰β‚‚ m a) trunc ΞΌβ‚‚ := by
    -- Factor trunc through proj which extracts the relevant coordinates
    let proj : (β„• β†’ 𝓐 β†’ R) β†’ ((β„• β†’ R) Γ— (β„• β†’ {b : 𝓐 // b β‰  a} β†’ R)) := fun Ο‰β‚‚ ↦
      (fun k ↦ if m β‰  0 then Ο‰β‚‚ (min k (m - 1)) a else Nonempty.some inferInstance,
      fun k ⟨b, _⟩ ↦ Ο‰β‚‚ k b)
    have h_trunc_proj : βˆ€ Ο‰β‚‚, trunc Ο‰β‚‚ = (fun p k b ↦
        if h : b = a then if m β‰  0 then p.1 k
          else Nonempty.some inferInstance else p.2 k ⟨b, h⟩) (proj Ο‰β‚‚) := by
      intro Ο‰β‚‚; ext k b; simp only [trunc, proj]; by_cases hb : b = a <;> simp [hb]; grind
    have h_proj_meas : Measurable proj := by
      refine Measurable.prod ?_ ?_
      Β· refine measurable_pi_lambda _ fun k ↦ ?_
        by_cases hm : m β‰  0
        Β· simp only [proj, ne_eq, hm, not_false_eq_true, ↓reduceIte]
          exact (measurable_pi_apply a).comp (measurable_pi_apply (min k (m - 1)))
        Β· simp [proj, hm]
      Β· exact measurable_pi_lambda _ (fun k ↦ measurable_pi_lambda _ (fun ⟨b, _⟩ ↦
          (measurable_pi_apply b).comp (measurable_pi_apply k)))
    have h_g_meas : Measurable (fun p : (β„• β†’ R) Γ— (β„• β†’ {b : 𝓐 // b β‰  a} β†’ R) ↦
        (fun k b ↦ if h : b = a then if m β‰  0 then p.1 k else Nonempty.some inferInstance
          else p.2 k ⟨b, h⟩)) := by
      refine measurable_pi_lambda _ (fun k ↦ measurable_pi_lambda _ (fun b ↦ ?_))
      by_cases hb : b = a
      Β· simp only [hb, ↓reduceDIte]
        by_cases hm : m β‰  0
        Β· simp only [ne_eq, hm, not_false_eq_true]
          exact (measurable_pi_apply k).comp measurable_fst
        Β· simp [hm]
      Β· simp only [hb, ↓reduceDIte]
        exact (measurable_pi_apply (⟨b, hb⟩ : {b : 𝓐 // b β‰  a})).comp
          ((measurable_pi_apply k).comp measurable_snd)
    -- Show (Ο‰β‚‚ m a) βŸ‚ proj: proj uses coordinates disjoint from (m, a)
    have h_indep_proj : IndepFun (fun Ο‰β‚‚ ↦ Ο‰β‚‚ m a) proj ΞΌβ‚‚ := by
      have h_row_bound (hm : m β‰  0) : βˆ€ k, min k (m - 1) < m := by
        intro k
        calc min k (m - 1) ≀ m - 1 := Nat.min_le_right k (m - 1)
          _ < m := Nat.sub_lt (by grind) Nat.one_pos
      rw [indepFun_iff_measure_inter_preimage_eq_mul]
      intro s t' hs ht'
      -- rows_lt_m extracts column a at rows < m, other_cols extracts columns β‰  a
      let rows_lt_m : (β„• β†’ 𝓐 β†’ R) β†’ (Iio m β†’ R) := fun Ο‰β‚‚ ⟨j, _⟩ ↦ Ο‰β‚‚ j a
      let other_cols : (β„• β†’ 𝓐 β†’ R) β†’ (β„• β†’ {b : 𝓐 // b β‰  a} β†’ R) := fun Ο‰β‚‚ k ⟨b, _⟩ ↦ Ο‰β‚‚ k b
      have h_proj_factor : βˆ€ Ο‰β‚‚, proj Ο‰β‚‚ =
          ((fun r k ↦ if hm : m β‰  0 then r ⟨min k (m - 1), Finset.mem_Iio.mpr (h_row_bound hm k)⟩
            else Nonempty.some inferInstance) (rows_lt_m Ο‰β‚‚),
           other_cols Ο‰β‚‚) := by
        intro Ο‰β‚‚; ext1
        Β· ext k
          by_cases hm : m β‰  0
          Β· simp [proj, rows_lt_m, hm]
          Β· simp [proj, hm]
        Β· rfl
      -- Use iIndepFun structure of the doubly-indexed infinite product
      have h_iindep : iIndepFun (fun (p : β„• Γ— 𝓐) Ο‰ ↦ Ο‰ p.1 p.2) ΞΌβ‚‚ :=
        iIndepFun_uncurry_infinitePi' (X := fun _ _ ↦ id) (fun _ ↦ Ξ½) (by fun_prop)
      have h_rows_meas : Measurable rows_lt_m :=
        measurable_pi_lambda _ (fun ⟨j, _⟩ ↦ (measurable_pi_apply a).comp (measurable_pi_apply j))
      have h_other_meas : Measurable other_cols :=
        measurable_pi_lambda _ (fun k ↦ measurable_pi_lambda _ (fun ⟨b, _⟩ ↦
          (measurable_pi_apply b).comp (measurable_pi_apply k)))
      -- Show (Ο‰β‚‚ m a) βŸ‚ (rows_lt_m, other_cols) via indep_iSup_of_disjoint
      have h_indep_combined : IndepFun (fun Ο‰β‚‚ ↦ Ο‰β‚‚ m a)
          (fun Ο‰β‚‚ ↦ (rows_lt_m Ο‰β‚‚, other_cols Ο‰β‚‚)) ΞΌβ‚‚ := by
        rw [IndepFun_iff_Indep]
        have h_comap_le : (MeasurableSpace.pi.prod MeasurableSpace.pi).comap
            (fun Ο‰β‚‚ ↦ (rows_lt_m Ο‰β‚‚, other_cols Ο‰β‚‚)) ≀
            ⨆ (p : {p : β„• Γ— 𝓐 // p β‰  (m, a)}), mR.comap (fun Ο‰ ↦ Ο‰ p.val.1 p.val.2) := by
          rw [MeasurableSpace.comap_prodMk]
          refine sup_le ?_ ?_
          Β· rw [MeasurableSpace.comap_pi]
            refine iSup_le (fun ⟨j, hj⟩ ↦ ?_)
            have h_ne : (j, a) β‰  (m, a) := fun h ↦ (Finset.mem_Iio.mp hj).ne (Prod.mk.inj h).1
            exact le_iSup_of_le ⟨(j, a), h_ne⟩ le_rfl
          Β· rw [MeasurableSpace.comap_pi]
            refine iSup_le (fun k ↦ ?_)
            rw [MeasurableSpace.comap_pi]
            refine iSup_le (fun ⟨b, hb⟩ ↦ ?_)
            have h_ne : (k, b) β‰  (m, a) := fun h ↦ hb (Prod.mk.inj h).2
            exact le_iSup_of_le ⟨(k, b), h_ne⟩ le_rfl
        refine indep_of_indep_of_le_right ?_ h_comap_le
        have h_disjoint : Disjoint ({(m, a)} : Set (β„• Γ— 𝓐)) {p | p β‰  (m, a)} := by simp
        have h_le : βˆ€ p : β„• Γ— 𝓐, mR.comap (fun Ο‰ : β„• β†’ 𝓐 β†’ R ↦ Ο‰ p.1 p.2) ≀
            MeasurableSpace.pi (m := fun _ ↦ MeasurableSpace.pi) := fun p ↦
          Measurable.comap_le ((measurable_pi_apply p.2).comp (measurable_pi_apply p.1))
        have h_iindep' : iIndep (fun p : β„• Γ— 𝓐 ↦ mR.comap (fun Ο‰ : β„• β†’ 𝓐 β†’ R ↦ Ο‰ p.1 p.2)) ΞΌβ‚‚ :=
          h_iindep.iIndep
        have h_indep := indep_iSup_of_disjoint h_le h_iindep' h_disjoint
        convert h_indep using 2
        Β· simp only [Set.mem_singleton_iff, iSup_iSup_eq_left]
        Β· simp only [ne_eq, Set.mem_ofPred_eq, iSup_subtype']
      have h_proj_preimage : proj ⁻¹' t' = (fun Ο‰β‚‚ ↦ (rows_lt_m Ο‰β‚‚, other_cols Ο‰β‚‚)) ⁻¹'
          {p | ((fun r k ↦ if hm : m β‰  0 then
            r ⟨min k (m - 1), Finset.mem_Iio.mpr (h_row_bound hm k)⟩
            else Nonempty.some inferInstance) p.1, p.2) ∈ t'}
          := by ext Ο‰β‚‚; simp only [Set.mem_preimage, Set.mem_ofPred_eq, h_proj_factor]
      rw [indepFun_iff_measure_inter_preimage_eq_mul] at h_indep_combined
      rw [h_proj_preimage]
      let T : Set ((Iio m β†’ R) Γ— (β„• β†’ {b : 𝓐 // b β‰  a} β†’ R)) :=
        {p | ((fun r k ↦ if hm : m β‰  0 then
          r ⟨min k (m - 1), Finset.mem_Iio.mpr (h_row_bound hm k)⟩
          else Nonempty.some inferInstance) p.1, p.2) ∈ t'}
      have hT_meas : MeasurableSet T := by
        refine ht'.preimage (Measurable.prod ?_ measurable_snd)
        refine measurable_pi_lambda _ (fun k ↦ ?_)
        by_cases hm : m β‰  0
        Β· simp only [ne_eq, hm, not_false_eq_true, ↓reduceDIte]
          exact (measurable_pi_apply (⟨min k (m - 1), Finset.mem_Iio.mpr (h_row_bound hm k)⟩ :
            Iio m)).comp measurable_fst
        Β· simp [hm]
      change ΞΌβ‚‚ ((fun Ο‰β‚‚ ↦ Ο‰β‚‚ m a) ⁻¹' s ∩ (fun Ο‰β‚‚ ↦ (rows_lt_m Ο‰β‚‚, other_cols Ο‰β‚‚)) ⁻¹' T) =
        ΞΌβ‚‚ ((fun Ο‰β‚‚ ↦ Ο‰β‚‚ m a) ⁻¹' s) *
        ΞΌβ‚‚ ((fun Ο‰β‚‚ ↦ (rows_lt_m Ο‰β‚‚, other_cols Ο‰β‚‚)) ⁻¹' T)
      exact h_indep_combined s T hs hT_meas
    have h_eq : trunc = (fun p k b ↦ if h : b = a then if m β‰  0 then p.1 k
        else Nonempty.some inferInstance else p.2 k ⟨b, h⟩) ∘ proj := by
      funext Ο‰β‚‚; exact h_trunc_proj Ο‰β‚‚
    rw [h_eq]
    exact h_indep_proj.comp measurable_id h_g_meas
  rw [indepFun_iff_measure_inter_preimage_eq_mul] at h_indep_trunc
  have h_const : βˆ€ ω₁, ΞΌβ‚‚ (((fun Ο‰β‚‚ ↦ Ο‰β‚‚ m a) ⁻¹' s) ∩ ((fun Ο‰β‚‚ ↦ (ω₁, trunc Ο‰β‚‚)) ⁻¹' t)) =
      ΞΌβ‚‚ ((fun Ο‰β‚‚ ↦ Ο‰β‚‚ m a) ⁻¹' s) * ΞΌβ‚‚ ((fun Ο‰β‚‚ ↦ (ω₁, trunc Ο‰β‚‚)) ⁻¹' t) := fun ω₁ ↦
    h_indep_trunc s _ hs (ht.preimage (by fun_prop))
  simp_rw [h_const]
  let c := ΞΌβ‚‚ ((fun Ο‰β‚‚ ↦ Ο‰β‚‚ m a) ⁻¹' s)
  change ∫⁻ x, c * ΞΌβ‚‚ ((fun Ο‰β‚‚ ↦ (x, trunc Ο‰β‚‚)) ⁻¹' t) βˆ‚ΞΌβ‚ =
    (∫⁻ _, c βˆ‚ΞΌβ‚) * ∫⁻ x, ΞΌβ‚‚ ((fun Ο‰β‚‚ ↦ (x, trunc Ο‰β‚‚)) ⁻¹' t) βˆ‚ΞΌβ‚
  have h_preimage : βˆ€ x, (fun Ο‰β‚‚ ↦ (x, trunc Ο‰β‚‚)) ⁻¹' t = trunc ⁻¹' (Prod.mk x ⁻¹' t) := fun _ ↦ rfl
  simp_rw [h_preimage]
  have h_map : βˆ€ x, ΞΌβ‚‚ (trunc ⁻¹' (Prod.mk x ⁻¹' t)) = (ΞΌβ‚‚.map trunc) (Prod.mk x ⁻¹' t) := by
    intro x; rw [Measure.map_apply h_trunc_meas (ht.preimage (by fun_prop))]
  simp_rw [h_map]
  rw [lintegral_const_mul _ (measurable_measure_prodMk_left_finite ht),
    lintegral_const, measure_univ, mul_one]

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, 55 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.