OAI/Analysis/AffineBernstein/TensorFlux.lean

GitHub source file

14 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.AffineBernstein.tangentProjectionCLM line 15
2. lemma OAI.AffineBernstein.tangentProjectionCLM_apply line 18
3. lemma OAI.AffineBernstein.inner_tangentProjection_unit line 21
4. lemma OAI.AffineBernstein.tangentProjection_self_unit line 26
5. lemma OAI.AffineBernstein.contDiffAt_projected_field line 30
6. lemma OAI.AffineBernstein.fderiv_projected_field line 35
7. def OAI.AffineBernstein.tensorFlux line 51

   Source comment

   The flux of the angular tensor acting on the projected vector field. Written in a fixed ambient basis, so no unspecified moving-frame derivatives appear.

   def tensorFlux (b : OrthonormalBasis ι ℝ E)
       (T : E → E →L[ℝ] E →L[ℝ] ℝ) (G : E → E) (q : E) : E :=
   …

8. lemma OAI.AffineBernstein.contDiffAt_tensorFlux line 56
9. lemma OAI.AffineBernstein.tensorFlux_tangent line 65
10. lemma OAI.AffineBernstein.fderiv_tensorFlux_scalar line 77
11. lemma OAI.AffineBernstein.fderiv_basis_combination line 89
12. lemma OAI.AffineBernstein.roundDivergence_basis_combination line 103
13. def OAI.AffineBernstein.roundHessianContraction line 113

    Source comment

    Intrinsic round Hessian contraction, formed from ambient derivatives and orthogonal projection. It is independent of the extension off the sphere.

    def roundHessianContraction (b : OrthonormalBasis ι ℝ E)
        (T : E → E →L[ℝ] E →L[ℝ] ℝ) (g : E → ℝ) (e : E) : ℝ :=
    …

14. lemma OAI.AffineBernstein.roundDivergence_tensorFlux line 119