GoodPhaseTargetSplit.lean`

1 declarations, 0 contain sorry, 0 declared as axioms

Split an actual compact target into geometrically admissible phase pieces.

theorem OAI.ClosedSurfaceR4.PhaseGeometry.split_target_into_good_phase_charts line 17

Source documentation

Every supported target with a good phase on its support admits a finite exact decomposition into targets for actual compactly bounded good charts.

theorem split_target_into_good_phase_charts {F : RField 4} (hF : ContDiff ℝ ∞ F)
    {φ : Base → ℝ} (hφ : ContDiff ℝ ∞ φ) (K : Compacts Base)
    (hImm : ∀ p ∈ (K : Set Base), Function.Injective (fderiv ℝ F p))
    (hgood : ∀ p ∈ (K : Set Base), Good (realSecondTensor F p) (phaseDerivative φ p))
    (A : SupportedField (F := ComplexTensor) K) :
…

Mentions: OAI.ClosedSurfaceR4.PhaseGeometry.Good, OAI.ClosedSurfaceR4.phaseDerivative