structure
definition
LiftingProgramCert
show as:
view math explainer →
open explainer
Generate a durable explainer page for this declaration.
open lean source
IndisputableMonolith.Sport.LiftingProgramDesign on GitHub at line 69.
browse module
All declarations in this module, on Recognition.
explainer page
depends on
used by
formal source
66 mul_lt_mul_of_pos_left hphi_inv_lt_one hk
67 simpa using this
68
69structure LiftingProgramCert where
70 intensity_pos : ∀ k, 0 < intensityAtRung k
71 one_step_ratio :
72 ∀ k, intensityAtRung (k + 1) = intensityAtRung k * phi⁻¹
73 strictly_decreasing :
74 ∀ k, intensityAtRung (k + 1) < intensityAtRung k
75
76/-- Lifting-program-design certificate. -/
77def liftingProgramCert : LiftingProgramCert where
78 intensity_pos := intensityAtRung_pos
79 one_step_ratio := intensityAtRung_succ_ratio
80 strictly_decreasing := intensityAtRung_strictly_decreasing
81
82end
83end LiftingProgramDesign
84end Sport
85end IndisputableMonolith