AtlasNearbyPhaseCancellation.lean`

2 declarations, 0 contain sorry, 0 declared as axioms

Atlas cancellation uniform over a neighborhood of a fixed immersion. The reference geometry, per-chart shifted profiles and finite phase family determine all constants before the varying map, target or scale is chosen.

theorem OAI.ClosedSurfaceR4.FiniteOrderSmoothing.SmoothingAtlas.atlas_nearby_phase_cancellation_all_profiles line 44

Source documentation

Fixed good-phase geometry gives uniform global cancellation for nearby maps with the specified shifted derivative profiles at the actual slow scale.

theorem atlas_nearby_phase_cancellation_all_profiles
    {ι : A.centers → Type*} [∀ i, Fintype (ι i)]
    (F : M → Space) (hF : ContMDiff planeModel spaceModel ∞ F)
    (φ : (i : A.centers) → ι i → JetPolynomial.Base → ℝ)
    (hφ : ∀ i j, ContDiff ℝ ∞ (φ i j))
    (K : (i : A.centers) → ι i → TopologicalSpace.Compacts JetPolynomial.Base)
    (hK : ∀ i j, (modeSupport (K i j) : Set SmallModes.Base) ⊆
      (modeSupport (A.chartWeightCompact i) : Set SmallModes.Base))
    (hImm : ∀ i j p, p ∈ (modeSupport (K i j) : Set SmallModes.Base) →
      Function.Injective (fderiv ℝ (spaceCoordinates ∘ A.vectorPlaneRead i F) p))
    (hgood : ∀ i j p, p ∈ (modeSupport (K i j) : Set SmallModes.Base) →
      PhaseGeometry.Good (RealModes.realSecondTensor (spaceCoordinates ∘ A.vectorPlaneRead i F) p)
…

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

theorem OAI.ClosedSurfaceR4.FiniteOrderSmoothing.SmoothingAtlas.atlas_nearby_phase_cancellation line 189

Source documentation

Fixed good-phase geometry gives uniform global cancellation for nearby maps with the specified shifted derivative profiles at the actual slow scale.

theorem atlas_nearby_phase_cancellation
    {ι : A.centers → Type*} [∀ i, Fintype (ι i)]
    (F : M → Space) (hF : ContMDiff planeModel spaceModel ∞ F)
    (φ : (i : A.centers) → ι i → JetPolynomial.Base → ℝ)
    (hφ : ∀ i j, ContDiff ℝ ∞ (φ i j))
    (K : (i : A.centers) → ι i → TopologicalSpace.Compacts JetPolynomial.Base)
    (hK : ∀ i j, (modeSupport (K i j) : Set SmallModes.Base) ⊆
      (modeSupport (A.chartWeightCompact i) : Set SmallModes.Base))
    (hImm : ∀ i j p, p ∈ (modeSupport (K i j) : Set SmallModes.Base) →
      Function.Injective (fderiv ℝ (spaceCoordinates ∘ A.vectorPlaneRead i F) p))
    (hgood : ∀ i j p, p ∈ (modeSupport (K i j) : Set SmallModes.Base) →
      PhaseGeometry.Good (RealModes.realSecondTensor (spaceCoordinates ∘ A.vectorPlaneRead i F) p)
…