OAI/Geometry/SurfaceImmersion/Atlas/ConvexQuadraticPhase.lean

GitHub source file

23 declarations, 0 contain sorry, 0 declared as axioms

The actual convex phases used in finite primitive preparation. Their coordinate covariant Hessians are uniformly positive on a sufficiently small disk when the metric connection has a fixed bound.

  1. def OAI.ClosedSurfaceR4.PhaseGeometry.convexQuadraticPhase line 16
  2. lemma OAI.ClosedSurfaceR4.PhaseGeometry.convexQuadraticPhase_smooth line 19
  3. lemma OAI.ClosedSurfaceR4.PhaseGeometry.convexQuadraticPhase_hasFDerivAt line 24
  4. lemma OAI.ClosedSurfaceR4.PhaseGeometry.convexQuadraticPhase_coordDeriv line 39
  5. lemma OAI.ClosedSurfaceR4.PhaseGeometry.convexQuadraticPhase_phaseDerivative line 44
  6. lemma OAI.ClosedSurfaceR4.PhaseGeometry.convexQuadraticPhase_regular line 50
  7. theorem OAI.ClosedSurfaceR4.PhaseGeometry.convexQuadraticPhase_chart line 58
  8. lemma OAI.ClosedSurfaceR4.PhaseGeometry.convexQuadraticPhase_second line 66
  9. abbrev OAI.ClosedSurfaceR4.PhaseGeometry.MetricFirstJet line 86

    Source documentation

    A metric value together with its first coordinate derivative.

    abbrev MetricFirstJet := PhaseMean.Tensor × (Base →L[ℝ] PhaseMean.Tensor)

    Mentions: OAI.ClosedSurfaceR4.PhaseMean.Tensor

  10. def OAI.ClosedSurfaceR4.PhaseGeometry.metricJetDet line 88
  11. def OAI.ClosedSurfaceR4.PhaseGeometry.metricConnectionAt line 92

    Source documentation

    The three symmetric Christoffel slots, with values in the coordinate tangent plane, computed from the metric and its first derivatives.

    def metricConnectionAt (J : MetricFirstJet) : Fin 3 → Base :=
…

    Mentions: OAI.ClosedSurfaceR4.PhaseGeometry.MetricFirstJet

  12. lemma OAI.ClosedSurfaceR4.PhaseGeometry.metricConnectionAt_contDiffAt line 98
  13. theorem OAI.ClosedSurfaceR4.PhaseGeometry.compact_metricConnection_bound line 106
  14. def OAI.ClosedSurfaceR4.PhaseGeometry.connectionContract line 114
  15. def OAI.ClosedSurfaceR4.PhaseGeometry.coordinateMetricHessian line 117
  16. lemma OAI.ClosedSurfaceR4.PhaseGeometry.convexQuadraticPhase_hessian line 122
  17. lemma OAI.ClosedSurfaceR4.PhaseGeometry.coordinateMetricHessian_fst_dy line 130
  18. lemma OAI.ClosedSurfaceR4.PhaseGeometry.abs_quadratic_combination line 140
  19. lemma OAI.ClosedSurfaceR4.PhaseGeometry.connectionContract_diagonal_bound line 161
  20. theorem OAI.ClosedSurfaceR4.PhaseGeometry.convexQuadraticPhase_hessian_lower line 175
  21. theorem OAI.ClosedSurfaceR4.PhaseGeometry.exists_uniform_convex_quadratic_phases line 217

    Source documentation

    The radius and quadratic coefficient are chosen from the connection and linear-covector bounds, before the individual metric or point.

    theorem exists_uniform_convex_quadratic_phases {B K : ℝ} (hB : 0 ≤ B) (hK : 0 ≤ K) :
    ∃ L r : ℝ, 0 < L ∧ 0 < r ∧
      ∀ (h : Base → PhaseMean.Tensor) (ell p : Base), ‖ell‖ ≤ K → ‖p‖ ≤ r →
        (∀ i, ‖metricConnectionAt (h p,fderiv ℝ h p) i‖ ≤ B) →
        ∀ v : Base, (L/2)*(v.1^2+v.2^2) ≤
          coordinateMetricHessian h (convexQuadraticPhase ell L) p v v := by
…

    Mentions: OAI.ClosedSurfaceR4.PhaseMean.Tensor, OAI.ClosedSurfaceR4.PhaseGeometry.metricConnectionAt, OAI.ClosedSurfaceR4.PhaseGeometry.coordinateMetricHessian, OAI.ClosedSurfaceR4.PhaseGeometry.convexQuadraticPhase

  22. theorem OAI.ClosedSurfaceR4.PhaseGeometry.compact_uniform_convex_quadratic_phases line 239
  23. theorem OAI.ClosedSurfaceR4.PhaseGeometry.finite_uniform_convex_phase_charts line 254

    Source documentation

    One disk and one quadratic coefficient work for all three phase covectors and every metric whose first jet belongs to the fixed compact set. Each phase has positive Hessian and is a genuine local coordinate.

    theorem finite_uniform_convex_phase_charts {J : Set MetricFirstJet}
    (hJ : IsCompact J) (hdet : ∀ j ∈ J, metricJetDet j ≠ 0)
    (ell : Fin 3 → Base) (hell : ∀ i, ell i ≠ 0) :
    ∃ L r : ℝ, 0 < L ∧ 0 < r ∧
      ∀ (h : Base → PhaseMean.Tensor) (p : Base), ‖p‖ ≤ r →
        (h p,fderiv ℝ h p) ∈ J → ∀ i,
          (∀ v : Base, v ≠ 0 →
            0 < coordinateMetricHessian h (convexQuadraticPhase (ell i) L) p v v) ∧
          ∃ e : OpenPartialHomeomorph Base Base, p ∈ e.source ∧
            (∀ x, (e x).1 = convexQuadraticPhase (ell i) L x) ∧
            ContDiff ℝ ∞ e ∧ ContDiffOn ℝ ∞ e.symm e.target := by
…

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