GrowthFactorCert

formal source

 127
 128/-! ## Certificate -/
 129
 130structure GrowthFactorCert where
 131  D_positive : ∀ a k tau0 : ℝ, 0 < a → 0 < k → 0 < tau0 → 0 < D_growth a k tau0
 132  D_ge_a : ∀ a k tau0 : ℝ, 0 < a → 0 < k → 0 < tau0 → a ≤ D_growth a k tau0
 133  f_gt_one : ∀ a k tau0 : ℝ, 0 < a → 0 < k → 0 < tau0 → 1 < f_growth a k tau0
 134  beta_positive : ∀ k tau0 : ℝ, 0 < k → 0 < tau0 → 0 < beta_growth k tau0
 135
 136theorem growth_factor_cert : GrowthFactorCert where
 137  D_positive := D_growth_pos
 138  D_ge_a := D_growth_ge_a
 139  f_gt_one := f_growth_gt_one
 140  beta_positive := beta_growth_pos
 141
 142end
 143
 144end ILGGrowthFactor
 145end Gravity
 146end IndisputableMonolith