QuadraticInteriorError.lean`

2 declarations, 0 contain sorry, 0 declared as axioms

Interior radial error from the explicit cutoff comparison

theorem OAI.RegularPointCoordinates.cutoff_inner_energy_le line 19

Source documentation

A nonnegative cutoff equal to one on the inner region dominates its actual gradient energy.

theorem cutoff_inner_energy_le {I Ω : Set X} (hI : MeasurableSet I) (hIΩ : I ⊆ Ω)
    (c w : SobolevSpace μ hQ) (χ : X → ℝ) (C : ℝ≥0)
    (hcrep : SobolevSpace.toLp μ hQ c =ᵐ[μ] χ)
    (hbound : ∀ x, |χ x| ≤ C) (hnonneg : ∀ x, 0 ≤ χ x)
    (hone : ∀ x ∈ I, χ x = 1) :
    (∫ x in I, localGamma μ hQ w w x ∂μ) ≤
      ∫ x in Ω, SobolevSpace.toLp μ hQ c x * localGamma μ hQ w w x ∂μ := by
…

Mentions: OAI.RegularPointCoordinates.SobolevSpace, OAI.RegularPointCoordinates.SobolevSpace.toLp, OAI.RegularPointCoordinates.localGamma

theorem OAI.RegularPointCoordinates.coordinateQuadratic_interior_radial_error line 47

Source documentation

Explicit interior radial error. The right side uses only the value error, actual Gram errors and fixed coordinate/cutoff bounds.

theorem coordinateQuadratic_interior_radial_error {n : ℕ} {I Ω : Set X}
    (hI : MeasurableSet I) (hIΩ : I ⊆ Ω) (hfin : μ Ω ≠ ∞)
    (u : Fin n → SobolevSpace μ hQ) (C D Lχ : ℝ≥0)
    (hu : ∀ j, IsSobolevHarmonicOn μ hQ Ω (u j))
    (hub : ∀ j, ∀ᵐ x ∂μ, |SobolevSpace.toLp μ hQ (u j) x| ≤ C)
    (c q : SobolevSpace μ hQ) (χ : X → ℝ)
    (hχ : LipschitzWith Lχ χ) (hcpt : HasCompactSupport χ)
    (hbound : ∀ x, |χ x| ≤ 1) (hnonneg : ∀ x, 0 ≤ χ x)
    (hsupp : tsupport χ ⊆ Ω) (hcrep : SobolevSpace.toLp μ hQ c =ᵐ[μ] χ)
    (hone : ∀ x ∈ I, χ x = 1)
    (hw : ∀ᵐ x ∂μ, |SobolevSpace.toLp μ hQ (q - coordinateQuadratic μ hQ u C) x| ≤ D)
    {δ M L : ℝ} (hδ : 0 ≤ δ) (hM : 0 ≤ M) (hL : 0 ≤ L)
…

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