def
definition
F_ofLog
show as:
view math explainer →
open explainer
Read the cached plain-language explainer.
open lean source
IndisputableMonolith.Cost.JcostCore on GitHub at line 187.
browse module
All declarations in this module, on Recognition.
explainer page
depends on
used by
formal source
184 axis_upper : ∀ t : ℝ, F (Real.exp t) ≤ Jcost (Real.exp t)
185 axis_lower : ∀ t : ℝ, Jcost (Real.exp t) ≤ F (Real.exp t)
186
187noncomputable def F_ofLog (G : ℝ → ℝ) : ℝ → ℝ := fun x => G (Real.log x)
188
189class LogModel (G : ℝ → ℝ) : Prop where
190 even_log : ∀ t : ℝ, G (-t) = G t
191 base0 : G 0 = 0
192 upper_cosh : ∀ t : ℝ, G t ≤ ((Real.exp t + Real.exp (-t)) / 2 - 1)
193 lower_cosh : ∀ t : ℝ, ((Real.exp t + Real.exp (-t)) / 2 - 1) ≤ G t
194
195@[simp] theorem Jcost_agrees_on_exp : AgreesOnExp Jcost := by
196 intro t; rfl
197
198instance : AveragingAgree Jcost := ⟨Jcost_agrees_on_exp⟩
199
200instance : SymmUnit Jcost :=
201 { symmetric := by
202 intro x hx
203 simp [Jcost_symm (x:=x) hx]
204 , unit0 := Jcost_unit0 }
205
206instance : AveragingDerivation Jcost :=
207 { toSymmUnit := (inferInstance : SymmUnit Jcost)
208 , agrees := Jcost_agrees_on_exp }
209
210instance : JensenSketch Jcost :=
211 { toSymmUnit := (inferInstance : SymmUnit Jcost)
212 , axis_upper := by intro t; exact le_of_eq rfl
213 , axis_lower := by intro t; exact le_of_eq rfl }
214
215/-!
216## Small-strain Taylor expansion
217This section provides small-strain expansions used by Axiom A4.