quadratic1DOctave

formal source

  75  quality := fun x => x ^ 2
  76
  77/-- The 1D quadratic octave. -/
  78def quadratic1DOctave : Octave where
  79  State := ℝ
  80  strain := quadratic1DStrain
  81  channels := {
  82    Index := Unit
  83    Obs := fun _ => ℝ
  84    channel := fun _ => quadratic1DChannel
  85  }
  86  inhabited := ⟨0⟩
  87
  88theorem quadratic1DOctave_wellPosed : quadratic1DOctave.wellPosed :=
  89  ⟨(0 : ℝ), quadratic1D_equilibrium⟩
  90
  91/-! ## Shifted Quadratic (demonstrates argmin invariance) -/
  92
  93/-- Shifted quadratic: J(x) = (x - a)² with minimum at a. -/
  94def shiftedQuadraticStrain (a : ℝ) : StrainFunctional ℝ where
  95  J := fun x => (x - a) ^ 2
  96
  97instance (a : ℝ) : StrainFunctional.NonNeg (shiftedQuadraticStrain a) where
  98  nonneg := fun x => sq_nonneg (x - a)
  99
 100theorem shifted_equilibrium (a : ℝ) : (shiftedQuadraticStrain a).isBalanced a := by
 101  simp [StrainFunctional.isBalanced, shiftedQuadraticStrain]
 102
 103theorem shifted_is_minimizer (a : ℝ) : (shiftedQuadraticStrain a).isMinimizer a := by
 104  intro y
 105  simp [StrainFunctional.weaklyBetter, shiftedQuadraticStrain]
 106  exact sq_nonneg (y - a)
 107
 108/-! ## Quadratic demonstrates monotone argmin invariance -/