OAI/Geometry/SurfaceImmersion/Correction/PolynomialQuadraticPhases.lean

GitHub source file

10 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.ClosedSurfaceR4.JetPolynomial.pairPhases line 11
2. def OAI.ClosedSurfaceR4.JetPolynomial.pairDirections line 12
3. def OAI.ClosedSurfaceR4.JetPolynomial.starField line 13
4. lemma OAI.ClosedSurfaceR4.JetPolynomial.starField_smooth line 15
5. lemma OAI.ClosedSurfaceR4.JetPolynomial.complexJet_starField line 21
6. lemma OAI.ClosedSurfaceR4.JetPolynomial.phase_star line 27
7. lemma OAI.ClosedSurfaceR4.JetPolynomial.starField_phase line 34
8. lemma OAI.ClosedSurfaceR4.JetPolynomial.pair_oscillatoryData line 40
9. lemma OAI.ClosedSurfaceR4.JetPolynomial.quadraticComplex_phase_factor line 54
10. theorem OAI.ClosedSurfaceR4.JetPolynomial.half_second_variation_oscillation line 67

    Source documentation

    The coefficient of the zero phase is precisely the mixed phase Hessian; all remaining self-interaction has phase twice the original phase.

    theorem half_second_variation_oscillation (e : Expression) (G : Base → Space)
        {φ : Base → ℝ} {H : Base → Fin 4 → ℂ}
        (hφ : ContDiff ℝ ∞ φ) (hH : ContDiff ℝ ∞ H) (τ : ℝ) (z : Base × ℝ) :
        (1 / 2 : ℝ) * (e.variations 1).eval
          ![G, realField (fun p => phase τ φ p • H p), realField (fun p => phase τ φ p • H p), 0] z =
          ((phase τ φ z.1 ^ 2) *
            conjugatedVariation e G (pairPhases φ φ) (pairDirections H H) τ 1 z).re / 4 +
          (conjugatedVariation e G (pairPhases φ (fun p => -φ p))
            (pairDirections H (starField H)) τ 1 z).re / 4 := by
    …

    Mentions: OAI.ClosedSurfaceR4.JetPolynomial.Expression, OAI.ClosedSurfaceR4.JetPolynomial.Base, OAI.ClosedSurfaceR4.JetPolynomial.Space, OAI.ClosedSurfaceR4.JetPolynomial.realField, OAI.ClosedSurfaceR4.JetPolynomial.pairPhases, OAI.ClosedSurfaceR4.JetPolynomial.pairDirections, OAI.ClosedSurfaceR4.JetPolynomial.starField