  25  | lebesgue | counting | dirac | hausdorff | borel
  26  deriving DecidableEq, Repr, BEq, Fintype
  27
  28theorem canonicalMeasureCount : Fintype.card CanonicalMeasure = 5 := by decide
  29
  30/-- J-cost is non-negative (measure-compatible). -/
  31theorem jcost_measurable {r : ℝ} (hr : 0 < r) : 0 ≤ Jcost r := by
  32  by_cases h : r = 1
  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

papers checked against this theorem

No papers in the current corpus map onto this theorem yet.