OAI/Geometry/SurfaceImmersion/Correction/SmoothedMetricStep.lean

GitHub source file

8 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.ClosedSurfaceR4.ExactCorrection.normalizedMetricDefect line 15
2. def OAI.ClosedSurfaceR4.ExactCorrection.realizedMetricError line 18
3. lemma OAI.ClosedSurfaceR4.ExactCorrection.contDiff_pullbackMetric line 23
4. lemma OAI.ClosedSurfaceR4.ExactCorrection.contDiff_metricCrossTerm line 28
5. lemma OAI.ClosedSurfaceR4.ExactCorrection.contDiff_normalizedMetricDefect line 36
6. lemma OAI.ClosedSurfaceR4.ExactCorrection.contDiff_realizedMetricError line 41
7. theorem OAI.ClosedSurfaceR4.ExactCorrection.actual_normalized_defect_identity line 50

   Source documentation

   The chosen error of the smoothed realization controls the actual new normalized defect. This is an identity of concrete maps, before estimates.

   theorem actual_normalized_defect_identity {target Hs : Base → ℝ}
       {δ δ' : ℝ} (hδ : δ ≠ 0) (hδ' : δ' ≠ 0)
       {G S U : Base → V} (hG : ContDiff ℝ ∞ G) (hS : ContDiff ℝ ∞ S)
       (hU : ContDiff ℝ ∞ U) (v w : Base) (x : Base) :
       δ' ^ 2 * (normalizedMetricDefect target δ' (G + U) v w x - target x) =
         δ ^ 2 * (normalizedMetricDefect target δ G v w x - Hs x) -
           realizedMetricError target Hs δ δ' S U v w x - metricCrossTerm (G - S) U x v w := by
   …

   Mentions: OAI.ClosedSurfaceR4.ExactCorrection.normalizedMetricDefect, OAI.ClosedSurfaceR4.ExactCorrection.realizedMetricError, OAI.ClosedSurfaceR4.ExactCorrection.metricCrossTerm

8. theorem OAI.ClosedSurfaceR4.ExactCorrection.normalized_metric_step_bound line 65

   Source documentation

   Weighted estimate for a complete normalized metric update. The three bounds are on the concrete smoothing tail, realization error and cross term.

   theorem normalized_metric_step_bound {target Hs : Base → ℝ}
       (ht : ContDiff ℝ ∞ target) (hs : ContDiff ℝ ∞ Hs)
       {δ δ' τ BH BE BC : ℝ} (hδ : δ ≠ 0) (hδ' : δ' ≠ 0) (hτ : 0 ≤ τ) (m : ℕ)
       {G S U : Base → V} (hG : ContDiff ℝ ∞ G) (hS : ContDiff ℝ ∞ S)
       (hU : ContDiff ℝ ∞ U) (v w : Base)
       (hbH : WeightedBound Set.univ τ m BH (normalizedMetricDefect target δ G v w - Hs))
       (hbE : WeightedBound Set.univ τ m BE (realizedMetricError target Hs δ δ' S U v w))
       (hbC : WeightedBound Set.univ τ m BC (fun x => metricCrossTerm (G - S) U x v w)) :
       WeightedBound Set.univ τ m ((δ' ^ 2)⁻¹ * (δ ^ 2 * BH + BE + BC))
         (normalizedMetricDefect target δ' (G + U) v w - target) := by
   …

   Mentions: OAI.ClosedSurfaceR4.ExactCorrection.normalizedMetricDefect, OAI.ClosedSurfaceR4.ExactCorrection.realizedMetricError, OAI.ClosedSurfaceR4.ExactCorrection.metricCrossTerm