LeanMachineLearning exposition

1.9. ForMathlib.Probability.Kernel.KernelSub🔗

Kernel substraction

Module LeanMachineLearning.ForMathlib.Probability.Kernel.KernelSub contains 15 exposed declarations.

sub_apply_eq_rnDeriv_add_singularPart🔗

LemmaMeasureTheory.Measure.sub_apply_eq_rnDeriv_add_singularPart
Details

No docstring.

🔗theorem
MeasureTheory.Measure.sub_apply_eq_rnDeriv_add_singularPart.{u_1}
  {α : Type u_1} {mα : MeasurableSpace α} {μ ν : Measure α}
  [IsFiniteMeasure μ] [IsFiniteMeasure ν] (s : Set α) :
  (μ - ν) s =
    (withDensity ν fun a => rnDeriv μ ν a - 1) s + (singularPart μ ν) s
MeasureTheory.Measure.sub_apply_eq_rnDeriv_add_singularPart.{u_1}
  {α : Type u_1} {mα : MeasurableSpace α}
  {μ ν : Measure α} [IsFiniteMeasure μ]
  [IsFiniteMeasure ν] (s : Set α) :
  (μ - ν) s =
    (withDensity ν fun a =>
          rnDeriv μ ν a - 1)
        s +
      (singularPart μ ν) s

Code

lemma sub_apply_eq_rnDeriv_add_singularPart [IsFiniteMeasure μ] [IsFiniteMeasure ν] (s : Set α) :
    (μ - ν) s = ν.withDensity (fun a ↦ μ.rnDeriv ν a - 1) s + μ.singularPart ν s
Used by (1)

Actions: Source · Open Issue

Proof
by
  have hμ : μ = ν.withDensity (fun a ↦ μ.rnDeriv ν a) + μ.singularPart ν := by
    rw [rnDeriv_add_singularPart]
  have hν : ν = ν.withDensity 1 := by rw [withDensity_one]
  conv_lhs => rw [hν, hμ, add_comm _ (μ.singularPart ν)]
  rw [← add_sub_of_mutuallySingular]
  swap
  · simp only [withDensity_one]
    exact mutuallySingular_singularPart μ ν
  simp only [coe_add, Pi.add_apply]
  have : IsFiniteMeasure (ν.withDensity 1) := by simp only [withDensity_one]; infer_instance
  rw [add_comm, ← withDensity_sub (by fun_prop) (by fun_prop)]
  congr

instSubOfDecidableIsSFiniteKernel_leanMachineLearning🔗

InstanceProbabilityTheory.Kernel.instSubOfDecidableIsSFiniteKernel_leanMachineLearning
Details

No docstring.

🔗def
ProbabilityTheory.Kernel.instSubOfDecidableIsSFiniteKernel_leanMachineLearning.{u_1,
    u_2}
  {α : Type u_1} {β : Type u_2} {mα : MeasurableSpace α}
  {mβ : MeasurableSpace β}
  [MeasurableSpace.CountableOrCountablyGenerated α β]
  [(η : Kernel α β) → Decidable (IsSFiniteKernel η)] : Sub (Kernel α β)
ProbabilityTheory.Kernel.instSubOfDecidableIsSFiniteKernel_leanMachineLearning.{u_1,
    u_2}
  {α : Type u_1} {β : Type u_2}
  {mα : MeasurableSpace α}
  {mβ : MeasurableSpace β}
  [MeasurableSpace.CountableOrCountablyGenerated
      α β]
  [(η : Kernel α β) →
      Decidable (IsSFiniteKernel η)] :
  Sub (Kernel α β)

Code

noncomputable
instance [∀ η : Kernel α β, Decidable (IsSFiniteKernel η)] :
    Sub (Kernel α β) where
  sub κ η
Used by (11)

Actions: Source · Open Issue

Proof
if h : IsSFiniteKernel κ ∧ IsSFiniteKernel η
    then
      have := h.1
      have := h.2
      η.withDensity (fun a ↦ κ.rnDeriv η a - 1) + κ.singularPart η
    else 0

sub_def🔗

LemmaProbabilityTheory.Kernel.sub_def
Details

No docstring.

