LeanMachineLearning exposition

ProbabilityTheory.Kernel.measurableSet_eq_zero🔗

Minimal Lean file

measurableSet_eq_zero🔗

LemmaProbabilityTheory.Kernel.measurableSet_eq_zero
Details

No docstring.

🔗theorem
ProbabilityTheory.Kernel.measurableSet_eq_zero.{u_1, u_2} {α : Type u_1}
  {β : Type u_2} {mα : MeasurableSpace α} {mβ : MeasurableSpace β}
  [MeasurableSpace.CountableOrCountablyGenerated α β] (κ : Kernel α β)
  [IsFiniteKernel κ] : MeasurableSet {a | κ a = 0}
ProbabilityTheory.Kernel.measurableSet_eq_zero.{u_1,
    u_2}
  {α : Type u_1} {β : Type u_2}
  {mα : MeasurableSpace α}
  {mβ : MeasurableSpace β}
  [MeasurableSpace.CountableOrCountablyGenerated
      α β]
  (κ : Kernel α β) [IsFiniteKernel κ] :
  MeasurableSet {a | κ a = 0}

Code

lemma measurableSet_eq_zero (κ : Kernel α β) [IsFiniteKernel κ] :
    MeasurableSet {a | κ a = 0}
Used by (1)

Actions: Source · Open Issue

Proof
by
  have h_sing : {a | κ a = 0} = {a | κ a ⟂ₘ κ a} := by ext; simp
  rw [h_sing]
  exact measurableSet_mutuallySingular κ κ