LeanMachineLearning exposition

ProbabilityTheory.Kernel.instIsFiniteKernelHSub_leanMachineLearning🔗

This page has the declaration's own card below, then its dependency graph, then a card for each dependency (type dependencies first, then the rest of the transitive closure). For a theorem, the graph and the dependency cards only follow its statement's dependencies (its proof is replaced by sorry, so what it proves doesn't depend on how); for everything else, both the type and the body/value are followed, since their content is part of what later declarations build on.

Minimal Lean file

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

Dependency graph

Type dependencies (1)

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

All dependencies, transitively (1)

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