LeanMachineLearning exposition

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

instCanonicallyOrderedAddFiniteMeasure_leanMachineLearning🔗

InstanceProbabilityTheory.instCanonicallyOrderedAddFiniteMeasure_leanMachineLearning
Details

No docstring.

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

Code

instance : CanonicallyOrderedAdd (FiniteMeasure α) where
  le_add_self μ ν
Type uses (1)
Body uses (3)

Actions: Source · Open Issue

Proof
fun s ↦ by simp
  exists_add_of_le {μ ν} hμν := by
    refine ⟨ν - μ, ?_⟩
    rw [FiniteMeasure.ext_iff_coe]
    simp only [FiniteMeasure.toMeasure_add, FiniteMeasure.toMeasure_sub]
    rw [add_comm, Measure.sub_add_cancel_of_le hμν]
  le_self_add μ ν := by
    simp only [FiniteMeasure.le_iff_coe, FiniteMeasure.toMeasure_add]
    exact Measure.le_add_right le_rfl

Dependency graph

Type dependencies (1)

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

All dependencies, transitively (3)

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

ext_iff_coe🔗

LemmaProbabilityTheory.FiniteMeasure.ext_iff_coe
Details

No docstring.

🔗theorem
ProbabilityTheory.FiniteMeasure.ext_iff_coe.{u_7} {α : Type u_7}
  {mα : MeasurableSpace α} {μ ν : MeasureTheory.FiniteMeasure α} :
  μ = ν ↔ ↑μ = ↑ν
ProbabilityTheory.FiniteMeasure.ext_iff_coe.{u_7}
  {α : Type u_7} {mα : MeasurableSpace α}
  {μ ν : MeasureTheory.FiniteMeasure α} :
  μ = ν ↔ ↑μ = ↑ν

Code

lemma FiniteMeasure.ext_iff_coe {α : Type*} {mα : MeasurableSpace α} {μ ν : FiniteMeasure α} :
    μ = ν ↔ (μ : Measure α) = ν
Used by (1)

Actions: Source · Open Issue

Proof
Subtype.ext_iff

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