`shifted_equilibrium`

proved

show as: view math explainer →

module: IndisputableMonolith.RRF.Models.Quadratic
domain: RRF
line: 100 · github
papers citing: none yet

open explainer

Read the cached plain-language explainer.

open lean source

IndisputableMonolith.RRF.Models.Quadratic on GitHub at line 100.

browse module

All declarations in this module, on Recognition.

explainer page

A cached Ask Recognition explainer exists for this declaration.

open explainer

depends on

formal source

  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 -/
 109
 110/-- The exponential transform `exp ∘ J` has the same argmin as `J`.
 111    Proof uses that exp is strictly monotone. -/
 112theorem exp_preserves_argmin (x : ℝ) :
 113    quadratic1DStrain.isMinimizer x →
 114    (∀ y, Real.exp (quadratic1DStrain.J x) ≤ Real.exp (quadratic1DStrain.J y)) := by
 115  intro hx y
 116  exact Real.exp_le_exp.mpr (hx y)
 117
 118end RRF.Models
 119end IndisputableMonolith

papers checked against this theorem

No papers in the current corpus map onto this theorem yet.