OAI/Analysis/BernoulliCone/HomogeneousCalculus.lean

GitHub source file

3 declarations, 0 contain sorry, 0 declared as axioms

1. lemma OAI.Bernoulli.ConeCalculus.euler_identity line 14
2. lemma OAI.Bernoulli.ConeCalculus.hessian_radial line 29

   Source documentation

   Euler's homogeneous identity differentiated on the actual open smooth phase. No Hessian or angular equation is assumed.

   lemma hessian_radial {f : E → ℝ} {O : Set E} (hO : IsOpen O)
       (hf : ContDiffOn ℝ ∞ f O)
       (hom : ∀ r : ℝ, 0 < r → ∀ y, f (r • y) = r*f y)
       {x : E} (hx : x∈O) (v : E) :
       fderiv ℝ (fderiv ℝ f) x v x = 0 := by
   …

3. lemma OAI.Bernoulli.ConeCalculus.laplacian_trace line 49