def
definition
F_ofLog
show as:
view math explainer →
open explainer
Generate a durable explainer page for this declaration.
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.