ProjectionResidualValues.lean`

2 declarations, 0 contain sorry, 0 declared as axioms

Uniform values of the normalized actual projection residual

theorem OAI.RegularPointCoordinates.framed_coordinate_value_bound line 20

Source documentation

Centered coordinate values bound every coefficient direction in its own exact normalization frame.

theorem framed_coordinate_value_bound {n : ℕ} (Ω : Set X)
    (u : Fin n → SobolevSpace μ hQ) (V : X → Euclidean n)
    (N : Euclidean n ≃L[ℝ] Euclidean n) {r L : ℝ}
    (hrep : ∀ j, SobolevSpace.toLp μ hQ (u j) =ᵐ[μ.restrict Ω] fun x => V x j)
    (hvalue : ∀ᵐ x ∂μ.restrict Ω,
      ‖(N : Euclidean n →L[ℝ] Euclidean n).adjoint (V x)‖ ≤ L * r)
    (b : Euclidean n) :
    ∀ᵐ x ∂μ.restrict Ω, |SobolevSpace.toLp μ hQ (sobolevColumnMap μ hQ u (N b)) x| ≤
      L * r * ‖b‖ := by
…

Mentions: OAI.RegularPointCoordinates.SobolevSpace, OAI.RegularPointCoordinates.Euclidean, OAI.RegularPointCoordinates.SobolevSpace.toLp, OAI.RegularPointCoordinates.sobolevColumnMap

theorem OAI.RegularPointCoordinates.physical_projection_residual_bound line 41

Source documentation

Both the constant and the linear part of the actual affine fit have size r²; hence the normalized residual is uniformly bounded.

theorem physical_projection_residual_bound {n : ℕ} (Ω : Set X)
    (u : Fin n → SobolevSpace μ hQ) (N : Euclidean n ≃L[ℝ] Euclidean n)
    (v η : SobolevSpace μ hQ) (c : ℝ) (b : Euclidean n)
    {r V H L : ℝ} (hr : 0 < r) (_hH : 0 ≤ H) (_hV : 0 ≤ V) (hL : 0 ≤ L)
    (hv : ∀ᵐ x ∂μ.restrict Ω, |SobolevSpace.toLp μ hQ v x| ≤ V * r ^ 2)
    (hη : SobolevSpace.toLp μ hQ η =ᵐ[μ.restrict Ω] fun _ => (1 : ℝ))
    (hu : ∀ᵐ x ∂μ.restrict Ω, |SobolevSpace.toLp μ hQ (sobolevColumnMap μ hQ u (N b)) x| ≤
      L * r * ‖b‖)
    (hcoeff : |c| + r * ‖b‖ ≤ H * V * r ^ 2) :
    ∀ᵐ x ∂μ.restrict Ω,
      |SobolevSpace.toLp μ hQ ((r ^ 2)⁻¹ • (v - c • η - sobolevColumnMap μ hQ u (N b))) x| ≤
        V + (1 + L) * H * V := by
…

Mentions: OAI.RegularPointCoordinates.SobolevSpace, OAI.RegularPointCoordinates.Euclidean, OAI.RegularPointCoordinates.SobolevSpace.toLp, OAI.RegularPointCoordinates.sobolevColumnMap