structure
definition
def or abbrev
FiniteDescriptionRegularity
show as:
view Lean formalization →
formal statement (Lean)
86structure FiniteDescriptionRegularity (J : ℝ → ℝ) : Prop where
87 continuity : ContinuityFromFiniteDescription J
88 convexity : StrictConvexityFromClosure J
89 calibration : CalibrationFromUnitChoice J
90
91/-- Fold the split finite-description obligations back into the legacy bundle. -/
92def FiniteDescriptionRegularity.toRegularityCert {J : ℝ → ℝ}
93 (h : FiniteDescriptionRegularity J) : RegularityCert J where
94 continuous := h.continuity.continuous
proof body
Definition body.
95 strict_convex := h.convexity.strict_convex
96 calibration := h.calibration.calibration
97
98/-- Unfold the legacy regularity bundle into the split obligations. -/
99def RegularityCert.toFiniteDescriptionRegularity {J : ℝ → ℝ}
100 (h : RegularityCert J) : FiniteDescriptionRegularity J where
101 continuity := ⟨h.continuous⟩
102 convexity := ⟨h.strict_convex⟩
103 calibration := ⟨h.calibration⟩
104
105/-- **R6 as theorem**: Compositional closure follows from continuity.
106If J is continuous on R_{>0}, then J(xy) + J(x/y) is finite. -/