RadialQuadraticLimit.lean`

3 declarations, 0 contain sorry, 0 declared as axioms

The radial value limit from Poisson height and metric approximation

theorem OAI.RegularPointCoordinates.radial_quadratic_value_error line 19

Source documentation

The dimensionless radial value error is the sum of the Poisson height error and the explicitly squared metric approximation error.

theorem radial_quadratic_value_error {n : ℕ} {p : X} {r S ε D : ℝ}
    (hr : 0 < r) (hS : 0 ≤ S) (hε : 0 ≤ ε) {V : X → Euclidean n}
    (hmetric : IsPointedApproximation p 0 r S ε V) (hcenter : V p = 0)
    {F : X → ℝ} {x : X} (hx : dist x p ≤ S * r)
    (hheight : |r ^ 2 * F x - dist p x ^ 2 / 2| ≤ r ^ 2 * D) :
    |F x - ‖V x‖ ^ 2 / 2| ≤ D + ε * (2 * S + ε) / 2 := by
…

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

theorem OAI.RegularPointCoordinates.radial_quadratic_mean_bound line 37

Source documentation

A bounded radial value error controls its normalized mean square. The reference measure need only be finite on the ball.

theorem radial_quadratic_mean_bound (μ : Measure X) [BorelSpace X]
    {n : ℕ} {p : X} {r S ε D : ℝ} (hr : 0 < r) (hS : 0 ≤ S)
    (hε : 0 ≤ ε) (hD : 0 ≤ D) (hfin : μ (ball p (S * r)) ≠ ∞)
    {V : X → Euclidean n} (hV : Measurable V)
    (hmetric : IsPointedApproximation p 0 r S ε V) (hcenter : V p = 0)
    {F : X → ℝ} (hF : AEStronglyMeasurable F (μ.restrict (ball p (S * r))))
    (hheight : ∀ᵐ x ∂μ.restrict (ball p (S * r)),
      |r ^ 2 * F x - dist p x ^ 2 / 2| ≤ r ^ 2 * D) :
    (μ.real (ball p (S * r)))⁻¹ *
      (∫ x in ball p (S * r), (F x - ‖V x‖ ^ 2 / 2) ^ 2 ∂μ) ≤
        (D + ε * (2 * S + ε) / 2) ^ 2 := by
…

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

theorem OAI.RegularPointCoordinates.radial_quadratic_mean_tendsto_zero line 80

Source documentation

Vanishing height error and vanishing metric error imply the exact quadratic value limit needed by local Poisson/harmonic compactness.

theorem radial_quadratic_mean_tendsto_zero (μ : Measure X) [BorelSpace X]
    {n : ℕ} {S : ℝ} (hS : 0 ≤ S)
    (p : ℕ → X) (r ε D : ℕ → ℝ) (V : ℕ → X → Euclidean n) (F : ℕ → X → ℝ)
    (hr : ∀ i, 0 < r i) (hε : ∀ i, 0 ≤ ε i) (hD : ∀ i, 0 ≤ D i)
    (hfin : ∀ i, μ (ball (p i) (S * r i)) ≠ ∞)
    (hV : ∀ i, Measurable (V i))
    (hmetric : ∀ i, IsPointedApproximation (p i) 0 (r i) S (ε i) (V i))
    (hcenter : ∀ i, V i (p i) = 0)
    (hF : ∀ i, AEStronglyMeasurable (F i) (μ.restrict (ball (p i) (S * r i))))
    (hheight : ∀ i, ∀ᵐ x ∂μ.restrict (ball (p i) (S * r i)),
      |r i ^ 2 * F i x - dist (p i) x ^ 2 / 2| ≤ r i ^ 2 * D i)
    (hε0 : Tendsto ε atTop (𝓝 0)) (hD0 : Tendsto D atTop (𝓝 0)) :
…

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