LeanMachineLearning exposition

1.15. ForMathlib.Probability.Kernel.Composition.MapComap🔗

Lemmas about map and comap of Markov kernels

Module LeanMachineLearning.ForMathlib.Probability.Kernel.Composition.MapComap contains 4 exposed declarations.

prodMkLeft_inj🔗

LemmaProbabilityTheory.Kernel.prodMkLeft_inj
Details

No docstring.

🔗theorem
ProbabilityTheory.Kernel.prodMkLeft_inj.{u_1, u_2, u_3} {α : Type u_1}
  {β : Type u_2} {γ : Type u_3} {mα : MeasurableSpace α}
  {mβ : MeasurableSpace β} {mγ : MeasurableSpace γ}
  [h_nonempty : Nonempty γ] (κ ν : Kernel α β) :
  prodMkLeft γ κ = prodMkLeft γ ν ↔ κ = ν
ProbabilityTheory.Kernel.prodMkLeft_inj.{u_1,
    u_2, u_3}
  {α : Type u_1} {β : Type u_2}
  {γ : Type u_3} {mα : MeasurableSpace α}
  {mβ : MeasurableSpace β}
  {mγ : MeasurableSpace γ}
  [h_nonempty : Nonempty γ]
  (κ ν : Kernel α β) :
  prodMkLeft γ κ = prodMkLeft γ ν ↔ κ = ν

Code

lemma prodMkLeft_inj [h_nonempty : Nonempty γ]
    (κ ν : Kernel α β) :
    κ.prodMkLeft γ = ν.prodMkLeft γ ↔ κ = ν
Used by (1)

Actions: Source · Open Issue

Proof
by
  simp only [Kernel.ext_iff, Kernel.prodMkLeft_apply, Prod.forall]
  exact ⟨fun h b ↦ h h_nonempty.some b, fun h _ b ↦ h b⟩

prodMkRight_inj🔗

LemmaProbabilityTheory.Kernel.prodMkRight_inj
Details

No docstring.

🔗theorem
ProbabilityTheory.Kernel.prodMkRight_inj.{u_1, u_2, u_3} {α : Type u_1}
  {β : Type u_2} {γ : Type u_3} {mα : MeasurableSpace α}
  {mβ : MeasurableSpace β} {mγ : MeasurableSpace γ}
  [h_nonempty : Nonempty γ] (κ ν : Kernel α β) :
  prodMkRight γ κ = prodMkRight γ ν ↔ κ = ν
ProbabilityTheory.Kernel.prodMkRight_inj.{u_1,
    u_2, u_3}
  {α : Type u_1} {β : Type u_2}
  {γ : Type u_3} {mα : MeasurableSpace α}
  {mβ : MeasurableSpace β}
  {mγ : MeasurableSpace γ}
  [h_nonempty : Nonempty γ]
  (κ ν : Kernel α β) :
  prodMkRight γ κ = prodMkRight γ ν ↔
    κ = ν

Code

lemma prodMkRight_inj [h_nonempty : Nonempty γ]
    (κ ν : Kernel α β) :
    κ.prodMkRight γ = ν.prodMkRight γ ↔ κ = ν

Actions: Source · Open Issue

Proof
by
  simp only [Kernel.ext_iff, Kernel.prodMkRight_apply, Prod.forall]
  exact ⟨fun h a ↦ h a h_nonempty.some, fun h a _ ↦ h a⟩

prodMkLeft_deterministic🔗

LemmaProbabilityTheory.Kernel.prodMkLeft_deterministic
Details

No docstring.

🔗theorem
ProbabilityTheory.Kernel.prodMkLeft_deterministic.{u_1, u_2, u_3}
  {α : Type u_1} {β : Type u_2} {γ : Type u_3} {mα : MeasurableSpace α}
  {mβ : MeasurableSpace β} {mγ : MeasurableSpace γ} {f : α → β}
  (hf : Measurable f) :
  prodMkLeft γ (deterministic f hf) =
    deterministic (fun p => f (Prod.snd p)) ⋯
ProbabilityTheory.Kernel.prodMkLeft_deterministic.{u_1,
    u_2, u_3}
  {α : Type u_1} {β : Type u_2}
  {γ : Type u_3} {mα : MeasurableSpace α}
  {mβ : MeasurableSpace β}
  {mγ : MeasurableSpace γ} {f : α → β}
  (hf : Measurable f) :
  prodMkLeft γ (deterministic f hf) =
    deterministic
      (fun p => f (Prod.snd p)) ⋯

Code

lemma prodMkLeft_deterministic {f : α → β} (hf : Measurable f) :
    (Kernel.deterministic f hf).prodMkLeft γ =
      Kernel.deterministic (fun p ↦ f p.2) (by fun_prop)
Used by (1)

Actions: Source · Open Issue

Proof
by
  ext
  simp [Kernel.deterministic_apply]

prodMkRight_deterministic🔗

LemmaProbabilityTheory.Kernel.prodMkRight_deterministic
Details

No docstring.

🔗theorem
ProbabilityTheory.Kernel.prodMkRight_deterministic.{u_1, u_2, u_3}
  {α : Type u_1} {β : Type u_2} {γ : Type u_3} {mα : MeasurableSpace α}
  {mβ : MeasurableSpace β} {mγ : MeasurableSpace γ} {f : α → β}
  (hf : Measurable f) :
  prodMkRight γ (deterministic f hf) =
    deterministic (fun p => f (Prod.fst p)) ⋯
ProbabilityTheory.Kernel.prodMkRight_deterministic.{u_1,
    u_2, u_3}
  {α : Type u_1} {β : Type u_2}
  {γ : Type u_3} {mα : MeasurableSpace α}
  {mβ : MeasurableSpace β}
  {mγ : MeasurableSpace γ} {f : α → β}
  (hf : Measurable f) :
  prodMkRight γ (deterministic f hf) =
    deterministic
      (fun p => f (Prod.fst p)) ⋯

Code

lemma prodMkRight_deterministic {f : α → β} (hf : Measurable f) :
    (Kernel.deterministic f hf).prodMkRight γ =
      Kernel.deterministic (fun p ↦ f p.1) (by fun_prop)

Actions: Source · Open Issue

Proof
by
  ext
  simp [Kernel.deterministic_apply]
  1. ProbabilityTheory.Kernel.prodMkLeft_inj
  2. ProbabilityTheory.Kernel.prodMkRight_inj
  3. ProbabilityTheory.Kernel.prodMkLeft_deterministic
  4. ProbabilityTheory.Kernel.prodMkRight_deterministic