🔗theorem
ProbabilityTheory.Kernel.sub_def.{u_1, u_2} {α : Type u_1}
  {β : Type u_2} {mα : MeasurableSpace α} {mβ : MeasurableSpace β}
  [MeasurableSpace.CountableOrCountablyGenerated α β] {κ η : Kernel α β}
  [(η : Kernel α β) → Decidable (IsSFiniteKernel η)] :
  κ - η =
    if h : IsSFiniteKernel κ ∧ IsSFiniteKernel η then
      have this := ⋯;
      have this_1 := ⋯;
      (withDensity η fun a => rnDeriv κ η a - 1) + singularPart κ η
    else 0
ProbabilityTheory.Kernel.sub_def.{u_1,
    u_2}
  {α : Type u_1} {β : Type u_2}
  {mα : MeasurableSpace α}
  {mβ : MeasurableSpace β}
  [MeasurableSpace.CountableOrCountablyGenerated
      α β]
  {κ η : Kernel α β}
  [(η : Kernel α β) →
      Decidable (IsSFiniteKernel η)] :
  κ - η =
    if h :
        IsSFiniteKernel κ ∧
          IsSFiniteKernel η then
      have this := ⋯;
      have this_1 := ⋯;
      (withDensity η fun a =>
          rnDeriv κ η a - 1) +
        singularPart κ η
    else 0

Code

lemma sub_def [∀ η : Kernel α β, Decidable (IsSFiniteKernel η)] :
    κ - η = if h : IsSFiniteKernel κ ∧ IsSFiniteKernel η
    then
      have
Type uses (1)
Used by (1)

Actions: Source · Open Issue

Proof
h.1
      have := h.2
      η.withDensity (fun a ↦ κ.rnDeriv η a - 1) + κ.singularPart η
    else 0 :=
  rfl

sub_of_not_isSFiniteKernel_left🔗

LemmaProbabilityTheory.Kernel.sub_of_not_isSFiniteKernel_left
Details

No docstring.

🔗theorem
ProbabilityTheory.Kernel.sub_of_not_isSFiniteKernel_left.{u_1, u_2}
  {α : Type u_1} {β : Type u_2} {mα : MeasurableSpace α}
  {mβ : MeasurableSpace β}
  [MeasurableSpace.CountableOrCountablyGenerated α β] {κ η : Kernel α β}
  [(η : Kernel α β) → Decidable (IsSFiniteKernel η)]
  (h : ¬IsSFiniteKernel κ) : κ - η = 0
ProbabilityTheory.Kernel.sub_of_not_isSFiniteKernel_left.{u_1,
    u_2}
  {α : Type u_1} {β : Type u_2}
  {mα : MeasurableSpace α}
  {mβ : MeasurableSpace β}
  [MeasurableSpace.CountableOrCountablyGenerated
      α β]
  {κ η : Kernel α β}
  [(η : Kernel α β) →
      Decidable (IsSFiniteKernel η)]
  (h : ¬IsSFiniteKernel κ) : κ - η = 0

Code

lemma sub_of_not_isSFiniteKernel_left [∀ η : Kernel α β, Decidable (IsSFiniteKernel η)]
    (h : ¬IsSFiniteKernel κ) : κ - η = 0
Type uses (1)

Actions: Source · Open Issue

Proof
by simp [sub_def, h]

sub_of_not_isSFiniteKernel_right🔗

LemmaProbabilityTheory.Kernel.sub_of_not_isSFiniteKernel_right
Details

No docstring.

🔗theorem
ProbabilityTheory.Kernel.sub_of_not_isSFiniteKernel_right.{u_1, u_2}
  {α : Type u_1} {β : Type u_2} {mα : MeasurableSpace α}
  {mβ : MeasurableSpace β}
  [MeasurableSpace.CountableOrCountablyGenerated α β] {κ η : Kernel α β}
  [(η : Kernel α β) → Decidable (IsSFiniteKernel η)]
  (h : ¬IsSFiniteKernel η) : κ - η = 0
ProbabilityTheory.Kernel.sub_of_not_isSFiniteKernel_right.{u_1,
    u_2}
  {α : Type u_1} {β : Type u_2}
  {mα : MeasurableSpace α}
  {mβ : MeasurableSpace β}
  [MeasurableSpace.CountableOrCountablyGenerated
      α β]
  {κ η : Kernel α β}
  [(η : Kernel α β) →
      Decidable (IsSFiniteKernel η)]
  (h : ¬IsSFiniteKernel η) : κ - η = 0

