LinearPhaseDerivativeProfiles.lean`

5 declarations, 0 contain sorry, 0 declared as axioms

All derivatives of a fixed linear phase are constant fields. The two profiles needed by local quadratic cancellation are therefore uniform in the derivative order, the map and both scales.

def OAI.ClosedSurfaceR4.JetPolynomial.Perturbation.originalPhaseLinear line 15
lemma OAI.ClosedSurfaceR4.JetPolynomial.Perturbation.phase_eq_originalPhaseLinear line 18
lemma OAI.ClosedSurfaceR4.JetPolynomial.Perturbation.linear_phase_original_derivative line 25
lemma OAI.ClosedSurfaceR4.JetPolynomial.Perturbation.linear_phase_coordinate_derivative line 32

theorem OAI.ClosedSurfaceR4.JetPolynomial.Perturbation.linear_phase_derivative_profiles line 41

Source documentation

Fixed finite linear phases provide the original-coordinate and mode-coordinate derivative bounds, including any additional input order.

theorem linear_phase_derivative_profiles {ι : Type*} [Fintype ι]
    (φ : ι → Base → ℝ) (ξ : ι → SmallModes.Base)
    (hphase : ∀ i, coordinatePhase (φ i) = phaseLinear (ξ i)) :
    ∃ F M : ℕ → ℝ, (∀ m, 1 ≤ F m) ∧ (∀ m, 1 ≤ M m) ∧
      (∀ (U : Set Base) (s : ℝ) (m r : ℕ) (i : ι) (v : Fin 2),
        WeightedBound U s (m + r) (F m)
          (fun x => fderiv ℝ (φ i) x (coordinateVector v))) ∧
      (∀ (s : ℝ) (m : ℕ) (i : ι) (v : SmallModes.Base), ‖v‖ ≤ 1 →
        WeightedBound Set.univ s m (M m) (SmallModes.coordDeriv v (coordinatePhase (φ i)))) := by
…

Mentions: OAI.ClosedSurfaceR4.JetPolynomial.Base, OAI.ClosedSurfaceR4.SmallModes.Base, OAI.ClosedSurfaceR4.JetPolynomial.Perturbation.coordinatePhase, OAI.ClosedSurfaceR4.phaseLinear, OAI.ClosedSurfaceR4.JetPolynomial.coordinateVector, OAI.ClosedSurfaceR4.SmallModes.coordDeriv