UniformCompactPhaseCancellation.lean`

1 declarations, 0 contain sorry, 0 declared as axioms

Uniform cancellation on compact good-phase supports with no assumed phase solver.

theorem OAI.ClosedSurfaceR4.PhaseGeometry.uniform_compact_good_phase_cancellation line 15

Source documentation

A compact good phase gives a uniform finite-loss cancellation estimate. The geometry and constants are chosen before the target and both scales.

theorem uniform_compact_good_phase_cancellation
    {G : JetPolynomial.Base → JetPolynomial.Space} (hG : ContDiff ℝ ∞ G)
    {φ : JetPolynomial.Base → ℝ} (hφ : ContDiff ℝ ∞ φ) (K : Compacts SmallModes.Base)
    (hImm : ∀ p ∈ (K : Set SmallModes.Base),
      Function.Injective (fderiv ℝ (G ∘ planeCoordinateIsometry.symm) p))
    (hgood : ∀ p ∈ (K : Set SmallModes.Base),
      Good (RealModes.realSecondTensor (G ∘ planeCoordinateIsometry.symm) p)
        (phaseDerivative (coordinatePhase φ) p)) (q : ℕ) :
    ∃ C D : ℕ → ℝ, (∀ m, 0 ≤ C m) ∧ (∀ m, 0 ≤ D m) ∧
      ∀ (A : SupportedField (F := ComplexTensor) K) (τ : ℝ) (s : ℝ≥0),
…

Mentions: OAI.ClosedSurfaceR4.JetPolynomial.Base, OAI.ClosedSurfaceR4.JetPolynomial.Space, OAI.ClosedSurfaceR4.SmallModes.Base, OAI.ClosedSurfaceR4.PhaseGeometry.Good, OAI.ClosedSurfaceR4.RealModes.realSecondTensor, OAI.ClosedSurfaceR4.phaseDerivative