Code

lemma sub_of_not_isSFiniteKernel_right [∀ η : Kernel α β, Decidable (IsSFiniteKernel η)]
    (h : ¬IsSFiniteKernel η) : κ - η = 0
Type uses (1)

Actions: Source · Open Issue

Proof
by simp [sub_def, h]

sub_of_isSFiniteKernel🔗

LemmaProbabilityTheory.Kernel.sub_of_isSFiniteKernel
Details

No docstring.

🔗theorem
ProbabilityTheory.Kernel.sub_of_isSFiniteKernel.{u_1, u_2}
  {α : Type u_1} {β : Type u_2} {mα : MeasurableSpace α}
  {mβ : MeasurableSpace β}
  [MeasurableSpace.CountableOrCountablyGenerated α β] {κ η : Kernel α β}
  [IsSFiniteKernel κ] [IsSFiniteKernel η]
  [(η : Kernel α β) → Decidable (IsSFiniteKernel η)] :
  κ - η = (withDensity η fun a => rnDeriv κ η a - 1) + singularPart κ η
ProbabilityTheory.Kernel.sub_of_isSFiniteKernel.{u_1,
    u_2}
  {α : Type u_1} {β : Type u_2}
  {mα : MeasurableSpace α}
  {mβ : MeasurableSpace β}
  [MeasurableSpace.CountableOrCountablyGenerated
      α β]
  {κ η : Kernel α β} [IsSFiniteKernel κ]
  [IsSFiniteKernel η]
  [(η : Kernel α β) →
      Decidable (IsSFiniteKernel η)] :
  κ - η =
    (withDensity η fun a =>
        rnDeriv κ η a - 1) +
      singularPart κ η

Code

lemma sub_of_isSFiniteKernel [IsSFiniteKernel κ] [IsSFiniteKernel η]
    [∀ η : Kernel α β, Decidable (IsSFiniteKernel η)] :
    κ - η = η.withDensity (fun a ↦ κ.rnDeriv η a - 1) + κ.singularPart η
Type uses (1)
Body uses (1)
Used by (1)

Actions: Source · Open Issue

Proof
by
  rw [sub_def, dif_pos]
  exact ⟨inferInstance, inferInstance⟩

sub_apply_eq_rnDeriv_add_singularPart🔗

LemmaProbabilityTheory.Kernel.sub_apply_eq_rnDeriv_add_singularPart
Details

No docstring.

🔗theorem
ProbabilityTheory.Kernel.sub_apply_eq_rnDeriv_add_singularPart.{u_1,
    u_2}
  {α : Type u_1} {β : Type u_2} {mα : MeasurableSpace α}
  {mβ : MeasurableSpace β}
  [MeasurableSpace.CountableOrCountablyGenerated α β] {κ η : Kernel α β}
  [(η : Kernel α β) → Decidable (IsSFiniteKernel η)] [IsSFiniteKernel κ]
  [IsSFiniteKernel η] (a : α) :
  (κ - η) a =
    (withDensity η fun a => rnDeriv κ η a - 1) a + (singularPart κ η) a
ProbabilityTheory.Kernel.sub_apply_eq_rnDeriv_add_singularPart.{u_1,
    u_2}
  {α : Type u_1} {β : Type u_2}
  {mα : MeasurableSpace α}
  {mβ : MeasurableSpace β}
  [MeasurableSpace.CountableOrCountablyGenerated
      α β]
  {κ η : Kernel α β}
  [(η : Kernel α β) →
      Decidable (IsSFiniteKernel η)]
  [IsSFiniteKernel κ] [IsSFiniteKernel η]
  (a : α) :
  (κ - η) a =
    (withDensity η fun a =>
          rnDeriv κ η a - 1)
        a +
      (singularPart κ η) a

Code

lemma sub_apply_eq_rnDeriv_add_singularPart [∀ η : Kernel α β, Decidable (IsSFiniteKernel η)]
    [IsSFiniteKernel κ] [IsSFiniteKernel η] (a : α) :
    (κ - η) a = η.withDensity (fun a ↦ κ.rnDeriv η a - 1) a + κ.singularPart η a
