OAI/Analysis/AffineBernstein/JointAngularCalculus.lean

GitHub source file

13 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.AffineBernstein.jointAngularGradient line 18

   Source comment

   Partial fiber gradient, represented through the derivative of the joint scalar.

   def jointAngularGradient (g : S × E → ℝ) (q : S × E) : E :=
   …

2. lemma OAI.AffineBernstein.jointAngularGradient_eq_slice line 21
3. lemma OAI.AffineBernstein.contDiffAt_jointAngularGradient line 31
4. def OAI.AffineBernstein.jointAngularHessianVec line 37

   Source comment

   Partial angular derivative of the gradient, represented without slice-dependent differentiation.

   def jointAngularHessianVec (g : S × E → ℝ) (q : S × E) (v : E) : E :=
   …

5. lemma OAI.AffineBernstein.jointAngularHessianVec_eq_slice line 41
6. lemma OAI.AffineBernstein.contDiffAt_jointAngularHessianVec line 50
7. def OAI.AffineBernstein.jointNewtonTensor line 57
8. lemma OAI.AffineBernstein.jointNewtonTensor_eq_slice line 60
9. lemma OAI.AffineBernstein.contDiffAt_jointNewtonTensor line 68
10. lemma OAI.AffineBernstein.continuousOn_sliceAngularGradient line 77
11. lemma OAI.AffineBernstein.continuousOn_sliceNewtonTensor line 86
12. lemma OAI.AffineBernstein.contDiffAt_tangentProjection line 96
13. lemma OAI.AffineBernstein.continuousOn_sliceRoundContraction line 101