UniformPhaseChartSolver.lean`

2 declarations, 0 contain sorry, 0 declared as axioms

One fixed phase chart supplies solvers throughout a controlled C2 neighborhood.

theorem OAI.ClosedSurfaceR4.PhaseGeometry.GoodPhaseChart.uniform_unperturbed_solvers_all_profiles line 15

Source documentation

The chart, coordinate constants and reconstruction profile are chosen before the nearby map, wavelength and slow scale.

theorem GoodPhaseChart.uniform_unperturbed_solvers_all_profiles
    {F : JetPolynomial.Base → JetPolynomial.Space} (hF : ContDiff ℝ ∞ F)
    {φ : JetPolynomial.Base → ℝ} (hφ : ContDiff ℝ ∞ φ)
    (e : GoodPhaseChart (F ∘ planeCoordinateIsometry.symm) (coordinatePhase φ))
    (K : Compacts JetPolynomial.Base)
    (hK : (modeSupport K : Set SmallModes.Base) ⊆ e.chart.source)
    : ∃ ρ : ℝ, 0 < ρ ∧ ∀ (A : ℕ → ℝ), (∀ m, 1 ≤ A m) →
    ∃ C J : ℕ → ℝ, (∀ m, 0 ≤ C m) ∧ (∀ m, 1 ≤ J m) ∧
      ∀ (G : JetPolynomial.Base → JetPolynomial.Space) (hG : ContDiff ℝ ∞ G)
        (B : ℝ), 0 ≤ B → B < ρ →
      WeightedBound univ 1 2 B
        ((G ∘ planeCoordinateIsometry.symm) - (F ∘ planeCoordinateIsometry.symm)) →
…

Mentions: OAI.ClosedSurfaceR4.JetPolynomial.Base, OAI.ClosedSurfaceR4.JetPolynomial.Space, OAI.ClosedSurfaceR4.PhaseGeometry.GoodPhaseChart, OAI.ClosedSurfaceR4.SmallModes.Base

theorem OAI.ClosedSurfaceR4.PhaseGeometry.GoodPhaseChart.uniform_unperturbed_solvers line 82

Source documentation

The chart, coordinate constants and reconstruction profile are chosen before the nearby map, wavelength and slow scale.

theorem GoodPhaseChart.uniform_unperturbed_solvers
    {F : JetPolynomial.Base → JetPolynomial.Space} (hF : ContDiff ℝ ∞ F)
    {φ : JetPolynomial.Base → ℝ} (hφ : ContDiff ℝ ∞ φ)
    (e : GoodPhaseChart (F ∘ planeCoordinateIsometry.symm) (coordinatePhase φ))
    (K : Compacts JetPolynomial.Base)
    (hK : (modeSupport K : Set SmallModes.Base) ⊆ e.chart.source)
    (A : ℕ → ℝ) (hA : ∀ m, 1 ≤ A m) :
    ∃ (ρ : ℝ) (C J : ℕ → ℝ), 0 < ρ ∧ (∀ m, 0 ≤ C m) ∧ (∀ m, 1 ≤ J m) ∧
      ∀ (G : JetPolynomial.Base → JetPolynomial.Space) (hG : ContDiff ℝ ∞ G)
        (B : ℝ), 0 ≤ B → B < ρ →
      WeightedBound univ 1 2 B
        ((G ∘ planeCoordinateIsometry.symm) - (F ∘ planeCoordinateIsometry.symm)) →
…

Mentions: OAI.ClosedSurfaceR4.JetPolynomial.Base, OAI.ClosedSurfaceR4.JetPolynomial.Space, OAI.ClosedSurfaceR4.PhaseGeometry.GoodPhaseChart, OAI.ClosedSurfaceR4.SmallModes.Base