class
definition
def or abbrev
LogModel
show as:
view Lean formalization →
formal statement (Lean)
109class LogModel (G : ℝ → ℝ) where
110 even_log : ∀ t : ℝ, G (-t) = G t
111 base0 : G 0 = 0
112 upper_cosh : ∀ t : ℝ, G t ≤ ((Real.exp t + Real.exp (-t)) / 2 - 1)
113 lower_cosh : ∀ t : ℝ, ((Real.exp t + Real.exp (-t)) / 2 - 1) ≤ G t
114
115instance (G : ℝ → ℝ) [LogModel G] : SymmUnit (F_ofLog G) :=
proof body
Definition body.
116 { symmetric := by
117 intro x hx
118 have hlog : Real.log (x⁻¹) = - Real.log x := by
119 simp
120 dsimp [F_ofLog]
121 have he : G (Real.log x) = G (- Real.log x) := by
122 simpa using (LogModel.even_log (G:=G) (Real.log x)).symm
123 simpa [hlog]
124 using he
125 , unit0 := by
126 dsimp [F_ofLog]
127 simpa [Real.log_one] using (LogModel.base0 (G:=G)) }
128
129instance (priority := 90) (G : ℝ → ℝ) [LogModel G] : JensenSketch (F_ofLog G) :=
130 JensenSketch.of_log_bounds (F:=F_ofLog G)
131 (symm := (inferInstance : SymmUnit (F_ofLog G)))
132 (upper_log := by
133 intro t
134 dsimp [F_ofLog]
135 simpa using (LogModel.upper_cosh (G:=G) t))
136 (lower_log := by
137 intro t
138 dsimp [F_ofLog]
139 simpa using (LogModel.lower_cosh (G:=G) t))
140