LeanMachineLearning exposition

ProbabilityTheory.instSubFiniteMeasure_leanMachineLearning🔗

Minimal Lean file

instSubFiniteMeasure_leanMachineLearning🔗

InstanceProbabilityTheory.instSubFiniteMeasure_leanMachineLearning
Details

No docstring.

🔗def
ProbabilityTheory.instSubFiniteMeasure_leanMachineLearning.{u_1}
  {α : Type u_1} {mα : MeasurableSpace α} :
  Sub (MeasureTheory.FiniteMeasure α)
ProbabilityTheory.instSubFiniteMeasure_leanMachineLearning.{u_1}
  {α : Type u_1}
  {mα : MeasurableSpace α} :
  Sub (MeasureTheory.FiniteMeasure α)

Code

noncomputable
instance : Sub (FiniteMeasure α)
Used by (4)

Actions: Source · Open Issue

Proof
⟨fun μ ν ↦ ⟨μ.toMeasure - ν.toMeasure, inferInstance⟩⟩