CompactPhaseCancellation.lean`

1 declarations, 0 contain sorry, 0 declared as axioms

Cancellation on an arbitrary compact support from actual good-phase geometry.

theorem OAI.ClosedSurfaceR4.PhaseGeometry.compact_good_phase_cancellation line 18

Source documentation

A single good phase on a compact support needs only finitely many local phase charts. Their actual corrections cancel the original target at every smaller wavelength, with one set of constants for that target.

theorem 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))
    (A : SupportedField (F := ComplexTensor) K) (q : ℕ) :
…

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