OAI/Analysis/AffineBernstein/ParametricVariationAlgebra.lean

GitHub source file

11 declarations, 0 contain sorry, 0 declared as axioms

1. lemma OAI.AffineBernstein.contDiff_adjugate_entry line 13
2. lemma OAI.AffineBernstein.contDiffAt_inverse_matrix_entry line 28
3. lemma OAI.AffineBernstein.hasDerivAt_det_entries line 35
4. def OAI.AffineBernstein.variationConormal line 56

   Source comment

   The conormal for the genuine variation (x+t a(x),u(x)+t beta(x)), written in its first jets, is (-q(t),1).

   def variationConormal (D : Matrix ι ι ℝ) (g d : ι → ℝ) (t : ℝ) (k : ι) : ℝ :=
   …

5. def OAI.AffineBernstein.variationSecondForm line 61

   Source comment

   The second form for that conormal. H,B are the Hessians of u,beta; C k is the Hessian of the kth horizontal displacement.

   def variationSecondForm (H B D : Matrix ι ι ℝ) (g d : ι → ℝ)
       (C : ι → Matrix ι ι ℝ) (t : ℝ) : Matrix ι ι ℝ :=
   …

6. def OAI.AffineBernstein.variationAreaDensity line 65
7. lemma OAI.AffineBernstein.variationConormal_zero line 70
8. lemma OAI.AffineBernstein.variationSecondForm_zero line 74
9. lemma OAI.AffineBernstein.contDiffAt_variationConormal line 78
10. lemma OAI.AffineBernstein.hasDerivAt_variationSecondForm line 90
11. lemma OAI.AffineBernstein.hasDerivAt_variationAreaDensity_raw line 103