OAI/Geometry/SurfaceImmersion/Atlas/CenteredConvexPhase.lean

GitHub source file

16 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.ClosedSurfaceR4.PhaseGeometry.centeredConvexPhase line 15
2. lemma OAI.ClosedSurfaceR4.PhaseGeometry.centeredConvexPhase_smooth line 18
3. lemma OAI.ClosedSurfaceR4.PhaseGeometry.centeredConvexPhase_hasFDerivAt line 22
4. lemma OAI.ClosedSurfaceR4.PhaseGeometry.centeredConvexPhase_coordDeriv line 29
5. lemma OAI.ClosedSurfaceR4.PhaseGeometry.centeredConvexPhase_phaseDerivative line 34
6. lemma OAI.ClosedSurfaceR4.PhaseGeometry.centeredConvexPhase_second line 40
7. lemma OAI.ClosedSurfaceR4.PhaseGeometry.centeredConvexPhase_regular line 63
8. lemma OAI.ClosedSurfaceR4.PhaseGeometry.centeredConvexPhase_hessian line 71
9. theorem OAI.ClosedSurfaceR4.PhaseGeometry.centeredConvexPhase_hessian_lower line 78
10. theorem OAI.ClosedSurfaceR4.PhaseGeometry.compact_uniform_centered_convex_phases line 120

    Source documentation

    The metric-jet compact set fixes the same Hessian constants at every center; the first metric jet is always taken at the actual point.

    theorem compact_uniform_centered_convex_phases {J : Set MetricFirstJet}
        (hJ : IsCompact J) (hdet : ∀ j ∈ J, metricJetDet j ≠ 0)
        {K : ℝ} (hK : 0 ≤ K) :
        ∃ L r : ℝ, 0 < L ∧ 0 < r ∧
          ∀ (h : Base → PhaseMean.Tensor) (ell c p : Base), ‖ell‖ ≤ K → ‖p-c‖ ≤ r →
            (h p,fderiv ℝ h p) ∈ J → ∀ v : Base,
            (L/2)*(v.1^2+v.2^2) ≤
              coordinateMetricHessian h (centeredConvexPhase ell L c) p v v := by
    …

    Mentions: OAI.ClosedSurfaceR4.PhaseGeometry.MetricFirstJet, OAI.ClosedSurfaceR4.PhaseGeometry.metricJetDet, OAI.ClosedSurfaceR4.PhaseMean.Tensor, OAI.ClosedSurfaceR4.PhaseGeometry.coordinateMetricHessian, OAI.ClosedSurfaceR4.PhaseGeometry.centeredConvexPhase

11. theorem OAI.ClosedSurfaceR4.PhaseGeometry.compact_perturbed_centered_phase_margin line 147

    Source documentation

    Exact positive phase coefficients and Hessian margins survive independent linear perturbations on a disk centered anywhere.

    theorem compact_perturbed_centered_phase_margin (P : PhaseBasis)
        {T : Set PhaseMean.Tensor} (hT : IsCompact T)
        (hTpos : ∀ H ∈ T, ∀ i, 0 < P.Q i H)
        {J : Set MetricFirstJet} (hJ : IsCompact J)
        (hdet : ∀ j ∈ J, metricJetDet j ≠ 0) :
        ∃ L r eps : ℝ, 0 < L ∧ 0 < r ∧ 0 < eps ∧
          ∀ ell : Fin 3 → Base, ‖ell-P.ξ‖ < eps → ∀ c p : Base, ‖p-c‖ ≤ r →
            let xi := fun i => phaseDerivative (centeredConvexPhase (ell i) L c) p
    …

    Mentions: OAI.ClosedSurfaceR4.PhaseGeometry.PhaseBasis, OAI.ClosedSurfaceR4.PhaseMean.Tensor, OAI.ClosedSurfaceR4.PhaseGeometry.MetricFirstJet, OAI.ClosedSurfaceR4.PhaseGeometry.metricJetDet, OAI.ClosedSurfaceR4.phaseDerivative, OAI.ClosedSurfaceR4.PhaseGeometry.centeredConvexPhase

12. def OAI.ClosedSurfaceR4.PhaseGeometry.centeredSpatialBasis line 198
13. lemma OAI.ClosedSurfaceR4.PhaseGeometry.centeredSpatialBasis_covectors line 202
14. lemma OAI.ClosedSurfaceR4.PhaseGeometry.centeredSpatialBasis_coefficient_smoothAt line 210
15. theorem OAI.ClosedSurfaceR4.PhaseGeometry.centered_convex_phase_charts_on_disk line 224

    Source documentation

    A single genuine phase chart contains the entire smaller centered disk.

    theorem centered_convex_phase_charts_on_disk (ell : Fin 3 → Base)
        (hell : ∀ i, ell i ≠ 0) (c : Base) {L r₀ : ℝ} (hL : 0 ≤ L) (hr₀ : 0 < r₀) :
        ∃ r : ℝ, 0 < r ∧ r ≤ r₀ ∧
          ∃ e : Fin 3 → OpenPartialHomeomorph Base Base,
            (∀ i x, (e i x).1 = centeredConvexPhase (ell i) L c x) ∧
            (∀ i, ContDiff ℝ ∞ (e i) ∧ ContDiffOn ℝ ∞ (e i).symm (e i).target) ∧
            ∀ i p, ‖p-c‖ ≤ r → p ∈ (e i).source := by
    …

    Mentions: OAI.ClosedSurfaceR4.PhaseGeometry.centeredConvexPhase

16. theorem OAI.ClosedSurfaceR4.PhaseGeometry.compact_centered_spatial_basis line 253

    Source documentation

    The actual spatial basis has precisely the centered phase gradients, positive tensor coefficients, and smoothly varying coefficient maps.

    theorem compact_centered_spatial_basis (P : PhaseBasis)
        {T : Set PhaseMean.Tensor} (hT : IsCompact T)
        (hTpos : ∀ H ∈ T, ∀ i, 0 < P.Q i H)
        {J : Set MetricFirstJet} (hJ : IsCompact J)
        (hdet : ∀ j ∈ J, metricJetDet j ≠ 0) :
        ∃ L r eps : ℝ, 0 < L ∧ 0 < r ∧ 0 < eps ∧
          ∀ ell : Fin 3 → Base, ‖ell-P.ξ‖ < eps → ∀ c p : Base, ‖p-c‖ ≤ r →
            ((centeredSpatialBasis P ell L c p).ξ =
              fun i => phaseDerivative (centeredConvexPhase (ell i) L c) p) ∧
            (∀ H ∈ T, ∀ i, 0 < (centeredSpatialBasis P ell L c p).Q i H) ∧
            (∀ i, ContDiffAt ℝ ∞ (fun x => (centeredSpatialBasis P ell L c x).Q i) p) ∧
            ∀ h : Base → PhaseMean.Tensor, (h p,fderiv ℝ h p) ∈ J → ∀ i v,
    …

    Mentions: OAI.ClosedSurfaceR4.PhaseGeometry.PhaseBasis, OAI.ClosedSurfaceR4.PhaseMean.Tensor, OAI.ClosedSurfaceR4.PhaseGeometry.MetricFirstJet, OAI.ClosedSurfaceR4.PhaseGeometry.metricJetDet, OAI.ClosedSurfaceR4.PhaseGeometry.centeredSpatialBasis, OAI.ClosedSurfaceR4.phaseDerivative, OAI.ClosedSurfaceR4.PhaseGeometry.centeredConvexPhase