Type uses (1)
Body uses (1)
Used by (2)

Actions: Source · Open Issue

Proof
by
  rw [sub_of_isSFiniteKernel]
  rfl

sub_apply🔗

LemmaProbabilityTheory.Kernel.sub_apply
Details

No docstring.

🔗theorem
ProbabilityTheory.Kernel.sub_apply.{u_1, u_2} {α : Type u_1}
  {β : Type u_2} {mα : MeasurableSpace α} {mβ : MeasurableSpace β}
  [MeasurableSpace.CountableOrCountablyGenerated α β] {κ η : Kernel α β}
  [(η : Kernel α β) → Decidable (IsSFiniteKernel η)] [IsFiniteKernel κ]
  [IsFiniteKernel η] (a : α) : (κ - η) a = κ a - η a
ProbabilityTheory.Kernel.sub_apply.{u_1,
    u_2}
  {α : Type u_1} {β : Type u_2}
  {mα : MeasurableSpace α}
  {mβ : MeasurableSpace β}
  [MeasurableSpace.CountableOrCountablyGenerated
      α β]
  {κ η : Kernel α β}
  [(η : Kernel α β) →
      Decidable (IsSFiniteKernel η)]
  [IsFiniteKernel κ] [IsFiniteKernel η]
  (a : α) : (κ - η) a = κ a - η a

Code

lemma sub_apply [∀ η : Kernel α β, Decidable (IsSFiniteKernel η)] [IsFiniteKernel κ]
    [IsFiniteKernel η] (a : α) :
    (κ - η) a = κ a - η a
Type uses (1)
Body uses (2)
Used by (1)

Actions: Source · Open Issue

Proof
by
  ext s hs
  rw [sub_apply_eq_rnDeriv_add_singularPart, Kernel.withDensity_apply _ (by fun_prop),
    Kernel.singularPart_eq_singularPart_measure, Measure.sub_apply_eq_rnDeriv_add_singularPart _]
  simp only [Measure.coe_add, Pi.add_apply]
  congr 2
  refine MeasureTheory.withDensity_congr_ae ?_
  filter_upwards [Kernel.rnDeriv_eq_rnDeriv_measure (κ := κ) (η := η) (a := a)] with b hb
  simp [← hb]

le_iff🔗

LemmaProbabilityTheory.Kernel.le_iff
Details

No docstring.

🔗theorem
ProbabilityTheory.Kernel.le_iff.{u_1, u_2} {α : Type u_1} {β : Type u_2}
  {mα : MeasurableSpace α} {mβ : MeasurableSpace β} (κ η : Kernel α β) :
  κ ≤ η ↔ ∀ (a : α), κ a ≤ η a
ProbabilityTheory.Kernel.le_iff.{u_1, u_2}
  {α : Type u_1} {β : Type u_2}
  {mα : MeasurableSpace α}
  {mβ : MeasurableSpace β}
  (κ η : Kernel α β) :
  κ ≤ η ↔ ∀ (a : α), κ a ≤ η a

Code

lemma le_iff (κ η : Kernel α β) : κ ≤ η ↔ ∀ a, κ a ≤ η a
Used by (2)

Actions: Source · Open Issue

Proof
Iff.rfl

sub_le_self🔗

LemmaProbabilityTheory.Kernel.sub_le_self
Details

No docstring.

🔗theorem
ProbabilityTheory.Kernel.sub_le_self.{u_1, u_2} {α : Type u_1}
  {β : Type u_2} {mα : MeasurableSpace α} {mβ : MeasurableSpace β}
  [MeasurableSpace.CountableOrCountablyGenerated α β] {κ η : Kernel α β}
  [(η : Kernel α β) → Decidable (IsSFiniteKernel η)] [IsFiniteKernel κ]
  [IsFiniteKernel η] : κ - η ≤ κ
ProbabilityTheory.Kernel.sub_le_self.{u_1,
    u_2}
  {α : Type u_1} {β : Type u_2}
  {mα : MeasurableSpace α}
  {mβ : MeasurableSpace β}
  [MeasurableSpace.CountableOrCountablyGenerated
      α β]
  {κ η : Kernel α β}
  [(η : Kernel α β) →
      Decidable (IsSFiniteKernel η)]
  [IsFiniteKernel κ] [IsFiniteKernel η] :
  κ - η ≤ κ

