AtlasCompactPhaseWeights.lean`

1 declarations, 0 contain sorry, 0 declared as axioms

One frequency per global phase, chosen simultaneously on every chart overlap.

theorem OAI.ClosedSurfaceR4.FiniteOrderSmoothing.SmoothingAtlas.exists_overlap_phase_weights line 22

Source documentation

Compactness selects frequencies before any target tensor or correction scale. The same frequency works in every chart that meets the phase support.

theorem exists_overlap_phase_weights {ι : Type*} [Finite ι]
    {F : M → Space} (hF : ContMDiff planeModel spaceModel ∞ F)
    (φ : ι → M → ℝ) (hφ : ∀ a, ContMDiff planeModel 𝓘(ℝ) ∞ (φ a))
    (S : ι → Set M) (hS : ∀ a, IsClosed (S a))
    (hImm : ∀ k p, p ∈ tsupport (A.weight k) → Function.Injective
      (fderiv ℝ (spaceCoordinates ∘ A.vectorPlaneRead k F) (coordinateChart (k : M) p)))
    (hgood : ∀ k a p, p ∈ tsupport (A.weight k) → p ∈ S a →
      Good (realSecondTensor (spaceCoordinates ∘ A.vectorPlaneRead k F)
        (coordinateChart (k : M) p))
        (phaseDerivative (A.vectorPlaneRead k (φ a)) (coordinateChart (k : M) p))) :
    ∃ w : ι → ℝ, (∀ a, 0 < w a) ∧
      ∀ k a b, a ≠ b → ∀ p, p ∈ tsupport (A.weight k) → p ∈ S a → p ∈ S b →
…

Mentions: OAI.ClosedSurfaceR4.Space, OAI.ClosedSurfaceR4.planeModel, OAI.ClosedSurfaceR4.spaceCoordinates, OAI.ClosedSurfaceR4.coordinateChart, OAI.ClosedSurfaceR4.phaseDerivative