AffineCommutatorIdentity.lean`

2 declarations, 0 contain sorry, 0 declared as axioms

The affine coefficient identity behind the two-center commutator

Here U is the centered coordinate column, G its radial derivative at z, H the difference of the two radial derivatives, and C the constant part of the affine approximation to H. D and V are the actual radial derivative maps; J is restriction to the common L2 region.

theorem OAI.RegularPointCoordinates.affine_commutator_identity line 22

Source documentation

The coefficient expression is a sum of the genuine commutator error and the four value/gradient errors of the two radial approximations.

theorem affine_commutator_identity
    (A B : Module.End ℝ E) (U G H C : E →ₗ[ℝ] F) (D V J : F →ₗ[ℝ] W)
    (hDU : ∀ a, D (U a) = J (G a))
    (hVU : ∀ a, V (U a) = J (H a))
    (hDC : ∀ a, D (C a) = 0) (b : E) :
    J (U ((A * B - B * (A - 1)) b)) - J (C ((A - 1) b)) =
      V (G b - U (A b)) - (V (G b) - D (H b) - J (H b)) -
        D (H b - U (B b) - C b) +
        J (H ((A - 1) b) - U (B ((A - 1) b)) - C ((A - 1) b)) -
        J (G (B b) - U (A (B b))) := by
…

theorem OAI.RegularPointCoordinates.affine_commutator_error_bound line 41

Source documentation

The exact identity keeps the five analytic errors additive. No small matrix term is absorbed before affine coefficient nondegeneracy is used.

theorem affine_commutator_error_bound
    (A B : Module.End ℝ E) (U G H C : E →ₗ[ℝ] F) (D V J : F →ₗ[ℝ] Y)
    (hDU : ∀ a, D (U a) = J (G a))
    (hVU : ∀ a, V (U a) = J (H a))
    (hDC : ∀ a, D (C a) = 0) (b : E)
    {e₁ e₂ e₃ e₄ e₅ : ℝ}
    (h₁ : ‖V (G b - U (A b))‖ ≤ e₁)
    (h₂ : ‖V (G b) - D (H b) - J (H b)‖ ≤ e₂)
    (h₃ : ‖D (H b - U (B b) - C b)‖ ≤ e₃)
    (h₄ : ‖J (H ((A - 1) b) - U (B ((A - 1) b)) - C ((A - 1) b))‖ ≤ e₄)
    (h₅ : ‖J (G (B b) - U (A (B b)))‖ ≤ e₅) :
    ‖J (U ((A * B - B * (A - 1)) b)) - J (C ((A - 1) b))‖ ≤
…