AtlasPolynomialValueBounds.lean`

3 declarations, 0 contain sorry, 0 declared as axioms

The restored polynomial value has one fixed finite loss. Compact local jet ranges suffice: a fixed cutoff removes the irrelevant values away from the outer atlas supports before applying the restoration estimate.

theorem OAI.ClosedSurfaceR4.FiniteOrderSmoothing.SmoothingAtlas.polynomial_outer_cutoff line 33

theorem OAI.ClosedSurfaceR4.FiniteOrderSmoothing.SmoothingAtlas.atlas_polynomial_value_bound line 57

Source documentation

Fixed local low-jet bounds give a global bound on the actual restored polynomial value. Its scale loss is the maximum of the chartwise losses.

theorem atlas_polynomial_value_bound {n : A.centers → ℕ}
    (P : ∀ i : A.centers, Fin 3 → Fin (n i) → Expression)
    (hP : ∀ i k l, (P i k l).SmoothCoeffs univ)
    (U : A.centers → Set JetPolynomial.Base) (hU : ∀ i, IsOpen (U i))
    (houter : ∀ i : A.centers, (chart (i : M)) '' tsupport (A.outer i) ⊆ U i)
    (Q : A.centers → Set LowJet) (hQ : ∀ i, IsCompact (Q i))
    (m : ℕ) (B : A.centers → ℝ) (hB : ∀ i, 1 ≤ B i) :
    ∃ D : ℝ, 0 ≤ D ∧ ∀ (G : M → Space), ContMDiff planeModel spaceModel ∞ G →
      (∀ i, MapsTo (lowJet (A.jetChartMap i G)) (U i) (Q i)) →
      ∀ (s ε : ℝ), 0 < s → s ≤ 1 → 0 ≤ ε → ε ≤ 1 →
      (∀ i, WeightedEstimates.WeightedBound (U i) s (m + tensorOrder (P i)) (B i)
        (lowJet (A.jetChartMap i G))) →
…

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

theorem OAI.ClosedSurfaceR4.FiniteOrderSmoothing.SmoothingAtlas.atlas_polynomial_value_bounds line 153

Source documentation

One profile controls every derivative order, before the actual map and scales are chosen.

theorem atlas_polynomial_value_bounds {n : A.centers → ℕ}
    (P : ∀ i : A.centers, Fin 3 → Fin (n i) → Expression)
    (hP : ∀ i k l, (P i k l).SmoothCoeffs univ)
    (U : A.centers → Set JetPolynomial.Base) (hU : ∀ i, IsOpen (U i))
    (houter : ∀ i : A.centers, (chart (i : M)) '' tsupport (A.outer i) ⊆ U i)
    (Q : A.centers → Set LowJet) (hQ : ∀ i, IsCompact (Q i))
    (B : A.centers → ℕ → ℝ) (hB : ∀ i m, 1 ≤ B i m) :
    ∃ D : ℕ → ℝ, (∀ m, 0 ≤ D m) ∧
      ∀ (G : M → Space), ContMDiff planeModel spaceModel ∞ G →
      (∀ i, MapsTo (lowJet (A.jetChartMap i G)) (U i) (Q i)) →
      ∀ (s ε : ℝ), 0 < s → s ≤ 1 → 0 ≤ ε → ε ≤ 1 →
      (∀ i m, WeightedEstimates.WeightedBound (U i) s (m + tensorOrder (P i)) (B i m)
…