LeanMachineLearning exposition

ProbabilityTheory.Kernel.deterministic_inj🔗

Minimal Lean file

deterministic_inj🔗

LemmaProbabilityTheory.Kernel.deterministic_inj
Details

Two deterministic kernels are equal if and only if their underlying functions are equal.

🔗theorem
ProbabilityTheory.Kernel.deterministic_inj.{u_1, u_2} {α : Type u_1}
  {β : Type u_2} {mα : MeasurableSpace α} {mβ : MeasurableSpace β}
  [MeasurableSpace.SeparatesPoints β] {f g : α → β} {hf : Measurable f}
  {hg : Measurable g} : deterministic f hf = deterministic g hg ↔ f = g
ProbabilityTheory.Kernel.deterministic_inj.{u_1,
    u_2}
  {α : Type u_1} {β : Type u_2}
  {mα : MeasurableSpace α}
  {mβ : MeasurableSpace β}
  [MeasurableSpace.SeparatesPoints β]
  {f g : α → β} {hf : Measurable f}
  {hg : Measurable g} :
  deterministic f hf =
      deterministic g hg ↔
    f = g

Code

lemma deterministic_inj [MeasurableSpace.SeparatesPoints β]
    {f g : α → β} {hf : Measurable f} {hg : Measurable g} :
    Kernel.deterministic f hf = Kernel.deterministic g hg ↔ f = g
Used by (5)

Actions: Source · Open Issue

Proof
by
  simp [Kernel.ext_iff, Kernel.deterministic_apply, dirac_eq_dirac_iff, funext_iff]