LeanMachineLearning exposition

ProbabilityTheory.instOrderedSubFiniteMeasure_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

instOrderedSubFiniteMeasure_leanMachineLearning🔗

InstanceProbabilityTheory.instOrderedSubFiniteMeasure_leanMachineLearning
Details

No docstring.

🔗theorem
ProbabilityTheory.instOrderedSubFiniteMeasure_leanMachineLearning.{u_1}
  {α : Type u_1} {mα : MeasurableSpace α} :
  OrderedSub (MeasureTheory.FiniteMeasure α)
ProbabilityTheory.instOrderedSubFiniteMeasure_leanMachineLearning.{u_1}
  {α : Type u_1}
  {mα : MeasurableSpace α} :
  OrderedSub
    (MeasureTheory.FiniteMeasure α)

Code

instance : OrderedSub (FiniteMeasure α) where
  tsub_le_iff_right μ ν ξ
Type uses (2)
Body uses (1)

Actions: Source · Open Issue

Proof
by
    simp only [FiniteMeasure.le_iff_coe, FiniteMeasure.toMeasure_sub, FiniteMeasure.toMeasure_add]
    exact Measure.sub_le_iff_le_add

Dependency graph

Type dependencies (2)

instPartialOrderFiniteMeasure_leanMachineLearning🔗

InstanceProbabilityTheory.instPartialOrderFiniteMeasure_leanMachineLearning
Details

No docstring.

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

Code

instance : PartialOrder (FiniteMeasure α)
Used by (3)

Actions: Source · Open Issue

Proof
PartialOrder.lift _ FiniteMeasure.toMeasure_injective

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⟩⟩

All dependencies, transitively (1)

le_iff_coe🔗

LemmaProbabilityTheory.FiniteMeasure.le_iff_coe
Details

No docstring.

🔗theorem
ProbabilityTheory.FiniteMeasure.le_iff_coe.{u_1} {α : Type u_1}
  {mα : MeasurableSpace α} {μ ν : MeasureTheory.FiniteMeasure α} :
  μ ≤ ν ↔ ↑μ ≤ ↑ν
ProbabilityTheory.FiniteMeasure.le_iff_coe.{u_1}
  {α : Type u_1} {mα : MeasurableSpace α}
  {μ ν : MeasureTheory.FiniteMeasure α} :
  μ ≤ ν ↔ ↑μ ≤ ↑ν

Code

lemma FiniteMeasure.le_iff_coe {μ ν : FiniteMeasure α} :
    μ ≤ ν ↔ (μ : Measure α) ≤ (ν : Measure α)
Type uses (1)
Used by (2)

Actions: Source · Open Issue

Proof
Iff.rfl