OAI/Geometry/SurfaceImmersion/Correction/AtlasPrimitiveMean.lean

GitHub source file

9 declarations, 0 contain sorry, 0 declared as axioms

Exact normalized mean identities for the global primitive iteration. The residual is always that of the actual restored polynomial metric.

  1. def OAI.ClosedSurfaceR4.FiniteOrderSmoothing.SmoothingAtlas.normalizedPolynomialDefect line 28
  2. def OAI.ClosedSurfaceR4.FiniteOrderSmoothing.SmoothingAtlas.polynomialMeanTarget line 33
  3. lemma OAI.ClosedSurfaceR4.FiniteOrderSmoothing.SmoothingAtlas.polynomialMeanTarget_eq line 39
  4. lemma OAI.ClosedSurfaceR4.FiniteOrderSmoothing.SmoothingAtlas.normalizedPolynomialDefect_smooth line 51
  5. lemma OAI.ClosedSurfaceR4.FiniteOrderSmoothing.SmoothingAtlas.polynomialMeanTarget_smooth line 62
  6. lemma OAI.ClosedSurfaceR4.FiniteOrderSmoothing.SmoothingAtlas.normalizedPolynomialDefect_seed line 75
  7. lemma OAI.ClosedSurfaceR4.FiniteOrderSmoothing.SmoothingAtlas.normalizedPolynomialDefect_after_step line 92
  8. lemma OAI.ClosedSurfaceR4.FiniteOrderSmoothing.SmoothingAtlas.polynomialMeanTarget_bound line 128

    Source documentation

    The next input stays in the same bounded family whenever the old normalized defect does.

    lemma polynomialMeanTarget_bound
    {P : (i : A.centers) → Fin 3 → Fin (n i) → Expression}
    (hP : ∀ i k l, (P i k l).SmoothCoeffs univ)
    {ε δ δ' s A₀ B₀ : ℝ} {m : ℕ} (hδ : 0 < δ) (hδ' : 0 ≤ δ')
    (hδδ : δ' ≤ δ) (hs : 0 ≤ s) (hA₀ : 0 ≤ A₀)
    {γ : ∀ x : M, CovariantTwoTensor x}
    (hγ : ContMDiff planeModel (planeModel.prod 𝓘(ℝ,TensorFiber)) ∞
      (fun x => TotalSpace.mk' TensorFiber x (γ x)))
    {G : M → Space} (hG : ContMDiff planeModel spaceModel ∞ G)
    (hγb : A.TensorWeightedBound s m A₀ γ)
    (hDb : A.TensorWeightedBound s m B₀ (A.normalizedPolynomialDefect P ε δ γ G)) :
    A.TensorWeightedBound s m (2*A₀+B₀) (A.polynomialMeanTarget P ε δ δ' γ G) := by
…

    Mentions: OAI.ClosedSurfaceR4.FiniteOrderSmoothing.CovariantTwoTensor, OAI.ClosedSurfaceR4.planeModel, OAI.ClosedSurfaceR4.FiniteOrderSmoothing.TensorFiber, OAI.ClosedSurfaceR4.Space

  9. lemma OAI.ClosedSurfaceR4.FiniteOrderSmoothing.SmoothingAtlas.polynomialMeanTarget_distance line 158

    Source documentation

    Quantitative closeness of the next input in the fixed tensor encoding.

    lemma polynomialMeanTarget_distance
    (P : (i : A.centers) → Fin 3 → Fin (n i) → Expression) (ε δ δ' : ℝ)
    (γ : ∀ x : M, CovariantTwoTensor x) (G : M → Space)
    (x : JetPolynomial.Base) {a b : ℝ}
    (hD : ‖A.tensorEncode (A.normalizedPolynomialDefect P ε δ γ G) x‖ ≤ a)
    (hγ : ‖A.tensorEncode γ x‖ ≤ b) :
    ‖A.tensorEncode (A.polynomialMeanTarget P ε δ δ' γ G) x-A.tensorEncode γ x‖ ≤
      a+(δ'^2/δ^2)*b := by
…

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