def
definition
AgreesOnExp
show as:
view math explainer →
open explainer
Generate a durable explainer page for this declaration.
open lean source
IndisputableMonolith.Cost on GitHub at line 34.
browse module
All declarations in this module, on Recognition.
explainer page
depends on
used by
formal source
31 rw [Jcost_eq_sq hx0]
32 positivity
33
34def AgreesOnExp (F : ℝ → ℝ) : Prop := ∀ t : ℝ, F (Real.exp t) = Jcost (Real.exp t)
35
36@[simp] lemma Jcost_exp (t : ℝ) :
37 Jcost (Real.exp t) = ((Real.exp t) + (Real.exp (-t))) / 2 - 1 := by
38 have h : (Real.exp t)⁻¹ = Real.exp (-t) := by
39 symm; simp [Real.exp_neg t]
40 simp [Jcost, h]
41
42class SymmUnit (F : ℝ → ℝ) : Prop where
43 symmetric : ∀ {x}, 0 < x → F x = F x⁻¹
44 unit0 : F 1 = 0
45
46class AveragingAgree (F : ℝ → ℝ) : Prop where
47 agrees : AgreesOnExp F
48
49class AveragingDerivation (F : ℝ → ℝ) : Prop extends SymmUnit F where
50 agrees : AgreesOnExp F
51
52lemma even_on_log_of_symm {F : ℝ → ℝ} [SymmUnit F] (t : ℝ) :
53 F (Real.exp t) = F (Real.exp (-t)) := by
54 have hx : 0 < Real.exp t := Real.exp_pos t
55 simpa [Real.exp_neg] using (SymmUnit.symmetric (F:=F) hx)
56
57class AveragingBounds (F : ℝ → ℝ) : Prop extends SymmUnit F where
58 upper : ∀ t : ℝ, F (Real.exp t) ≤ Jcost (Real.exp t)
59 lower : ∀ t : ℝ, Jcost (Real.exp t) ≤ F (Real.exp t)
60
61theorem agrees_on_exp_of_bounds {F : ℝ → ℝ} [AveragingBounds F] :
62 AgreesOnExp F := by
63 intro t
64 have h₁ := AveragingBounds.upper (F:=F) t