OAI/Analysis/AffineBernstein/ParametricFirstVariation.lean

GitHub source file

3 declarations, 0 contain sorry, 0 declared as axioms

1. lemma OAI.AffineBernstein.trace_sum_matrices line 11
2. lemma OAI.AffineBernstein.hasDerivAt_graphVariationArea_raw line 28
3. lemma OAI.AffineBernstein.hasDerivAt_graphVariationArea_normal line 71

   Source comment

   The tangential part of the exact parametrized first-variation density is an ordinary divergence; the remaining part is the genuine graph variation.

   lemma hasDerivAt_graphVariationArea_normal {n : ℕ} {Ω : Set (Space n)} (hΩ : IsOpen Ω)
       {u η : Space n → ℝ} (hu : ContDiffOn ℝ ∞ u Ω) (hη : ContDiffOn ℝ ∞ η Ω)
       {a : Fin n → Space n → ℝ} (ha : ∀ k, ContDiffOn ℝ ∞ (a k) Ω)
       {x : Space n} (hx : x ∈ Ω) (hp : (hessian u x).PosDef) :
       HasDerivAt (graphVariationArea u (verticalVariation u η a) a x)
         ((1 / ((n : ℝ) + 2)) * affineAreaDensity u x *
           (∑ i, ∑ j, (hessian u x)⁻¹ i j * hessian η x i j) +
           ∑ k, dirDeriv (coordinateVector n k) (fun y => affineAreaDensity u y * a k y) x) 0 := by
   …

   Mentions: OAI.AffineBernstein.Space, OAI.AffineBernstein.hessian, OAI.AffineBernstein.graphVariationArea, OAI.AffineBernstein.verticalVariation, OAI.AffineBernstein.affineAreaDensity, OAI.AffineBernstein.dirDeriv, OAI.AffineBernstein.coordinateVector