GoodPhaseCover.lean`

3 declarations, 0 contain sorry, 0 declared as axioms

Finite good phase charts covering the compact support of a correction.

structure OAI.ClosedSurfaceR4.PhaseGeometry.GoodPhaseChart line 13
Source documentation
All geometric data of one compactly bounded local phase chart.
```
structure GoodPhaseChart (F : RField 4) (φ : Base → ℝ) where
…
```
theorem OAI.ClosedSurfaceR4.PhaseGeometry.exists_goodPhaseChart line 26

theorem OAI.ClosedSurfaceR4.PhaseGeometry.finite_good_phase_cover line 37

Source documentation

No global coordinate chart for a mixed phase is assumed: finitely many actual local phase charts cover its compact support.

theorem finite_good_phase_cover {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)) :
    ∃ (t : Finset K) (c : t → GoodPhaseChart F φ),
      (K : Set Base) ⊆ ⋃ i : t, (c i).chart.source := by
…

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