coronalTime_strictly_increasing

formal source

  52    coronalTime (k + 1) = coronalTime k * phi := by
  53  unfold coronalTime; rw [pow_succ]; ring
  54
  55theorem coronalTime_strictly_increasing (k : ℕ) :
  56    coronalTime k < coronalTime (k + 1) := by
  57  rw [coronalTime_succ_ratio]
  58  have hk : 0 < coronalTime k := coronalTime_pos k
  59  have hphi_gt_one : (1 : ℝ) < phi := by
  60    have := Constants.phi_gt_onePointFive; linarith
  61  have : coronalTime k * 1 < coronalTime k * phi :=
  62    mul_lt_mul_of_pos_left hphi_gt_one hk
  63  simpa using this
  64
  65theorem coronal_adjacent_ratio (k : ℕ) :
  66    coronalTime (k + 1) / coronalTime k = phi := by
  67  rw [coronalTime_succ_ratio]
  68  field_simp [(coronalTime_pos k).ne']
  69
  70structure CoronalLyapunovCert where
  71  time_pos : ∀ k, 0 < coronalTime k
  72  one_step_ratio : ∀ k, coronalTime (k + 1) = coronalTime k * phi
  73  strictly_increasing : ∀ k, coronalTime k < coronalTime (k + 1)
  74  adjacent_ratio_eq_phi : ∀ k, coronalTime (k + 1) / coronalTime k = phi
  75
  76/-- Coronal Lyapunov timescale certificate. -/
  77def coronalLyapunovCert : CoronalLyapunovCert where
  78  time_pos := coronalTime_pos
  79  one_step_ratio := coronalTime_succ_ratio
  80  strictly_increasing := coronalTime_strictly_increasing
  81  adjacent_ratio_eq_phi := coronal_adjacent_ratio
  82
  83end
  84end CoronalLyapunovTime
  85end Astrophysics