LeanMachineLearning exposition

1.12. ForMathlib.Probability.Independence.IndepInfinitePi🔗

Lemmas about independence and infinite products

Module LeanMachineLearning.ForMathlib.Probability.Independence.IndepInfinitePi contains 2 exposed declarations.

comap_pi🔗

LemmaMeasurableSpace.comap_pi
Details

No docstring.

🔗theorem
MeasurableSpace.comap_pi.{u_1, u_2, u_3} {δ : Type u_1}
  {X : δ → Type u_2} [m : (a : δ) → MeasurableSpace (X a)]
  {α : Type u_3} {g : α → (a : δ) → X a} :
  MeasurableSpace.comap g pi =
    ⨆ a, MeasurableSpace.comap (fun x => g x a) (m a)
MeasurableSpace.comap_pi.{u_1, u_2, u_3}
  {δ : Type u_1} {X : δ → Type u_2}
  [m : (a : δ) → MeasurableSpace (X a)]
  {α : Type u_3} {g : α → (a : δ) → X a} :
  MeasurableSpace.comap g pi =
    ⨆ a,
      MeasurableSpace.comap
        (fun x => g x a) (m a)

Code

lemma comap_pi {g : α → ∀ a, X a} : pi.comap g = ⨆ a, (m a).comap (fun x ↦ g x a)
Used by (2)

Actions: Source · Open Issue

Proof
by
  simp_rw [pi, comap_iSup, comap_comp, comp_def]

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]
  1. MeasurableSpace.comap_pi
  2. ProbabilityTheory.indepFun_proj_infinitePi_infinitePi