OAI/Geometry/SurfaceImmersion/Primitive/SurfacePrimitiveError.lean

GitHub source file

4 declarations, 0 contain sorry, 0 declared as axioms

The finite primitive's actual metric error is the sum of its solved mean error and the fast finite tail. The prescribed amplitude is fixed in position.

  1. def OAI.ClosedSurfaceR4.SurfaceVelocityFamily.Loop.meanOperator line 16
  2. lemma OAI.ClosedSurfaceR4.SurfaceVelocityFamily.Loop.meanOperator_smooth line 24
  3. lemma OAI.ClosedSurfaceR4.SurfaceVelocityFamily.Loop.meanMetric_eq_meanOperator line 33
  4. theorem OAI.ClosedSurfaceR4.SurfaceVelocityFamily.Loop.compact_primitive_error line 47

    Source documentation

    A solved mean equation controls the actual primitive metric at every finite weighted order. The tail loss is chosen before the order or slow map.

    theorem compact_primitive_error {a : Base → ℝ} (ha : ContDiff ℝ ∞ a)
    (hamp : l.HasSpatialAmplitude a) {S : TopologicalSpace.Opens Base}
    {K : Set LowJet} (hK : IsCompact K) (hKO : K ⊆ O)
    (n : ℕ) (b c : Bool) (ℓ : Base →L[ℝ] ℝ)
    (hℓx : ℓ (coordinateVector 0) = 1) (hℓy : ℓ (coordinateVector 1) = 0) :
    ∃ d : ℕ, ∀ (m : ℕ) (B : ℝ), 1 ≤ B → ∃ D : ℝ, 0 ≤ D ∧
      ∀ (G : JetPolynomial.Base → JetPolynomial.Space) (hG : ContDiff ℝ ∞ G) (hGK : MapsTo (lowJet G) S K)
        (s z : ℝ), 0 < z → z ≤ s → s ≤ 1 →
      WeightedBound S s (m+(2*(n+1)+1)) B (lowJet G) →
      let g := l.geometry G hG (fun _ hp => hKO (hGK hp))
…

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