LeanMachineLearning exposition

ProbabilityTheory.indepFun_proj_infinitePi_infinitePi🔗

Minimal Lean file

indepFun_proj_infinitePi_infinitePi🔗

LemmaProbabilityTheory.indepFun_proj_infinitePi_infinitePi
Details

No docstring.

🔗theorem
ProbabilityTheory.indepFun_proj_infinitePi_infinitePi.{u_1, u_2, u_3}
  {ι : Type u_1} {κ : Type u_2} {𝓧 : ι → κ → Type u_3}
  [m𝓧 : (i : ι) → (j : κ) → MeasurableSpace (𝓧 i j)]
  {μ : (i : ι) → (j : κ) → MeasureTheory.Measure (𝓧 i j)}
  [∀ (i : ι) (j : κ), MeasureTheory.IsProbabilityMeasure (μ i j)]
  {a b : κ} (h : a ≠ b) :
  IndepFun (fun ω i => ω i a) (fun ω i => ω i b)
    (MeasureTheory.Measure.infinitePi fun i =>
      MeasureTheory.Measure.infinitePi (μ i))
ProbabilityTheory.indepFun_proj_infinitePi_infinitePi.{u_1,
    u_2, u_3}
  {ι : Type u_1} {κ : Type u_2}
  {𝓧 : ι → κ → Type u_3}
  [m𝓧 :
    (i : ι) →
      (j : κ) → MeasurableSpace (𝓧 i j)]
  {μ :
    (i : ι) →
      (j : κ) →
        MeasureTheory.Measure (𝓧 i j)}
  [∀ (i : ι) (j : κ),
      MeasureTheory.IsProbabilityMeasure
        (μ i j)]
  {a b : κ} (h : a ≠ b) :
  IndepFun (fun ω i => ω i a)
    (fun ω i => ω i b)
    (MeasureTheory.Measure.infinitePi
      fun i =>
      MeasureTheory.Measure.infinitePi
        (μ i))

Code

lemma indepFun_proj_infinitePi_infinitePi {a b : κ} (h : a ≠ b) :
    IndepFun (fun ω i ↦ ω i a) (fun ω i ↦ ω i b) (infinitePi (fun i ↦ infinitePi (μ i)))
Body uses (1)
Used by (1)

Actions: Source · Open Issue

Proof
by
  simp_rw [IndepFun_iff_Indep, MeasurableSpace.comap_pi]
  have hd : Disjoint (range fun i : ι ↦ (i, a)) (range fun i ↦ (i, b)) := by
    simp [disjoint_range_iff, h]
  convert indep_iSup_of_disjoint (fun _ ↦ Measurable.comap_le (by fun_prop))
    (iIndepFun_uncurry_infinitePi' (X := fun _ _ x ↦ x) μ (by fun_prop)) hd
  all_goals rw [iSup_range]