ProjectionCoordinateValues.lean`

1 declarations, 0 contain sorry, 0 declared as axioms

Actual centered coordinate bounds on the projection region

theorem OAI.RegularPointCoordinates.projection_coordinate_values line 21

Source documentation

The existing metric approximation supplies the physical coordinate value estimate used in the two-center projection. The bound is uniform in the scale, frame, and covector.

theorem projection_coordinate_values {n : ℕ} {p : X} {s epsilon : ℝ}
    (hs : 0 < s) (hepsilon : epsilon ≤ 1)
    (u : Fin n → SobolevSpace μ hQ) (V : X → Euclidean n)
    (N : Euclidean n ≃L[ℝ] Euclidean n) (hcenter : V p = 0)
    (hrep : ∀ j, SobolevSpace.toLp μ hQ (u j) =ᵐ[
      μ.restrict (ball p (s / 512))] fun x => V x j)
    (hmetric : IsPointedApproximation p 0 (s / 64) 4 epsilon
      (fun x => (s / 64)⁻¹ • (N : Euclidean n →L[ℝ] Euclidean n).adjoint (V x))) :
    ∀ b : Euclidean n, ∀ᵐ x ∂μ.restrict (ball p (s / 512)),
      |SobolevSpace.toLp μ hQ (sobolevColumnMap μ hQ u (N b)) x| ≤ s * ‖b‖ := by
…

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