AveragingDerivation

formal source

  40  simpa [heq]
  41
  42/-- Typeclass for averaging derivation -/
  43class AveragingDerivation (F : ℝ → ℝ) : Prop extends SymmUnit F where
  44  agrees : ∀ t : ℝ, F (Real.exp t) = Jcost (Real.exp t)
  45
  46/-- Flog definition -/
  47noncomputable def Flog (F : ℝ → ℝ) (t : ℝ) : ℝ := F (Real.exp t)
  48
  49lemma Flog_eq_Jlog_pt {F : ℝ → ℝ} [AveragingDerivation F] (t : ℝ) :
  50  Flog F t = Jlog t := by
  51  dsimp [Flog, Jlog]
  52  exact AveragingDerivation.agrees t
  53
  54lemma Flog_eq_Jlog {F : ℝ → ℝ} [AveragingDerivation F] :
  55  (fun t => Flog F t) = Jlog := by
  56  funext t; simpa using (Flog_eq_Jlog_pt (F:=F) t)
  57
  58lemma hasDerivAt_Flog_of_derivation {F : ℝ → ℝ} [AveragingDerivation F] (t : ℝ) :
  59  HasDerivAt (Flog F) (Real.sinh t) t := by
  60  have h := hasDerivAt_Jlog t
  61  have hfun := (Flog_eq_Jlog (F:=F))
  62  -- rewrite derivative of Jlog to derivative of Flog via function equality
  63  simpa [hfun] using h
  64
  65@[simp] lemma deriv_Flog_zero_of_derivation {F : ℝ → ℝ} [AveragingDerivation F] :
  66  deriv (Flog F) 0 = 0 := by
  67  classical
  68  simpa using (hasDerivAt_Flog_of_derivation (F:=F) 0).deriv
  69
  70lemma Flog_nonneg_of_derivation {F : ℝ → ℝ} [AveragingDerivation F] (t : ℝ) :
  71  0 ≤ Flog F t := by
  72  have := Jlog_nonneg t
  73  simpa [Flog_eq_Jlog_pt (F:=F) t] using this