class
definition
AveragingDerivation
show as:
view math explainer →
open explainer
Read the cached plain-language explainer.
open lean source
IndisputableMonolith.Cost.JcostCore on GitHub at line 169.
browse module
All declarations in this module, on Recognition.
explainer page
depends on
used by
formal source
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)
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