LeanMachineLearning exposition

ProbabilityTheory.Kernel.measurableSet_eq🔗

Minimal Lean file

measurableSet_eq🔗

LemmaProbabilityTheory.Kernel.measurableSet_eq
Details

No docstring.

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

Code

lemma measurableSet_eq (κ η : Kernel α β) [IsFiniteKernel κ] [IsFiniteKernel η] :
    MeasurableSet {a | κ a = η a}
Body uses (4)
Used by (4)

Actions: Source · Open Issue

Proof
by
  classical
  have h_sub : {a | κ a = η a} = {a | (κ - η) a = 0} ∩ {a | (η - κ) a = 0} := by
    ext1 a
    simp only [Set.mem_setOf_eq, Set.mem_inter_iff, sub_apply_eq_zero_iff_le]
    exact ⟨fun h ↦ by simp [h], fun h ↦ le_antisymm h.1 h.2⟩
  rw [h_sub]
  refine MeasurableSet.inter ?_ ?_
  · exact measurableSet_eq_zero _
  · exact measurableSet_eq_zero _