PolynomialZeroPhaseExpansion.lean`

7 declarations, 0 contain sorry, 0 declared as axioms

Separate the actual polynomial Hessian into its zero-phase part and explicit doubled and mixed phases. Ordered pairs retain all multiplicities.

def OAI.ClosedSurfaceR4.JetPolynomial.Perturbation.quadraticPhaseCoefficient line 14
lemma OAI.ClosedSurfaceR4.JetPolynomial.Perturbation.phase_mul line 19
def OAI.ClosedSurfaceR4.JetPolynomial.Perturbation.quadraticOscillation line 23
lemma OAI.ClosedSurfaceR4.JetPolynomial.Perturbation.quadraticMeanCoefficient_eq_phaseCoefficient line 33
lemma OAI.ClosedSurfaceR4.JetPolynomial.Perturbation.quadraticPhaseCoefficient_oscillation line 40
lemma OAI.ClosedSurfaceR4.JetPolynomial.Perturbation.weighted_half_second_variation_phases line 59
theorem OAI.ClosedSurfaceR4.JetPolynomial.Perturbation.quadratic_zero_phase_expansion line 82
Source documentation
The omitted terms have exactly the doubled/sum/difference phases. The geometric good-phase hypothesis is only needed later to solve these modes.
```
theorem quadratic_zero_phase_expansion {n : ℕ} {ι : Type*} [Fintype ι] [DecidableEq ι]
    (P : Fin n → Expression) (ε : ℝ) (G : Base → Space)
    (φ : ι → Base → ℝ) (H : ι → Base → Fin 4 → ℂ)
    (hφ : ∀ i, ContDiff ℝ ∞ (φ i)) (hH : ∀ i, ContDiff ℝ ∞ (H i))
    (τ t : ℝ) (p : Base) :
    (∑ l : Fin n, ε ^ (l.val + 1) * ((1 / 2 : ℝ) * ((P l).variations 1).eval
      ![G, realField (oscillatorySum τ φ H), realField (oscillatorySum τ φ H), 0] (p,t))) =
    (∑ i, quadraticMeanCoefficient P ε G (φ i) (H i) τ t p) +
      quadraticOscillation P ε G φ H τ t p := by
…
```
Mentions: OAI.ClosedSurfaceR4.JetPolynomial.Expression, OAI.ClosedSurfaceR4.JetPolynomial.Base, OAI.ClosedSurfaceR4.JetPolynomial.Space, OAI.ClosedSurfaceR4.JetPolynomial.Perturbation.eval, OAI.ClosedSurfaceR4.JetPolynomial.realField, OAI.ClosedSurfaceR4.JetPolynomial.oscillatorySum, OAI.ClosedSurfaceR4.JetPolynomial.Perturbation.quadraticMeanCoefficient, OAI.ClosedSurfaceR4.JetPolynomial.Perturbation.quadraticOscillation