Code

lemma sub_le_self [∀ η : Kernel α β, Decidable (IsSFiniteKernel η)] [IsFiniteKernel κ]
    [IsFiniteKernel η] :
    κ - η ≤ κ
Type uses (1)
Body uses (2)
Used by (1)

Actions: Source · Open Issue

Proof
by
  rw [le_iff]
  intro a
  rw [sub_apply]
  exact Measure.sub_le

instIsFiniteKernelHSub_leanMachineLearning🔗

InstanceProbabilityTheory.Kernel.instIsFiniteKernelHSub_leanMachineLearning
Details

No docstring.

🔗theorem
ProbabilityTheory.Kernel.instIsFiniteKernelHSub_leanMachineLearning.{u_1,
    u_2}
  {α : Type u_1} {β : Type u_2} {mα : MeasurableSpace α}
  {mβ : MeasurableSpace β}
  [MeasurableSpace.CountableOrCountablyGenerated α β] {κ η : Kernel α β}
  [(η : Kernel α β) → Decidable (IsSFiniteKernel η)] [IsFiniteKernel κ]
  [IsFiniteKernel η] : IsFiniteKernel (κ - η)
ProbabilityTheory.Kernel.instIsFiniteKernelHSub_leanMachineLearning.{u_1,
    u_2}
  {α : Type u_1} {β : Type u_2}
  {mα : MeasurableSpace α}
  {mβ : MeasurableSpace β}
  [MeasurableSpace.CountableOrCountablyGenerated
      α β]
  {κ η : Kernel α β}
  [(η : Kernel α β) →
      Decidable (IsSFiniteKernel η)]
  [IsFiniteKernel κ] [IsFiniteKernel η] :
  IsFiniteKernel (κ - η)

Code

instance [∀ η : Kernel α β, Decidable (IsSFiniteKernel η)]
    [IsFiniteKernel κ] [IsFiniteKernel η] : IsFiniteKernel (κ - η)
Type uses (1)
Body uses (1)
Used by (1)

Actions: Source · Open Issue

Proof
isFiniteKernel_of_le sub_le_self

sub_apply_eq_zero_iff_le🔗

LemmaProbabilityTheory.Kernel.sub_apply_eq_zero_iff_le
Details

No docstring.

🔗theorem
ProbabilityTheory.Kernel.sub_apply_eq_zero_iff_le.{u_1, u_2}
  {α : Type u_1} {β : Type u_2} {mα : MeasurableSpace α}
  {mβ : MeasurableSpace β}
  [MeasurableSpace.CountableOrCountablyGenerated α β] {κ η : Kernel α β}
  [(η : Kernel α β) → Decidable (IsSFiniteKernel η)] [IsFiniteKernel κ]
  [IsFiniteKernel η] (a : α) : (κ - η) a = 0 ↔ κ a ≤ η a
ProbabilityTheory.Kernel.sub_apply_eq_zero_iff_le.{u_1,
    u_2}
  {α : Type u_1} {β : Type u_2}
  {mα : MeasurableSpace α}
  {mβ : MeasurableSpace β}
  [MeasurableSpace.CountableOrCountablyGenerated
      α β]
  {κ η : Kernel α β}
  [(η : Kernel α β) →
      Decidable (IsSFiniteKernel η)]
  [IsFiniteKernel κ] [IsFiniteKernel η]
  (a : α) : (κ - η) a = 0 ↔ κ a ≤ η a

Code

lemma sub_apply_eq_zero_iff_le [∀ η : Kernel α β, Decidable (IsSFiniteKernel η)]
    [IsFiniteKernel κ] [IsFiniteKernel η] (a : α) : (κ - η) a = 0 ↔ κ a ≤ η a
Type uses (1)
Body uses (1)
Used by (2)

Actions: Source · Open Issue

