ModulatedPolynomialJets.lean`

GitHub source file

10 declarations, 0 contain sorry, 0 declared as axioms

Actual oscillatory direction jets factor into one phase per direction and a slow amplitude jet.

lemma OAI.ClosedSurfaceR4.JetPolynomial.MixedExpression.scaleJets_base line 16
lemma OAI.ClosedSurfaceR4.JetPolynomial.MixedExpression.scaleJets_succ line 20
abbrev OAI.ClosedSurfaceR4.JetPolynomial.ModulatedJets.DirectionFields line 28
def OAI.ClosedSurfaceR4.JetPolynomial.ModulatedJets.amplitudeData line 30
def OAI.ClosedSurfaceR4.JetPolynomial.ModulatedJets.oscillatoryData line 35
lemma OAI.ClosedSurfaceR4.JetPolynomial.ModulatedJets.amplitudeData_base line 41
lemma OAI.ClosedSurfaceR4.JetPolynomial.ModulatedJets.amplitudeData_succ line 45
lemma OAI.ClosedSurfaceR4.JetPolynomial.ModulatedJets.oscillatoryData_factor line 50
lemma OAI.ClosedSurfaceR4.JetPolynomial.ModulatedJets.amplitudeData_smooth line 61
theorem OAI.ClosedSurfaceR4.JetPolynomial.ModulatedJets.variation_phase_factor line 72
Source documentation
Exact phase cancellation for each of the first three complexified variations. The remaining factors are the modulated amplitude jets.
```
theorem variation_phase_factor (e : Expression) (G : Base → Space) {φ : Fin 3 → Base → ℝ}
    {H : DirectionFields} (hφ : ∀ j, ContDiff ℝ ∞ (φ j))
    (hH : ∀ j, ContDiff ℝ ∞ (H j)) (τ : ℝ) (z : Base × ℝ) (i : Fin 3) :
    (e.variations i).evalComplex G (oscillatoryData G φ H τ) z =
      (phase τ (φ 0) z.1 * (if 1 ≤ i then phase τ (φ 1) z.1 else 1) *
        (if 2 ≤ i then phase τ (φ 2) z.1 else 1)) *
      (e.variations i).evalComplex G (amplitudeData G φ H τ) z := by
…
```
Mentions: OAI.ClosedSurfaceR4.JetPolynomial.Expression, OAI.ClosedSurfaceR4.JetPolynomial.Base, OAI.ClosedSurfaceR4.JetPolynomial.Space, OAI.ClosedSurfaceR4.JetPolynomial.ModulatedJets.DirectionFields, OAI.ClosedSurfaceR4.JetPolynomial.ModulatedJets.oscillatoryData, OAI.ClosedSurfaceR4.JetPolynomial.ModulatedJets.phase, OAI.ClosedSurfaceR4.JetPolynomial.ModulatedJets.amplitudeData