def
definition
AgreesOnExp
show as:
view math explainer →
open explainer
Read the cached plain-language explainer.
open lean source
IndisputableMonolith.Cost.JcostCore on GitHub at line 154.
browse module
All declarations in this module, on Recognition.
explainer page
depends on
used by
formal source
151 simpa [hsq, pow_two] using this
152 exact (hineq.trans hcompare)
153
154def AgreesOnExp (F : ℝ → ℝ) : Prop := ∀ t : ℝ, F (Real.exp t) = Jcost (Real.exp t)
155
156@[simp] lemma Jcost_exp (t : ℝ) :
157 Jcost (Real.exp t) = ((Real.exp t) + (Real.exp (-t))) / 2 - 1 := by
158 have h : (Real.exp t)⁻¹ = Real.exp (-t) := by
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)