OAI/Geometry/SurfaceImmersion/Correction/BoundedSurfaceCorrection.lean

GitHub source file

8 declarations, 0 contain sorry, 0 declared as axioms

Apply the finite periodic correction to the actual geometric second-jet family, including global smooth extension and its uniform scale bound.

  1. def OAI.ClosedSurfaceR4.SurfaceVelocityFamily.Loop.yData line 21
  2. def OAI.ClosedSurfaceR4.SurfaceVelocityFamily.Loop.cData line 22
  3. def OAI.ClosedSurfaceR4.SurfaceVelocityFamily.Loop.xData line 23
  4. def OAI.ClosedSurfaceR4.SurfaceVelocityFamily.Loop.coefficientExpressions line 25
  5. lemma OAI.ClosedSurfaceR4.SurfaceVelocityFamily.Loop.yData_smooth line 28
  6. lemma OAI.ClosedSurfaceR4.SurfaceVelocityFamily.Loop.cData_smooth line 31
  7. lemma OAI.ClosedSurfaceR4.SurfaceVelocityFamily.Loop.xData_smooth line 35
  8. theorem OAI.ClosedSurfaceR4.SurfaceVelocityFamily.Loop.bounded_surface_correction line 41

    Source documentation

    The loss exponent is fixed by the geometric loop and finite depth, before choosing a slow map or a differentiation order. The same coefficients have cancellation, support, polynomial representation, and the scale bound.

    theorem bounded_surface_correction {S : TopologicalSpace.Opens JetPolynomial.Base}
    {K : Set LowJet} (hK : IsCompact K) (hKO : K ⊆ O)
    (n : ℕ) (ℓ : JetPolynomial.Base →L[ℝ] ℝ) :
    ∃ d : ℕ, ∀ (m : ℕ) (B : ℝ), 1 ≤ B → ∃ D : ℝ, 0 ≤ D ∧
      ∀ (G : JetPolynomial.Base → JetPolynomial.Space) (hG : ContDiff ℝ ∞ G)
        (hGK : MapsTo (lowJet G) S K),
      let g := l.geometry G hG (fun _ hp => hKO (hGK hp))
…

    Mentions: OAI.ClosedSurfaceR4.JetPolynomial.Base, OAI.ClosedSurfaceR4.JetPolynomial.Space