RadialQuadraticL2Limit.lean`

3 declarations, 0 contain sorry, 0 declared as axioms

The quadratic radial limit from mean-square Poisson error

theorem OAI.RegularPointCoordinates.coordinateQuadratic_dimensionless_error line 20

Source documentation

Metric approximation controls the dimensionless distance quadratic against the actual bounded coordinate quadratic.

theorem coordinateQuadratic_dimensionless_error {n : ℕ} {p : X} {r S ε : ℝ}
    (hr : 0 < r) (hS : 0 ≤ S) (hε : 0 ≤ ε)
    (u : Fin n → SobolevSpace μ hQ) (C : ℝ≥0) (V : X → Euclidean n)
    (hu : ∀ j, ∀ᵐ x ∂μ, |SobolevSpace.toLp μ hQ (u j) x| ≤ C)
    (hrep : ∀ j, SobolevSpace.toLp μ hQ (u j) =ᵐ[μ.restrict (ball p (S * r))] fun x => V x j)
    (hmetric : IsPointedApproximation p 0 r S ε V) (hcenter : V p = 0)
    (q : SobolevSpace μ hQ)
    (hq : SobolevSpace.toLp μ hQ q =ᵐ[μ.restrict (ball p (S * r))]
      fun x => dist p x ^ 2 / (2 * r ^ 2)) :
    ∀ᵐ x ∂μ.restrict (ball p (S * r)),
      |SobolevSpace.toLp μ hQ (q - coordinateQuadratic μ hQ u C) x| ≤
        ε * (2 * S + ε) / 2 := by
…

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

theorem OAI.RegularPointCoordinates.radial_quadratic_l2_bound line 48

Source documentation

The normalized coordinate error is bounded by the Poisson L2 error plus the metric approximation error. No uniform vanishing height is needed.

theorem radial_quadratic_l2_bound {n : ℕ} {p : X} {r S ε : ℝ}
    (hr : 0 < r) (hS : 0 ≤ S) (hε : 0 ≤ ε)
    (hfin : μ (ball p (S * r)) ≠ ∞)
    (u : Fin n → SobolevSpace μ hQ) (C : ℝ≥0) (V : X → Euclidean n)
    (hu : ∀ j, ∀ᵐ x ∂μ, |SobolevSpace.toLp μ hQ (u j) x| ≤ C)
    (hrep : ∀ j, SobolevSpace.toLp μ hQ (u j) =ᵐ[μ.restrict (ball p (S * r))] fun x => V x j)
    (hmetric : IsPointedApproximation p 0 r S ε V) (hcenter : V p = 0)
    (f q : SobolevSpace μ hQ)
    (hq : SobolevSpace.toLp μ hQ q =ᵐ[μ.restrict (ball p (S * r))]
      fun x => dist p x ^ 2 / (2 * r ^ 2)) :
    ‖normalizeLocalL2 μ (ball p (S * r)) hfin (SobolevSpace.restrictLp μ hQ
      (ball p (S * r)) (f - coordinateQuadratic μ hQ u C))‖ ≤
…

theorem OAI.RegularPointCoordinates.radial_quadratic_l2_limit line 76

Source documentation

Strong mean-square convergence to squared distance and metric approximation give the radial value limit in the Euclidean coordinates.

theorem radial_quadratic_l2_limit {n : ℕ} {S : ℝ} (hS : 0 ≤ S)
    (p : ℕ → X) (r ε : ℕ → ℝ) (u : ℕ → Fin n → SobolevSpace μ hQ)
    (C : ℕ → ℝ≥0) (V : ℕ → X → Euclidean n) (f q : ℕ → SobolevSpace μ hQ)
    (hr : ∀ i, 0 < r i) (hε : ∀ i, 0 ≤ ε i) (hε0 : Tendsto ε atTop (𝓝 0))
    (hfin : ∀ i, μ (ball (p i) (S * r i)) ≠ ∞)
    (hu : ∀ i j, ∀ᵐ x ∂μ, |SobolevSpace.toLp μ hQ (u i j) x| ≤ C i)
    (hrep : ∀ i j, SobolevSpace.toLp μ hQ (u i j) =ᵐ[μ.restrict (ball (p i) (S * r i))]
      fun x => V i x j)
    (hmetric : ∀ i, IsPointedApproximation (p i) 0 (r i) S (ε i) (V i))
    (hcenter : ∀ i, V i (p i) = 0)
    (hq : ∀ i, SobolevSpace.toLp μ hQ (q i) =ᵐ[μ.restrict (ball (p i) (S * r i))]
      fun x => dist (p i) x ^ 2 / (2 * r i ^ 2))
…

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