 106
 107noncomputable def F_ofLog (G : ℝ → ℝ) : ℝ → ℝ := fun x => G (Real.log x)
 108
 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) :=
 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))

papers checked against this theorem

No papers in the current corpus map onto this theorem yet.