CorrectionMetricIdentity.lean`

6 declarations, 0 contain sorry, 0 declared as axioms

Updating the unsmoothed map

The exact algebraic identity in the smoothing iteration. The difference between the true and smoothed metric increments is bilinear in the smoothing tail and the new increment, with no square of the tail.

def OAI.ClosedSurfaceR4.ExactCorrection.pullbackMetric line 21
def OAI.ClosedSurfaceR4.ExactCorrection.metricCrossTerm line 24
theorem OAI.ClosedSurfaceR4.ExactCorrection.pullbackMetric_add line 28
theorem OAI.ClosedSurfaceR4.ExactCorrection.metricCrossTerm_sub line 38

theorem OAI.ClosedSurfaceR4.ExactCorrection.unsmoothed_metric_increment line 48

Source documentation

Comparing increments at the true map and its smoothing requires only one copy of the smoothing tail.

theorem unsmoothed_metric_increment {G S U : E → V} {x : E}
    (hG : DifferentiableAt ℝ G x) (hS : DifferentiableAt ℝ S x)
    (hU : DifferentiableAt ℝ U x) (v w : E) :
    pullbackMetric (fun y => G y + U y) x v w - pullbackMetric G x v w =
      pullbackMetric (fun y => S y + U y) x v w - pullbackMetric S x v w +
        metricCrossTerm (fun y => G y - S y) U x v w := by
…

Mentions: OAI.ClosedSurfaceR4.ExactCorrection.pullbackMetric, OAI.ClosedSurfaceR4.ExactCorrection.metricCrossTerm

theorem OAI.ClosedSurfaceR4.ExactCorrection.normalized_defect_identity line 61

Source documentation

The normalized error identity after the target amplitude is changed. The hypotheses identify the old defect, new defect, and smoothed increment error; they impose no estimate or existence assumption.

theorem normalized_defect_identity {G S U : E → V} {x : E}
    (hG : DifferentiableAt ℝ G x) (hS : DifferentiableAt ℝ S x)
    (hU : DifferentiableAt ℝ U x) (v w : E)
    (δ δ' target H Hs H' error : ℝ)
    (hold : δ ^ 2 * H = target - pullbackMetric G x v w)
    (hnew : δ' ^ 2 * H' = target - pullbackMetric (fun y => G y + U y) x v w)
    (herror : error = pullbackMetric (fun y => S y + U y) x v w -
      pullbackMetric S x v w - (δ ^ 2 * Hs - δ' ^ 2 * target)) :
    δ' ^ 2 * (H' - target) = δ ^ 2 * (H - Hs) - error -
      metricCrossTerm (fun y => G y - S y) U x v w := by
…

Mentions: OAI.ClosedSurfaceR4.ExactCorrection.pullbackMetric, OAI.ClosedSurfaceR4.ExactCorrection.metricCrossTerm