OAI/Analysis/AffineBernstein/SphereTensorCalculus.lean

GitHub source file

5 declarations, 0 contain sorry, 0 declared as axioms

1. lemma OAI.AffineBernstein.fderiv_bilinear_field line 16
2. lemma OAI.AffineBernstein.radial_tensor_derivative line 29

   Source comment

   Derivatives of the radial eigenspace remain radial in the radial direction. The polynomial identity avoids differentiating an arbitrarily chosen eigenvalue.

   lemma radial_tensor_derivative {T : E → E →L[ℝ] E →L[ℝ] ℝ} {e v : E}
       (hT : DifferentiableAt ℝ T e) (he : inner ℝ e e = 1) (hv : inner ℝ e v = 0)
       (hr : ∀ᶠ q in 𝓝 e, T q q v * inner ℝ q q = T q q q * inner ℝ q v) :
       fderiv ℝ T e e e v = 0 := by
   …

3. lemma OAI.AffineBernstein.roundTensorDerivative_eq_of_radial line 65
4. lemma OAI.AffineBernstein.trace_projected_bilinear line 84
5. theorem OAI.AffineBernstein.projected_tensor_divergence line 109

   Source comment

   Tangential divergence of the restricted Newton tensor. Both normal corrections vanish by genuine radial invariance, not as an IBP assumption.

   theorem projected_tensor_divergence (b : OrthonormalBasis ι ℝ E)
       {T : E → E →L[ℝ] E →L[ℝ] ℝ} {e v : E}
       (hT : DifferentiableAt ℝ T e) (he : inner ℝ e e = 1) (hv : inner ℝ e v = 0)
       (hs : ∀ u w, T e u w = T e w u)
       (hr : ∀ᶠ q in 𝓝 e, ∀ w, T q q w * inner ℝ q q = T q q q * inner ℝ q w)
       (hdiv : ∀ w, (∑ i, fderiv ℝ T e (b i) (b i) w) = 0) :
       (∑ i, roundTensorDerivative T e (tangentProjection e (b i))
         (tangentProjection e (b i)) v) = 0 := by
   …

   Mentions: OAI.AffineBernstein.roundTensorDerivative, OAI.AffineBernstein.tangentProjection