Kernels substraction

theorem MeasureTheory.Measure.sub_le_iff_add_of_le {α : Type u_1} {mα : MeasurableSpace α} {μ ν ξ : Measure α} [IsFiniteMeasure ν] (h_le : ν ≤ μ) : μ - ν ≤ ξ ↔ μ ≤ ξ + ν

theorem MeasureTheory.Measure.sub_le_iff_add {α : Type u_1} {mα : MeasurableSpace α} {μ ν ξ : Measure α} [IsFiniteMeasure μ] [IsFiniteMeasure ν] : μ - ν ≤ ξ ↔ μ ≤ ξ + ν

theorem MeasureTheory.Measure.add_sub_of_mutuallySingular {α : Type u_1} {mα : MeasurableSpace α} {μ ν ξ : Measure α} (h : μ.MutuallySingular ξ) : μ + (ν - ξ) = μ + ν - ξ

theorem MeasureTheory.Measure.withDensity_sub_aux {α : Type u_1} {mα : MeasurableSpace α} {μ : Measure α} {f g : α → ENNReal} [IsFiniteMeasure (μ.withDensity g)] (hg : Measurable g) (hgf : g ≤ᶠ[ae μ] f) : μ.withDensity f - μ.withDensity g = μ.withDensity (f - g)

theorem MeasureTheory.Measure.withDensity_sub {α : Type u_1} {mα : MeasurableSpace α} {μ : Measure α} {f g : α → ENNReal} [IsFiniteMeasure (μ.withDensity g)] (hf : Measurable f) (hg : Measurable g) : μ.withDensity f - μ.withDensity g = μ.withDensity (f - g)

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

noncomputable instance ProbabilityTheory.Kernel.instSubOfDecidableIsSFiniteKernel_leanBandits {α : 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.

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

@[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

@[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

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 η

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

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

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

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

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

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

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 ↔ κ ≤ η

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

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