structure
definition
MeasureTheoryCert
show as:
view math explainer →
open explainer
Read the cached plain-language explainer.
open lean source
IndisputableMonolith.Mathematics.MeasureTheoryFromRS on GitHub at line 36.
browse module
All declarations in this module, on Recognition.
explainer page
depends on
used by
formal source
33 · rw [h, Jcost_unit0]
34 · exact le_of_lt (Jcost_pos_of_ne_one r hr h)
35
36structure MeasureTheoryCert where
37 five_measures : Fintype.card CanonicalMeasure = 5
38 jcost_nonneg : ∀ {r : ℝ}, 0 < r → 0 ≤ Jcost r
39
40def measureTheoryCert : MeasureTheoryCert where
41 five_measures := canonicalMeasureCount
42 jcost_nonneg := jcost_measurable
43
44end IndisputableMonolith.Mathematics.MeasureTheoryFromRS