OAI/Analysis/AffineBernstein/TubeSecondForm.lean

GitHub source file

8 declarations, 0 contain sorry, 0 declared as axioms

1. lemma OAI.AffineBernstein.support_tangent_identity line 17
2. def OAI.AffineBernstein.supportParam line 34

   Source comment

   Raw Gauss parametrization, before restricting the angular variable to a chart.

   def supportParam (Y : S × E → E) (q : S × E) : S × E := (q.1, Y q)

3. def OAI.AffineBernstein.supportConormal line 36
4. lemma OAI.AffineBernstein.supportParam_fderiv line 41
5. lemma OAI.AffineBernstein.supportParam_second line 49
6. lemma OAI.AffineBernstein.supportConormal_tangent line 67
7. lemma OAI.AffineBernstein.support_second_inner line 79
8. lemma OAI.AffineBernstein.supportConormal_second line 130

   Source comment

   Source (tube-second-form), as an identity of actual conormal second jets. It is valid before angular chart restriction, including the radial null line.

   lemma supportConormal_second {H : S × E → ℝ} {Y : S × E → E} {x : S × E}
       (hH : ContDiffAt ℝ ∞ H x) (hY : ContDiffAt ℝ ∞ Y x)
       (heul : H =ᶠ[𝓝 x] (fun q => inner ℝ q.2 (Y q)))
       (hgrad : ∀ᶠ q in 𝓝 x, ∀ w : E, fderiv ℝ H q (0,w) = inner ℝ (Y q) w)
       (v w : S × E) :
       supportConormal H x (fderiv ℝ (fderiv ℝ (supportParam Y)) x v w) =
         -fderiv ℝ (fderiv ℝ H) x (v.1,0) (w.1,0) +
           fderiv ℝ (fderiv ℝ H) x (0,v.2) (0,w.2) := by
   …

   Mentions: OAI.AffineBernstein.supportConormal, OAI.AffineBernstein.supportParam