OAI/Geometry/SurfaceImmersion/Atlas/CompactPhaseSolvers.lean

GitHub source file

1 declarations, 0 contain sorry, 0 declared as axioms

1. theorem OAI.ClosedSurfaceR4.PhaseGeometry.compact_phase_solvers line 16

   Source documentation

   Local good-phase geometry supplies all the solver data on a finite support decomposition. There is no assumption of a chart on the entire support.

   theorem compact_phase_solvers
       {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) :
   …

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