class
definition
SymmUnit
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 162.
browse module
All declarations in this module, on Recognition.
explainer page
depends on
used by
formal source
159 symm; simp [Real.exp_neg t]
160 simp [Jcost, h]
161
162class SymmUnit (F : ℝ → ℝ) : Prop where
163 symmetric : ∀ {x}, 0 < x → F x = F x⁻¹
164 unit0 : F 1 = 0
165
166class AveragingAgree (F : ℝ → ℝ) : Prop where
167 agrees : AgreesOnExp F
168
169class AveragingDerivation (F : ℝ → ℝ) : Prop extends SymmUnit F where
170 agrees : AgreesOnExp F
171
172class AveragingBounds (F : ℝ → ℝ) : Prop extends SymmUnit F where
173 upper : ∀ t : ℝ, F (Real.exp t) ≤ Jcost (Real.exp t)
174 lower : ∀ t : ℝ, Jcost (Real.exp t) ≤ F (Real.exp t)
175
176def mkAveragingBounds (F : ℝ → ℝ)
177 (symm : SymmUnit F)
178 (upper : ∀ t : ℝ, F (Real.exp t) ≤ Jcost (Real.exp t))
179 (lower : ∀ t : ℝ, Jcost (Real.exp t) ≤ F (Real.exp t)) :
180 AveragingBounds F :=
181{ toSymmUnit := symm, upper := upper, lower := lower }
182
183class JensenSketch (F : ℝ → ℝ) : Prop extends SymmUnit F where
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)