AtlasPrimitiveSeedBounds.lean`

4 declarations, 0 contain sorry, 0 declared as axioms

Uniform local jets and global displacement of the actual contracted primitive seed, and its initial normalized polynomial defect.

lemma OAI.ClosedSurfaceR4.FiniteOrderSmoothing.SmoothingAtlas.jetChartMap_const_smul line 34
lemma OAI.ClosedSurfaceR4.FiniteOrderSmoothing.SmoothingAtlas.jetChartMap_primitiveSeed line 43

theorem OAI.ClosedSurfaceR4.FiniteOrderSmoothing.SmoothingAtlas.atlas_primitive_seed_bounds line 50

Source documentation

The compact low-jet range, all local derivative profiles, and the global quadratic displacement profile are chosen before the contraction parameter.

theorem atlas_primitive_seed_bounds
    (F : M → Space) (hF : ContMDiff planeModel spaceModel ∞ F)
    (U : A.centers → Set JetPolynomial.Base) (hU : ∀ i, IsOpen (U i))
    (K : A.centers → Compacts JetPolynomial.Base) (hUK : ∀ i, U i ⊆ K i) :
    ∃ Q : Set LowJet, IsCompact Q ∧
    ∃ J B : A.centers → ℕ → ℝ, ∃ D : ℕ → ℝ,
      (∀ i m, 1 ≤ J i m) ∧ (∀ i m, 1 ≤ B i m) ∧ (∀ m, 0 ≤ D m) ∧
      ∀ δ : ℝ, δ^2 ≤ 1 →
        ContMDiff planeModel spaceModel ∞ (Real.sqrt (1-δ^2) • F) ∧
        (∀ i, MapsTo (lowJet (A.jetChartMap i (Real.sqrt (1-δ^2) • F))) (U i) Q) ∧
        (∀ i m, WeightedEstimates.WeightedBound (U i) 1 m (B i m)
          (lowJet (A.jetChartMap i (Real.sqrt (1-δ^2) • F)))) ∧
…

Mentions: OAI.ClosedSurfaceR4.Space, OAI.ClosedSurfaceR4.planeModel, OAI.ClosedSurfaceR4.JetPolynomial.Base, OAI.ClosedSurfaceR4.WeightedEstimates.WeightedBound

theorem OAI.ClosedSurfaceR4.FiniteOrderSmoothing.SmoothingAtlas.atlas_primitive_seed_defect_bounds line 99

Source documentation

The normalized defect of the contracted seed is globally of order ε/δ², with a fixed all-order profile.

theorem atlas_primitive_seed_defect_bounds {n : A.centers → ℕ}
    (P : ∀ i : A.centers, Fin 3 → Fin (n i) → Expression)
    (hP : ∀ i k l, (P i k l).SmoothCoeffs univ)
    (F : M → Space) (hF : ContMDiff planeModel spaceModel ∞ F)
    (U : A.centers → Set JetPolynomial.Base) (hU : ∀ i, IsOpen (U i))
    (K : A.centers → Compacts JetPolynomial.Base) (hUK : ∀ i, U i ⊆ K i)
    (houter : ∀ i : A.centers, (chart (i : M)) '' tsupport (A.outer i) ⊆ U i) :
    ∃ D E : ℕ → ℝ, (∀ m, 0 ≤ D m) ∧ (∀ m, 0 ≤ E m) ∧
      ∀ (δ ε : ℝ), δ ≠ 0 → δ^2 ≤ 1 → 0 ≤ ε → ε ≤ 1 →
        (∀ m, A.WeightedBound 1 m (D m * δ^2) (Real.sqrt (1-δ^2) • F-F)) ∧
        (∀ m, A.TensorWeightedBound 1 m (E m * ε / δ^2)
          (A.normalizedPolynomialDefect P ε δ (inducedTensor F)
…

Mentions: OAI.ClosedSurfaceR4.Space, OAI.ClosedSurfaceR4.planeModel, OAI.ClosedSurfaceR4.JetPolynomial.Base, OAI.ClosedSurfaceR4.FiniteOrderSmoothing.chart, OAI.ClosedSurfaceR4.FiniteOrderSmoothing.inducedTensor