OAI/Analysis/AffineBernstein/TubeDensityVariation.lean

GitHub source file

8 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.AffineBernstein.tubeAreaDensity line 16
2. lemma OAI.AffineBernstein.hasDerivAt_tubeAreaDensity line 21

   Source comment

   Literal Jacobi first variation of the tube density, including empty angular matrices. This is the integrand needed in source (tube-euler).

   lemma hasDerivAt_tubeAreaDensity (B D : Matrix ι ι ℝ) (R T : Matrix κ κ ℝ)
       (hB : B.PosDef) (hR : R.PosDef) (δ : ℝ) :
       HasDerivAt (fun t : ℝ => tubeAreaDensity (B + t • D) (R + t • T) δ)
         (δ * Real.rpow B.det (δ-1) * Real.rpow R.det (1-δ) *
           (∑ i, ∑ j, B.adjugate j i * D i j) +
          (1-δ) * Real.rpow B.det δ * Real.rpow R.det (-δ) *
           (∑ i, ∑ j, R.adjugate j i * T i j)) 0 := by
   …

   Mentions: OAI.AffineBernstein.tubeAreaDensity

3. lemma OAI.AffineBernstein.second_fderiv_affine_comp line 42
4. lemma OAI.AffineBernstein.second_fderiv_prod_left line 56
5. lemma OAI.AffineBernstein.second_fderiv_prod_right line 62
6. lemma OAI.AffineBernstein.bilinear_matrix_posDef line 68
7. lemma OAI.AffineBernstein.tubeBaseMatrix_posDef line 88
8. lemma OAI.AffineBernstein.tubeRadiusMatrix_posDef line 106