LeanMachineLearning exposition

ProbabilityTheory.Kernel.instSubOfDecidableIsSFiniteKernel_leanMachineLearning🔗

Minimal Lean file

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