OAI/Geometry/SurfaceImmersion/Correction/PrimitiveMeanStep.lean

GitHub source file

10 declarations, 0 contain sorry, 0 declared as axioms

The normalized target and error in successive primitive mean steps. The target is defined from the actual old mean metric; its next defect is exactly the rescaled error of the constructed increment.

  1. def OAI.ClosedSurfaceR4.PrimitiveRealization.normalizedMeanDefect line 14
  2. def OAI.ClosedSurfaceR4.PrimitiveRealization.primitiveMeanTarget line 17
  3. lemma OAI.ClosedSurfaceR4.PrimitiveRealization.primitiveMeanTarget_eq line 20
  4. lemma OAI.ClosedSurfaceR4.PrimitiveRealization.primitiveMeanTarget_smooth line 28
  5. lemma OAI.ClosedSurfaceR4.PrimitiveRealization.normalizedMeanDefect_smooth line 33
  6. lemma OAI.ClosedSurfaceR4.PrimitiveRealization.primitiveMeanTarget_identity line 38
  7. lemma OAI.ClosedSurfaceR4.PrimitiveRealization.primitiveMeanTarget_distance line 45
  8. lemma OAI.ClosedSurfaceR4.PrimitiveRealization.primitiveMeanTarget_bound line 63
  9. lemma OAI.ClosedSurfaceR4.PrimitiveRealization.normalizedMeanDefect_after_step line 84
  10. lemma OAI.ClosedSurfaceR4.PrimitiveRealization.normalizedMeanDefect_after_local_step line 109

    Source documentation

    A cutoff extension of the target gives the same next defect wherever it agrees with the actual primitive mean target.

    lemma normalizedMeanDefect_after_local_step {U : Set SmallModes.Base} (hU : IsOpen U)
    {γ P Q H : SmallModes.Base → Tensor} (hγ : ContDiff ℝ ∞ γ)
    (hP : ContDiff ℝ ∞ P) (hQ : ContDiff ℝ ∞ Q)
    {δ δ' s C : ℝ} {m : ℕ} (hδ : δ ≠ 0) (hδ' : δ' ≠ 0)
    (hH : ∀ x ∈ U, H x = primitiveMeanTarget δ δ' γ P x)
    (hb : WeightedBound U s m C (Q-P-(δ^2 : ℝ) • H)) :
    WeightedBound U s m (C / δ'^2) (normalizedMeanDefect δ' γ Q) := by
…

    Mentions: OAI.ClosedSurfaceR4.SmallModes.Base, OAI.ClosedSurfaceR4.PrimitiveRealization.primitiveMeanTarget, OAI.ClosedSurfaceR4.PrimitiveRealization.normalizedMeanDefect