Flog_eq_Jlog

formal source

  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
  74
  75lemma Flog_eq_zero_iff_of_derivation {F : ℝ → ℝ} [AveragingDerivation F] (t : ℝ) :
  76  Flog F t = 0 ↔ t = 0 := by
  77  have := Jlog_eq_zero_iff t
  78  simpa [Flog_eq_Jlog_pt (F:=F) t] using this
  79
  80theorem T5_EL_equiv_general {F : ℝ → ℝ} [AveragingDerivation F] :
  81  deriv (Flog F) 0 = 0 ∧ (∀ t : ℝ, Flog F 0 ≤ Flog F t) ∧ (∀ t : ℝ, Flog F t = 0 ↔ t = 0) := by
  82  refine ⟨deriv_Flog_zero_of_derivation (F:=F), ?_, ?_⟩
  83  · intro t; exact Flog_nonneg_of_derivation (F:=F) t
  84  · intro t; exact Flog_eq_zero_iff_of_derivation (F:=F) t