Proof
by
  simp_rw [sub_apply_eq_rnDeriv_add_singularPart,
    add_eq_zero_iff_of_nonneg (Measure.zero_le _) (Measure.zero_le _)]
  refine ⟨fun h ↦ ?_, fun h ↦ ?_⟩
  · rw [Kernel.withDensity_apply _ (by fun_prop), withDensity_eq_zero_iff (by fun_prop)] at h
    rw [singularPart_eq_zero_iff_absolutelyContinuous κ η a] at h
    rw [← Measure.rnDeriv_le_one_iff_le h.2]
    filter_upwards [h.1, rnDeriv_eq_rnDeriv_measure (κ := κ) (η := η) (a := a)] with b hb1 hb2
    rw [← hb2]
    simp only [Pi.sub_apply, Pi.one_apply, Pi.zero_apply] at hb1
    rwa [tsub_eq_zero_iff_le] at hb1
  · rw [(singularPart_eq_zero_iff_absolutelyContinuous κ η a).mpr
        (Measure.absolutelyContinuous_of_le h)]
    rw [Kernel.withDensity_apply _ (by fun_prop), withDensity_eq_zero_iff (by fun_prop)]
    simp only [and_true]
    suffices κ.rnDeriv η a ≤ᵐ[η a] 1 by
      filter_upwards [this] with b hb
      simpa [tsub_eq_zero_iff_le] using hb
    filter_upwards [Measure.rnDeriv_le_one_of_le h,
      rnDeriv_eq_rnDeriv_measure (κ := κ) (η := η) (a := a)] with b hb1 hb2
    rwa [hb2]

sub_eq_zero_iff_le🔗

LemmaProbabilityTheory.Kernel.sub_eq_zero_iff_le
Details

No docstring.

🔗theorem
ProbabilityTheory.Kernel.sub_eq_zero_iff_le.{u_1, u_2} {α : Type u_1}
  {β : Type u_2} {mα : MeasurableSpace α} {mβ : MeasurableSpace β}
  [MeasurableSpace.CountableOrCountablyGenerated α β] {κ η : Kernel α β}
  [(η : Kernel α β) → Decidable (IsSFiniteKernel η)] [IsFiniteKernel κ]
  [IsFiniteKernel η] : κ - η = 0 ↔ κ ≤ η
ProbabilityTheory.Kernel.sub_eq_zero_iff_le.{u_1,
    u_2}
  {α : Type u_1} {β : Type u_2}
  {mα : MeasurableSpace α}
  {mβ : MeasurableSpace β}
  [MeasurableSpace.CountableOrCountablyGenerated
      α β]
  {κ η : Kernel α β}
  [(η : Kernel α β) →
      Decidable (IsSFiniteKernel η)]
  [IsFiniteKernel κ] [IsFiniteKernel η] :
  κ - η = 0 ↔ κ ≤ η

Code

lemma sub_eq_zero_iff_le [∀ η : Kernel α β, Decidable (IsSFiniteKernel η)]
    [IsFiniteKernel κ] [IsFiniteKernel η] : κ - η = 0 ↔ κ ≤ η
Type uses (1)
Body uses (2)

Actions: Source · Open Issue

Proof
by
  simp [Kernel.ext_iff, le_iff, sub_apply_eq_zero_iff_le]

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 κ κ

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 _
  1. MeasureTheory.Measure.sub_apply_eq_rnDeriv_add_singularPart
  2. ProbabilityTheory.Kernel.instSubOfDecidableIsSFiniteKernel_leanMachineLearning
  3. ProbabilityTheory.Kernel.sub_def
  4. ProbabilityTheory.Kernel.sub_of_not_isSFiniteKernel_left
  5. ProbabilityTheory.Kernel.sub_of_not_isSFiniteKernel_right
  6. ProbabilityTheory.Kernel.sub_of_isSFiniteKernel
  7. ProbabilityTheory.Kernel.sub_apply_eq_rnDeriv_add_singularPart
  8. ProbabilityTheory.Kernel.sub_apply
  9. ProbabilityTheory.Kernel.le_iff
  10. ProbabilityTheory.Kernel.sub_le_self
  11. ProbabilityTheory.Kernel.instIsFiniteKernelHSub_leanMachineLearning
  12. ProbabilityTheory.Kernel.sub_apply_eq_zero_iff_le
  13. ProbabilityTheory.Kernel.sub_eq_zero_iff_le
  14. ProbabilityTheory.Kernel.measurableSet_eq_zero
  15. ProbabilityTheory.Kernel.measurableSet_eq