OAI/Geometry/SurfaceImmersion/Correction/SupportedPolynomialOperator.lean

GitHub source file

3 declarations, 0 contain sorry, 0 declared as axioms

The actual polynomial linearization as an operator on smooth fields of fixed compact support, with its finite derivative-loss seminorm estimate.

  1. def OAI.ClosedSurfaceR4.JetPolynomial.Expression.variationLM line 20
  2. lemma OAI.ClosedSurfaceR4.JetPolynomial.Expression.variationLM_apply line 36
  3. theorem OAI.ClosedSurfaceR4.JetPolynomial.Expression.variationLM_bound line 44

    Source documentation

    A fixed finite derivative loss suffices at every output order. The operator acts on genuine supported smooth functions, not a Banach completion.

    theorem variationLM_bound {Q : Set LowJet} (hO : IsOpen O) (hU : IsOpen U)
    (hQcompact : IsCompact Q) (hQO : Q ⊆ O) (he : e.SmoothCoeffs O)
    (K : Compacts Base) (hKU : (K : Set Base) ⊆ U) (m : ℕ) (B : ℝ) (hB : 1 ≤ B) :
    ∃ D : ℝ, 0 ≤ D ∧ ∀ (G : Base → Space) (hG : ContDiff ℝ ∞ G)
      (hGQ : Set.MapsTo (lowJet G) U Q) (s : ℝ≥0), 0 < (s : ℝ) → s ≤ 1 →
      WeightedBound U s (m + e.order) B (lowJet G) →
      ∀ t ∈ Set.Icc (0 : ℝ) 1, ∀ H : SupportedField (F := Space) K,
…

    Mentions: OAI.ClosedSurfaceR4.JetPolynomial.LowJet, OAI.ClosedSurfaceR4.JetPolynomial.Base, OAI.ClosedSurfaceR4.JetPolynomial.Space, OAI.ClosedSurfaceR4.JetPolynomial.lowJet, OAI.ClosedSurfaceR4.JetPolynomial.SupportedField