PhaseReparametrization.lean`

5 declarations, 0 contain sorry, 0 declared as axioms

A good covector supplies the actual free coordinate system for a mode.

lemma OAI.ClosedSurfaceR4.RealModes.phaseInverse_det line 16
lemma OAI.ClosedSurfaceR4.RealModes.phaseInverse_dy line 30

theorem OAI.ClosedSurfaceR4.RealModes.realSecond_phase line 36

Source documentation

The normal acceleration in the new y direction is a positive scalar multiple of the old second fundamental form in the covector's kernel.

theorem realSecond_phase {F : RField 4} (hF : ContDiff ℝ ∞ F)
    {ξ : Base} (hξ : ξ ≠ 0) (p : Base)
    (hImm : Function.Injective (fderiv ℝ F ((phaseEquiv ξ hξ).symm p))) :
    realSecond (F ∘ (phaseEquiv ξ hξ).symm) p =
      ((ξ.1 ^ 2 + ξ.2 ^ 2)⁻¹) ^ 2 •
        secondQuadratic (realSecondTensor F ((phaseEquiv ξ hξ).symm p)) (-ξ.2, ξ.1) := by
…

Mentions: OAI.ClosedSurfaceR4.RealModes.RField, OAI.ClosedSurfaceR4.RealModes.realSecond, OAI.ClosedSurfaceR4.RealModes.realSecondTensor

theorem OAI.ClosedSurfaceR4.RealModes.realModeDomain_phase line 51
Source documentation
Immersion and the good-direction condition on an open set produce the free-mode domain required by the finite oscillatory construction.
```
theorem realModeDomain_phase {F : RField 4} (hF : ContDiff ℝ ∞ F)
    {O : Set Base} (hO : IsOpen O) {ξ : Base} (hξ : ξ ≠ 0)
    (hImm : ∀ p ∈ O, Function.Injective (fderiv ℝ F p))
    (hgood : ∀ p ∈ O, Good (realSecondTensor F p) ξ) :
    RealModeDomain (F ∘ (phaseEquiv ξ hξ).symm) ((phaseEquiv ξ hξ) '' O) := by
…
```
Mentions: OAI.ClosedSurfaceR4.RealModes.RField, OAI.ClosedSurfaceR4.RealModes.realSecondTensor, OAI.ClosedSurfaceR4.RealModes.RealModeDomain

def OAI.ClosedSurfaceR4.RealModes.supportedFreeChartOfPhase line 74

Source documentation

A good phase gives all coordinate data for a supported free chart.

def supportedFreeChartOfPhase {F : RField 4} (hF : ContDiff ℝ ∞ F)
    {O S : Set Base} (hO : IsOpen O) (hS : IsClosed S) (hSO : S ⊆ O)
    {ξ : Base} (hξ : ξ ≠ 0) (ψ : Base → ℝ)
    (hImm : ∀ p ∈ O, Function.Injective (fderiv ℝ F p))
    (hgood : ∀ p ∈ O, Good (realSecondTensor F p) ξ)
    (hsupp : ∀ p ∈ O, phaseEquiv ξ hξ p ∈ tsupport ψ → p ∈ S) :
    SupportedFreeChart F (fun p => ξ.1 * p.1 + ξ.2 * p.2) ψ S where
…

Mentions: OAI.ClosedSurfaceR4.RealModes.RField, OAI.ClosedSurfaceR4.RealModes.realSecondTensor, OAI.ClosedSurfaceR4.RealModes.SupportedFreeChart