SphericalMetricPhaseData.lean`

7 declarations, 0 contain sorry, 0 declared as axioms

A smooth three-space immersion supplies the actual starting phase geometry.

lemma OAI.ClosedSurfaceR4.FiniteOrderSmoothing.inner_spaceCoordinates_symm line 15
lemma OAI.ClosedSurfaceR4.FiniteOrderSmoothing.fderiv_realDot_apply line 20
lemma OAI.ClosedSurfaceR4.FiniteOrderSmoothing.sphere_real_radial_first line 36
lemma OAI.ClosedSurfaceR4.FiniteOrderSmoothing.sphere_real_radial_second line 48

lemma OAI.ClosedSurfaceR4.FiniteOrderSmoothing.sphere_realSecondForm_inward line 70

Source documentation

The inward radial pairing of the coordinate second form is the induced metric, even though the coordinate representative is only smooth on its chart.

lemma sphere_realSecondForm_inward {F : RField 4} {U : Set Base}
    (hU : IsOpen U) (hF : ContDiffOn ℝ ∞ F U)
    (hunit : ∀ y, F y ⬝ᵥ F y = 1) {x : Base} (hx : x ∈ U) (v w : Base) :
    realSecondForm F v w x ⬝ᵥ (-F x) =
      coordDeriv v F x ⬝ᵥ coordDeriv w F x := by
…

theorem OAI.ClosedSurfaceR4.FiniteOrderSmoothing.spherical_coordinate_second_nonzero line 89
Source documentation
A spherical immersion has nonzero second fundamental form in every coordinate chart, with the first coordinate direction as an explicit witness.
```
theorem spherical_coordinate_second_nonzero {G : M → Space}
    (hG : ContMDiff planeModel spaceModel ∞ G) (hunit : ∀ p, ‖G p‖ = 1)
    (hI : ∀ p, Function.Injective (mfderiv planeModel spaceModel G p)) (p : M) :
    ∃ v w : Base, realSecondForm (coordinateMap G p) v w (coordinateCenter p) ≠ 0 := by
…
```
Mentions: OAI.ClosedSurfaceR4.Space, OAI.ClosedSurfaceR4.planeModel, OAI.ClosedSurfaceR4.coordinateMap, OAI.ClosedSurfaceR4.coordinateCenter

theorem OAI.ClosedSurfaceR4.FiniteOrderSmoothing.metricPhaseData_of_three_space_immersion line 121

Source documentation

A given smooth immersion into three-space yields a spherical immersion and all the concrete phase geometry for any smooth target metric.

theorem metricPhaseData_of_three_space_immersion
    (g : SmoothMetric M) {F : M → SphericalStart.ThreeSpace}
    (hF : ContMDiff planeModel 𝓘(ℝ,SphericalStart.ThreeSpace) ∞ F)
    (hI : ∀ p, Function.Injective (mfderiv planeModel 𝓘(ℝ,SphericalStart.ThreeSpace) F p)) :
    ∃ G : M → Space, ContMDiff planeModel spaceModel ∞ G ∧
      (∀ p, ‖G p‖ = 1) ∧
      (∀ p, Function.Injective (mfderiv planeModel spaceModel G p)) ∧
      Nonempty (MetricGoodPhaseData g G) := by
…

Mentions: OAI.ClosedSurfaceR4.SmoothMetric, OAI.ClosedSurfaceR4.SphericalStart.ThreeSpace, OAI.ClosedSurfaceR4.planeModel, OAI.ClosedSurfaceR4.Space, OAI.ClosedSurfaceR4.FiniteOrderSmoothing.MetricGoodPhaseData