NormalizedJetCorrection.lean`

6 declarations, 0 contain sorry, 0 declared as axioms

Second jets of radial normalization, for the finite-point flattening of the starting spherical immersion.

def OAI.ClosedSurfaceR4.SphericalJets.radialNormalize line 14
Source documentation
Radial normalization is kept as an actual map of Euclidean four-space.
```
def radialNormalize (x : Space) : Space := ‖x‖⁻¹ • x
```
Mentions: OAI.ClosedSurfaceR4.SphericalJets.Space
lemma OAI.ClosedSurfaceR4.SphericalJets.radialNormalize_smoothAt line 16
lemma OAI.ClosedSurfaceR4.SphericalJets.radialNormalize_fderiv_unit line 20
lemma OAI.ClosedSurfaceR4.SphericalJets.secondDerivative_apply line 33
lemma OAI.ClosedSurfaceR4.SphericalJets.secondDerivative_comp line 41

theorem OAI.ClosedSurfaceR4.SphericalJets.radialNormalize_second_jet_difference line 71

Source documentation

Maps with identical value and first derivative differ after radial normalization by the differential of normalization applied to their second-jet difference.

theorem radialNormalize_second_jet_difference {F G : Plane → Space}
    (hF : ContDiff ℝ ∞ F) (hG : ContDiff ℝ ∞ G) (p v w : Plane)
    (hFp : ‖F p‖ = 1) (hvalue : G p = F p)
    (hfirst : fderiv ℝ G p = fderiv ℝ F p) :
    fderiv ℝ (fderiv ℝ (radialNormalize ∘ G)) p v w -
      fderiv ℝ (fderiv ℝ (radialNormalize ∘ F)) p v w =
    (fderiv ℝ (fderiv ℝ G) p v w - fderiv ℝ (fderiv ℝ F) p v w) -
      inner ℝ (F p) (fderiv ℝ (fderiv ℝ G) p v w - fderiv ℝ (fderiv ℝ F) p v w) • F p := by
…

Mentions: OAI.ClosedSurfaceR4.SphericalJets.Plane, OAI.ClosedSurfaceR4.SphericalJets.Space, OAI.ClosedSurfaceR4.SphericalJets.radialNormalize