OAI/Analysis/AffineBernstein/BilinearNewton.lean

GitHub source file

19 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.AffineBernstein.bilinearOfMatrix line 18
2. lemma OAI.AffineBernstein.bilinearOfMatrix_apply line 24
3. lemma OAI.AffineBernstein.bilinearOfMatrix_basis line 29
4. lemma OAI.AffineBernstein.bilinearOfMatrix_symm line 35
5. lemma OAI.AffineBernstein.bilinearOfMatrix_radial line 48
6. lemma OAI.AffineBernstein.contDiffAt_bilinearOfMatrix line 64
7. lemma OAI.AffineBernstein.fderiv_bilinearOfMatrix_basis line 72
8. lemma OAI.AffineBernstein.bilinearOfMatrix_field_divergence line 84
9. def OAI.AffineBernstein.basisHessian line 99

   Source comment

   Full ambient Hessian in a constant orthonormal basis.

   def basisHessian (b : OrthonormalBasis ι ℝ E) (H : E → ℝ) (x : E) : Matrix ι ι ℝ :=
   …

10. lemma OAI.AffineBernstein.contDiffAt_basisHessian line 103
11. lemma OAI.AffineBernstein.basisHessian_isSymm line 109
12. lemma OAI.AffineBernstein.fderiv_basisHessian line 115
13. lemma OAI.AffineBernstein.basisHessian_codazzi line 125
14. def OAI.AffineBernstein.supportNewtonTensor line 140

    Source comment

    Global polynomial tensor whose tangential restriction is the angular cofactor.

    def supportNewtonTensor (b : OrthonormalBasis ι ℝ E) (H : E → ℝ) (x : E) :
        E →L[ℝ] E →L[ℝ] ℝ := bilinearOfMatrix b (newtonTensor (basisHessian b H x))

    Mentions: OAI.AffineBernstein.bilinearOfMatrix, OAI.AffineBernstein.newtonTensor, OAI.AffineBernstein.basisHessian

15. lemma OAI.AffineBernstein.contDiffAt_supportNewtonTensor line 143
16. lemma OAI.AffineBernstein.supportNewtonTensor_isSymm line 151
17. lemma OAI.AffineBernstein.supportNewtonTensor_flat_divergence line 156
18. lemma OAI.AffineBernstein.supportNewtonTensor_radial line 167
19. theorem OAI.AffineBernstein.supportNewtonTensor_round_divergence line 184

    Source comment

    The genuinely differentiated angular divergence identity for a smooth one-homogeneous support extension. Its only analytic input is the actual radial Hessian identity; flat Piola and both normal cancellations are proved.

    theorem supportNewtonTensor_round_divergence (b : OrthonormalBasis ι ℝ E)
        {U : Set E} (hU : IsOpen U) {H : E → ℝ} (hH : ContDiffOn ℝ ∞ H U)
        (hr : ∀ q ∈ U, ∀ v, fderiv ℝ (fderiv ℝ H) q v q = 0)
        {e v : E} (heU : e ∈ U) (he : inner ℝ e e = 1) (hv : inner ℝ e v = 0) :
        (∑ i, roundTensorDerivative (supportNewtonTensor b H) e
          (tangentProjection e (b i)) (tangentProjection e (b i)) v) = 0 := by
    …

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