QuadraticModelValues.lean`

4 declarations, 0 contain sorry, 0 declared as axioms

Values and local metric accuracy of the actual quadratic model

theorem OAI.RegularPointCoordinates.coordinateQuadratic_bound line 18

theorem OAI.RegularPointCoordinates.coordinateQuadratic_eq_norm line 39

Source documentation

The finite-coordinate definition agrees with the squared Euclidean norm on every region where the columns represent that coordinate map.

theorem coordinateQuadratic_eq_norm {n : ℕ} {Ω : Set X}
    (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 Ω] fun x => v x j) :
    SobolevSpace.toLp μ hQ (coordinateQuadratic μ hQ u C) =ᵐ[μ.restrict Ω]
      fun x => ‖v x‖ ^ 2 / 2 := by
…

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

theorem OAI.RegularPointCoordinates.bounded_metric_coordinates line 56

Source documentation

The actual clipped extensions are harmonic, globally bounded and pointwise unchanged on the metric-approximation region.

theorem bounded_metric_coordinates {n : ℕ} {p : X} {r R ε : ℝ}
    (hr : 0 < r) (hR : 0 ≤ R) (hε : 0 ≤ ε)
    (u : Fin n → SobolevSpace μ hQ) (v : X → Euclidean n)
    (hu : ∀ j, IsSobolevHarmonicOn μ hQ (ball p (R * r)) (u j))
    (hrep : ∀ j, SobolevSpace.toLp μ hQ (u j) =ᵐ[μ.restrict (ball p (R * r))] fun x => v x j)
    (hv : v p = 0)
    (hmetric : IsPointedApproximation p 0 r R ε (fun x => r⁻¹ • v x)) :
    let C : ℝ≥0 := ⟨r * (R + ε), mul_nonneg hr.le (add_nonneg hR hε)⟩
…

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

theorem OAI.RegularPointCoordinates.coordinateQuadratic_metric_value_error line 89

Source documentation

A metric approximation supplies precisely the value-error premise in the cutoff gradient comparison, using the actual coordinate quadratic.

theorem coordinateQuadratic_metric_value_error {n : ℕ} {p : X} {r R ε : ℝ}
    (hr : 0 < r) (hR : 0 ≤ R) (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 (R * r))] fun x => v x j)
    (hv : v p = 0)
    (hmetric : IsPointedApproximation p 0 r R ε (fun x => r⁻¹ • v x))
    (q : SobolevSpace μ hQ)
    (hq : SobolevSpace.toLp μ hQ q =ᵐ[μ.restrict (ball p (R * r))]
      fun x => dist p x ^ 2 / 2) :
    ∀ᵐ x ∂μ.restrict (ball p (R * r)),
      |SobolevSpace.toLp μ hQ (q - coordinateQuadratic μ hQ u C) x| ≤
…

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