UniformPhaseChartBounds.lean`

1 declarations, 0 contain sorry, 0 declared as axioms

Uniform mode coefficients and normal fields on the fixed local phase chart.

theorem OAI.ClosedSurfaceR4.PhaseGeometry.GoodPhaseChart.uniform_mode_bounds line 14

Source documentation

The radius and all constant profiles are fixed before the perturbed map. Only its weighted two-jet size enters, with the explicit polynomial power.

theorem GoodPhaseChart.uniform_mode_bounds {F : RField 4} (hF : ContDiff ℝ ∞ F)
    {φ : Base → ℝ} (c : GoodPhaseChart F φ) :
    ∃ (ρ : ℝ) (D E : ℕ → ℝ), 0 < ρ ∧ (∀ m, 1 ≤ D m) ∧ (∀ m, 1 ≤ E m) ∧
      ∀ (G : RField 4), ContDiff ℝ ∞ G → ∀ C₀ : ℝ, 0 ≤ C₀ → C₀ < ρ →
      WeightedBound univ 1 2 C₀ (G-F) →
      RealModeDomain (G ∘ c.chart.symm) c.chart.target ∧
      ∀ (m : ℕ) (s C : ℝ), 0 < s → 1 ≤ C →
        WeightedBound c.chart.target s m C (realTwoJet (G ∘ c.chart.symm)) →
        ReconstructionCoefficientBound (fun p => complexify ((G ∘ c.chart.symm) p))
          c.chart.target s m ((m.factorial : ℝ) * D m * C^m) ∧
        WeightedBound c.chart.target s m ((m.factorial : ℝ) * E m * C^m)
          (freeNormal (G ∘ c.chart.symm)) := by
…

Mentions: OAI.ClosedSurfaceR4.PhaseGeometry.GoodPhaseChart