Documentation

LeanMachineLearning.Probability.Kernel.KernelSub

Kernels substraction #

source
theorem MeasureTheory.Measure.sub_apply_eq_rnDeriv_add_singularPart {α : Type u_1} {mα : MeasurableSpace α} {μ ν : Measure α} [IsFiniteMeasure μ] [IsFiniteMeasure ν] (s : Set α) :
(μ - ν) s = (ν.withDensity fun (a : α) => μ.rnDeriv ν a - 1) s + (μ.singularPart ν) s
source
@[implicit_reducible]
noncomputable instance ProbabilityTheory.Kernel.instSubOfDecidableIsSFiniteKernel_leanMachineLearning {α : Type u_1} {β : Type u_2} {mα : MeasurableSpace α} {mβ : MeasurableSpace β} [MeasurableSpace.CountableOrCountablyGenerated α β] [(η : Kernel α β) → Decidable (IsSFiniteKernel η)] :
Sub (Kernel α β)
Equations
  • One or more equations did not get rendered due to their size.
source
theorem ProbabilityTheory.Kernel.sub_def {α : 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
source
@[simp]
theorem ProbabilityTheory.Kernel.sub_of_not_isSFiniteKernel_left {α : Type u_1} {β : Type u_2} {mα : MeasurableSpace α} {mβ : MeasurableSpace β} [MeasurableSpace.CountableOrCountablyGenerated α β] {κ η : Kernel α β} [(η : Kernel α β) → Decidable (IsSFiniteKernel η)] (h : ¬IsSFiniteKernel κ) :
κ - η = 0
source
@[simp]
theorem ProbabilityTheory.Kernel.sub_of_not_isSFiniteKernel_right {α : Type u_1} {β : Type u_2} {mα : MeasurableSpace α} {mβ : MeasurableSpace β} [MeasurableSpace.CountableOrCountablyGenerated α β] {κ η : Kernel α β} [(η : Kernel α β) → Decidable (IsSFiniteKernel η)] (h : ¬IsSFiniteKernel η) :
κ - η = 0
source
theorem ProbabilityTheory.Kernel.sub_of_isSFiniteKernel {α : 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 η
source
theorem ProbabilityTheory.Kernel.sub_apply_eq_rnDeriv_add_singularPart {α : 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
source
theorem ProbabilityTheory.Kernel.sub_apply {α : Type u_1} {β : Type u_2} {mα : MeasurableSpace α} {mβ : MeasurableSpace β} [MeasurableSpace.CountableOrCountablyGenerated α β] {κ η : Kernel α β} [(η : Kernel α β) → Decidable (IsSFiniteKernel η)] [IsFiniteKernel κ] [IsFiniteKernel η] (a : α) :
(κ - η) a = κ a - η a
source
theorem ProbabilityTheory.Kernel.le_iff {α : Type u_1} {β : Type u_2} {mα : MeasurableSpace α} {mβ : MeasurableSpace β} (κ η : Kernel α β) :
κ ≤ η ↔ ∀ (a : α), κ a ≤ η a
source
theorem ProbabilityTheory.Kernel.sub_le_self {α : Type u_1} {β : Type u_2} {mα : MeasurableSpace α} {mβ : MeasurableSpace β} [MeasurableSpace.CountableOrCountablyGenerated α β] {κ η : Kernel α β} [(η : Kernel α β) → Decidable (IsSFiniteKernel η)] [IsFiniteKernel κ] [IsFiniteKernel η] :
κ - η ≤ κ
source
instance ProbabilityTheory.Kernel.instIsFiniteKernelHSub_leanMachineLearning {α : Type u_1} {β : Type u_2} {mα : MeasurableSpace α} {mβ : MeasurableSpace β} [MeasurableSpace.CountableOrCountablyGenerated α β] {κ η : Kernel α β} [(η : Kernel α β) → Decidable (IsSFiniteKernel η)] [IsFiniteKernel κ] [IsFiniteKernel η] :
IsFiniteKernel (κ - η)
source
theorem ProbabilityTheory.Kernel.sub_apply_eq_zero_iff_le {α : Type u_1} {β : Type u_2} {mα : MeasurableSpace α} {mβ : MeasurableSpace β} [MeasurableSpace.CountableOrCountablyGenerated α β] {κ η : Kernel α β} [(η : Kernel α β) → Decidable (IsSFiniteKernel η)] [IsFiniteKernel κ] [IsFiniteKernel η] (a : α) :
(κ - η) a = 0 ↔ κ a ≤ η a
source
theorem ProbabilityTheory.Kernel.sub_eq_zero_iff_le {α : Type u_1} {β : Type u_2} {mα : MeasurableSpace α} {mβ : MeasurableSpace β} [MeasurableSpace.CountableOrCountablyGenerated α β] {κ η : Kernel α β} [(η : Kernel α β) → Decidable (IsSFiniteKernel η)] [IsFiniteKernel κ] [IsFiniteKernel η] :
κ - η = 0 ↔ κ ≤ η
source
theorem ProbabilityTheory.Kernel.measurableSet_eq_zero {α : Type u_1} {β : Type u_2} {mα : MeasurableSpace α} {mβ : MeasurableSpace β} [MeasurableSpace.CountableOrCountablyGenerated α β] (κ : Kernel α β) [IsFiniteKernel κ] :
MeasurableSet {a : α | κ a = 0}
source
theorem ProbabilityTheory.Kernel.measurableSet_eq {α : Type u_1} {β : Type u_2} {mα : MeasurableSpace α} {mβ : MeasurableSpace β} [MeasurableSpace.CountableOrCountablyGenerated α β] (κ η : Kernel α β) [IsFiniteKernel κ] [IsFiniteKernel η] :
MeasurableSet {a : α | κ a = η a}