ConvexPhaseDecomposition.lean`

10 declarations, 0 contain sorry, 0 declared as axioms

The actual positive coefficient forms of the three convex phases. The chart and cone radii are chosen together before a path metric.

def OAI.ClosedSurfaceR4.PhaseGeometry.convexPhaseCovectors line 15
lemma OAI.ClosedSurfaceR4.PhaseGeometry.convexPhaseCovectors_smooth line 18
lemma OAI.ClosedSurfaceR4.PhaseGeometry.convexPhaseCovectors_eq_phaseDerivative line 24
lemma OAI.ClosedSurfaceR4.PhaseGeometry.convexPhaseCovectors_dist line 30
def OAI.ClosedSurfaceR4.PhaseGeometry.convexPhaseCoefficient line 37
lemma OAI.ClosedSurfaceR4.PhaseGeometry.convexPhaseCoefficient_smoothAt line 41
lemma OAI.ClosedSurfaceR4.PhaseGeometry.convexPhaseCoefficient_decomposition line 48

theorem OAI.ClosedSurfaceR4.PhaseGeometry.compact_positive_convex_phase_charts line 59

Source documentation

One sufficiently small disk retains both the actual positive basis coefficients and the positive metric Hessians for every fixed compact family of admissible metric first jets.

theorem compact_positive_convex_phase_charts (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 : ℝ, 0 < L ∧ 0 < r ∧
      (∀ p : Base, ‖p‖ ≤ r →
        (perturbedPhaseOperator P (convexPhaseCovectors P L p)).IsInvertible ∧
        (∀ H ∈ T, ∀ i, 0 < convexPhaseCoefficient P L p i H) ∧
        (∀ i, ContDiffAt ℝ ∞ (fun x => convexPhaseCoefficient P L x i) p)) ∧
      ∀ (h : Base → PhaseMean.Tensor) (p : Base), ‖p‖ ≤ r →
        (h p,fderiv ℝ h p) ∈ J → ∀ i,
…

Mentions: OAI.ClosedSurfaceR4.PhaseGeometry.PhaseBasis, OAI.ClosedSurfaceR4.PhaseMean.Tensor, OAI.ClosedSurfaceR4.PhaseGeometry.MetricFirstJet, OAI.ClosedSurfaceR4.PhaseGeometry.metricJetDet, OAI.ClosedSurfaceR4.PhaseGeometry.perturbedPhaseOperator, OAI.ClosedSurfaceR4.PhaseGeometry.convexPhaseCovectors, OAI.ClosedSurfaceR4.PhaseGeometry.convexPhaseCoefficient

theorem OAI.ClosedSurfaceR4.PhaseGeometry.convex_phase_charts_on_disk line 96

Source documentation

Shrinking once supplies a single chart for each entire closed disk, instead of choosing a different local chart at each of its points.

theorem convex_phase_charts_on_disk (P : PhaseBasis) {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 = convexQuadraticPhase (P.ξ i) L x) ∧
        (∀ i, ContDiff ℝ ∞ (e i) ∧ ContDiffOn ℝ ∞ (e i).symm (e i).target) ∧
        ∀ i p, ‖p‖ ≤ r → p ∈ (e i).source := by
…

Mentions: OAI.ClosedSurfaceR4.PhaseGeometry.PhaseBasis, OAI.ClosedSurfaceR4.PhaseGeometry.convexQuadraticPhase

theorem OAI.ClosedSurfaceR4.PhaseGeometry.compact_perturbed_convex_phase_margin line 124
Source documentation
The cone and Hessian margins persist under small independent changes of the linear parts, with the same quadratic coefficient and disk.
```
theorem compact_perturbed_convex_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 → ∀ p : Base, ‖p‖ ≤ r →
        let xi := fun i => phaseDerivative (convexQuadraticPhase (ell i) L) p
…
```
Mentions: OAI.ClosedSurfaceR4.PhaseGeometry.PhaseBasis, OAI.ClosedSurfaceR4.PhaseMean.Tensor, OAI.ClosedSurfaceR4.PhaseGeometry.MetricFirstJet, OAI.ClosedSurfaceR4.PhaseGeometry.metricJetDet, OAI.ClosedSurfaceR4.phaseDerivative, OAI.ClosedSurfaceR4.PhaseGeometry.convexQuadraticPhase