def
definition
def or abbrev
marsAtmosphereJCostScheduleCert
show as:
view Lean formalization →
formal statement (Lean)
105def marsAtmosphereJCostScheduleCert : MarsAtmosphereJCostScheduleCert where
106 rate_zero := releaseRate_zero
proof body
Definition body.
107 rate_pos := releaseRate_pos
108 rate_succ := releaseRate_succ
109 rate_strict_mono := @releaseRate_strict_mono
110 cumulative_zero := cumulativeRelease_zero
111 cumulative_succ := cumulativeRelease_succ
112 cumulative_nonneg := cumulativeRelease_nonneg
113 cumulative_strict_mono := @cumulativeRelease_strict_mono
114
115/-- **MARS TERRAFORM ONE-STATEMENT.** Release rate ladder
116`r(n) = r_0 · φ^n`, strictly monotonic, adjacent ratio φ; cumulative
117release strictly monotonic. -/