lyapunovAt_pos

formal source

  34numerical heating = smaller exponent). -/
  35def lyapunovAt (k : ℕ) : ℝ := referenceExponent * phi ^ (-(k : ℤ))
  36
  37theorem lyapunovAt_pos (k : ℕ) : 0 < lyapunovAt k := by
  38  unfold lyapunovAt referenceExponent
  39  have : 0 < phi ^ (-(k : ℤ)) := zpow_pos Constants.phi_pos _
  40  linarith [this]
  41
  42theorem lyapunovAt_succ_ratio (k : ℕ) :
  43    lyapunovAt (k + 1) = lyapunovAt k * phi⁻¹ := by
  44  unfold lyapunovAt
  45  have hphi_ne : phi ≠ 0 := Constants.phi_ne_zero
  46  have : phi ^ (-((k : ℤ) + 1)) = phi ^ (-(k : ℤ)) * phi⁻¹ := by
  47    rw [show (-((k : ℤ) + 1)) = -(k : ℤ) + (-1 : ℤ) by ring]
  48    rw [zpow_add₀ hphi_ne]; simp
  49  have hcast : ((k + 1 : ℕ) : ℤ) = (k : ℤ) + 1 := by push_cast; ring
  50  rw [hcast, this]; ring
  51
  52theorem lyapunovAt_adjacent_ratio (k : ℕ) :
  53    lyapunovAt (k + 1) / lyapunovAt k = phi⁻¹ := by
  54  rw [lyapunovAt_succ_ratio]
  55  field_simp [(lyapunovAt_pos k).ne']
  56
  57structure PICLyapunovCert where
  58  lyapunov_pos : ∀ k, 0 < lyapunovAt k
  59  one_step_ratio : ∀ k, lyapunovAt (k + 1) = lyapunovAt k * phi⁻¹
  60  adjacent_ratio : ∀ k, lyapunovAt (k + 1) / lyapunovAt k = phi⁻¹
  61
  62/-- PIC-simulation Lyapunov certificate. -/
  63def picLyapunovCert : PICLyapunovCert where
  64  lyapunov_pos := lyapunovAt_pos
  65  one_step_ratio := lyapunovAt_succ_ratio
  66  adjacent_ratio := lyapunovAt_adjacent_ratio
  67