ConstantDirectionError.lean`

2 declarations, 0 contain sorry, 0 declared as axioms

From recovered affine coefficients to the constant direction

theorem OAI.RegularPointCoordinates.normalized_constant_direction_error line 20

Source documentation

The two-center radial derivative is close to the actual displacement once its affine linear and constant coefficients have been recovered.

theorem normalized_constant_direction_error {n : ℕ}
    (Ω : Set X) (hfin : μ Ω ≠ ∞) (hpos : μ Ω ≠ 0) (η : SobolevSpace μ hQ)
    (hη : SobolevSpace.toLp μ hQ η =ᵐ[μ.restrict Ω] fun _ => (1 : ℝ))
    (U H : Euclidean n →L[ℝ] SobolevSpace μ hQ) (B : Euclidean n →L[ℝ] Euclidean n)
    (c d : Euclidean n →L[ℝ] ℝ) {e R L D : ℝ} (hR : 0 ≤ R)
    (hU : ∀ b, ‖normalizeLocalL2 μ Ω hfin (SobolevSpace.restrictLp μ hQ Ω (U b))‖ ≤ R * ‖b‖)
    (hfit : ∀ b, ‖normalizeLocalL2 μ Ω hfin (SobolevSpace.restrictLp μ hQ Ω
      (H b - U (B b) - c b • η))‖ ≤ e * ‖b‖)
    (hB : ‖B‖ ≤ L) (hconst : ‖c - d‖ ≤ D) (b : Euclidean n) :
    ‖normalizeLocalL2 μ Ω hfin (SobolevSpace.restrictLp μ hQ Ω (H b - d b • η))‖ ≤
      (e + R * L + D) * ‖b‖ := by
…

Mentions: OAI.RegularPointCoordinates.SobolevSpace, OAI.RegularPointCoordinates.SobolevSpace.toLp, OAI.RegularPointCoordinates.Euclidean, OAI.RegularPointCoordinates.normalizeLocalL2, OAI.RegularPointCoordinates.SobolevSpace.restrictLp

theorem OAI.RegularPointCoordinates.normalized_two_center_direction_error line 56

Source documentation

In the two-center application the affine constant is the displaced coordinate covector composed with the first radial matrix. Both recovered coefficient estimates therefore give the desired constant direction.

theorem normalized_two_center_direction_error {n : ℕ}
    (Ω : Set X) (hfin : μ Ω ≠ ∞) (hpos : μ Ω ≠ 0) (η : SobolevSpace μ hQ)
    (hη : SobolevSpace.toLp μ hQ η =ᵐ[μ.restrict Ω] fun _ => (1 : ℝ))
    (U H : Euclidean n →L[ℝ] SobolevSpace μ hQ)
    (Ax Az : Euclidean n →L[ℝ] Euclidean n) (c d : Euclidean n →L[ℝ] ℝ)
    {e R L D M : ℝ} (hR : 0 ≤ R) (hx : ‖Ax - 1‖ ≤ 1 / 2) (hc : c = d.comp Ax)
    (hU : ∀ b, ‖normalizeLocalL2 μ Ω hfin (SobolevSpace.restrictLp μ hQ Ω (U b))‖ ≤ R * ‖b‖)
    (hfit : ∀ b, ‖normalizeLocalL2 μ Ω hfin (SobolevSpace.restrictLp μ hQ Ω
      (H b - U ((Az - Ax) b) - c b • η))‖ ≤ e * ‖b‖)
    (hB : ‖Az - Ax‖ ≤ L) (hM : ‖c‖ ≤ M) (hconst : ‖c.comp (Az - 1)‖ ≤ D)
    (b : Euclidean n) :
    ‖normalizeLocalL2 μ Ω hfin (SobolevSpace.restrictLp μ hQ Ω (H b - d b • η))‖ ≤
…