OneStepDynamics

formal source

  19noncomputable section
  20
  21/-- An abstract one-step discrete dynamics with a defect functional. -/
  22structure OneStepDynamics (α : Type) where
  23  step : α → α
  24  defect : α → ℝ
  25  defect_nonincreasing : ∀ s, defect (step s) ≤ defect s
  26
  27/-- The 8-step evolution operator. -/
  28def step8 {α : Type} (dyn : OneStepDynamics α) : α → α :=
  29  dyn.step^[8]
  30
  31/-- Iterating a one-step defect-nonincreasing map preserves defect monotonicity. -/
  32theorem iterate_defect_nonincreasing {α : Type} (dyn : OneStepDynamics α) :
  33    ∀ n s, dyn.defect ((dyn.step^[n]) s) ≤ dyn.defect s := by
  34  intro n
  35  induction n with
  36  | zero =>
  37      intro s
  38      simp
  39  | succ n ihn =>
  40      intro s
  41      rw [Function.iterate_succ_apply']
  42      exact le_trans (dyn.defect_nonincreasing ((dyn.step^[n]) s)) (ihn s)
  43
  44/-- A single 8-tick window is defect-nonincreasing. -/
  45theorem step8_defect_nonincreasing {α : Type} (dyn : OneStepDynamics α) :
  46    ∀ s, dyn.defect (step8 dyn s) ≤ dyn.defect s := by
  47  intro s
  48  simpa [step8] using iterate_defect_nonincreasing dyn 8 s
  49
  50/-- The 8-step dynamics itself is a one-step defect-nonincreasing system. -/
  51def windowDynamics {α : Type} (dyn : OneStepDynamics α) : OneStepDynamics α where
  52  step := step8 dyn