LeanMachineLearning exposition

Bandits.ArrayModel.indepFun_cond_comp🔗

Minimal Lean file

indepFun_cond_comp🔗

LemmaBandits.ArrayModel.indepFun_cond_comp
Details

No docstring.

🔗theorem
Bandits.ArrayModel.indepFun_cond_comp.{u_3, u_4, u_5, u_6}
  {𝓐 : Type u_3} {β : Type u_4} {γ : Type u_5} {δ : Type u_6}
  {m𝓐 : MeasurableSpace 𝓐} {mβ : MeasurableSpace β}
  {mγ : MeasurableSpace γ} {mδ : MeasurableSpace δ}
  [MeasurableSingletonClass δ] {μ : MeasureTheory.Measure 𝓐} {X : 𝓐 → β}
  {Y : 𝓐 → γ} (hXY : ProbabilityTheory.IndepFun X Y μ)
  (hY : Measurable Y) {Z : γ → δ} (hZ : Measurable Z) (z : δ) :
  ProbabilityTheory.IndepFun X Y μ[|Z ∘ Y ⁻¹' {z}]
Bandits.ArrayModel.indepFun_cond_comp.{u_3,
    u_4, u_5, u_6}
  {𝓐 : Type u_3} {β : Type u_4}
  {γ : Type u_5} {δ : Type u_6}
  {m𝓐 : MeasurableSpace 𝓐}
  {mβ : MeasurableSpace β}
  {mγ : MeasurableSpace γ}
  {mδ : MeasurableSpace δ}
  [MeasurableSingletonClass δ]
  {μ : MeasureTheory.Measure 𝓐}
  {X : 𝓐 → β} {Y : 𝓐 → γ}
  (hXY : ProbabilityTheory.IndepFun X Y μ)
  (hY : Measurable Y) {Z : γ → δ}
  (hZ : Measurable Z) (z : δ) :
  ProbabilityTheory.IndepFun X Y
    μ[|Z ∘ Y ⁻¹' {z}]

Code

lemma indepFun_cond_comp {𝓐 β γ δ : Type*} {m𝓐 : MeasurableSpace 𝓐} {mβ : MeasurableSpace β}
    {mγ : MeasurableSpace γ} {mδ : MeasurableSpace δ} [MeasurableSingletonClass δ] {μ : Measure 𝓐}
    {X : 𝓐 → β} {Y : 𝓐 → γ} (hXY : X ⟂ᵢ[μ] Y) (hY : Measurable Y)
    {Z : γ → δ} (hZ : Measurable Z) (z : δ) :
    X ⟂ᵢ[μ[|(Z ∘ Y) ⁻¹' {z}]] Y
Body uses (1)
Used by (1)

Actions: Source · Open Issue

Proof
by
  have h_preim : (Z ∘ Y) ⁻¹' {z} = Y ⁻¹' (Z ⁻¹' {z}) := by grind
  simp_rw [h_preim]
  exact indepFun_cond_of_indepFun hXY hY (hZ (measurableSet_singleton z))