lemma proved term proof

`phi_hasDerivAt`

No prose has been written for this declaration yet. The Lean source and graph data below render without it.

formal statement (Lean)

 100private lemma phi_hasDerivAt (H : ℝ → ℝ) (h_cont : Continuous H) (t : ℝ) :
 101    HasDerivAt (Phi H) (H t) t :=

proof body

Term-mode proof.

 102  intervalIntegral.integral_hasDerivAt_right (h_cont.intervalIntegrable 0 t)
 103    h_cont.aestronglyMeasurable.stronglyMeasurableAtFilter h_cont.continuousAt
 104

used by (9)

From the project-wide theorem graph. These declarations reference this one in their body.

deriv_phi_eq in IndisputableMonolith.Cost.AczelProof decl_use
exists_integral_ne_zero in IndisputableMonolith.Cost.AczelProof decl_use
phi_differentiable in IndisputableMonolith.Cost.AczelProof decl_use
phi_hasDerivAt in IndisputableMonolith.Cost.AczelProof decl_use
representation_formula in IndisputableMonolith.Cost.AczelProof decl_use
deriv_phi_eq in IndisputableMonolith.Cost.AczelTheorem decl_use
exists_integral_ne_zero in IndisputableMonolith.Cost.AczelTheorem decl_use
phi_differentiable in IndisputableMonolith.Cost.AczelTheorem decl_use
representation_formula in IndisputableMonolith.Cost.AczelTheorem decl_use

depends on (5)

Lean names referenced from this declaration's body.

H in IndisputableMonolith.Algebra.CostAlgebra decl_use
Phi in IndisputableMonolith.Cost.AczelProof decl_use
phi_hasDerivAt in IndisputableMonolith.Cost.AczelProof decl_use
Phi in IndisputableMonolith.Cost.AczelTheorem decl_use
H in IndisputableMonolith.Cost.FunctionalEquation decl_use