QuadraticUniformBounds.lean`

3 declarations, 0 contain sorry, 0 declared as axioms

Uniform constants in the quadratic-model gradient comparison

theorem OAI.RegularPointCoordinates.gamma_abs_le_of_bounds line 18

Source documentation

Cauchy--Schwarz with the actual local square-gradient bounds.

theorem gamma_abs_le_of_bounds {Ω : Set X} (f g : SobolevSpace μ hQ)
    {A B : ℝ} (hA : 0 ≤ A) (hB : 0 ≤ B)
    (hf : ∀ᵐ x ∂μ.restrict Ω, localGamma μ hQ f f x ≤ A ^ 2)
    (hg : ∀ᵐ x ∂μ.restrict Ω, localGamma μ hQ g g x ≤ B ^ 2) :
    ∀ᵐ x ∂μ.restrict Ω, |localGamma μ hQ f g x| ≤ A * B := by
…

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

theorem OAI.RegularPointCoordinates.coordinateQuadratic_cutoff_bound line 31

Source documentation

Bounded coordinate values and gradients control the cutoff cross term of their actual quadratic potential.

theorem coordinateQuadratic_cutoff_bound {n : ℕ} {Ω : Set X}
    (u : Fin n → SobolevSpace μ hQ) (C : ℝ≥0) (c : SobolevSpace μ hQ)
    (hub : ∀ j, ∀ᵐ x ∂μ, |SobolevSpace.toLp μ hQ (u j) x| ≤ C)
    {M L : ℝ} (hM : 0 ≤ M) (hL : 0 ≤ L)
    (hu : ∀ j, ∀ᵐ x ∂μ.restrict Ω, localGamma μ hQ (u j) (u j) x ≤ M ^ 2)
    (hc : ∀ᵐ x ∂μ.restrict Ω, localGamma μ hQ c c x ≤ L ^ 2) :
    ∀ᵐ x ∂μ.restrict Ω,
      |localGamma μ hQ c (coordinateQuadratic μ hQ u C) x| ≤ (n : ℝ) * C * M * L := by
…

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

theorem OAI.RegularPointCoordinates.coordinateQuadratic_uniform_value_gradient line 58

Source documentation

The gradient comparison now has explicit constants from coordinate and cutoff bounds, with no separate cross-term assumption.

theorem coordinateQuadratic_uniform_value_gradient {n : ℕ} {Ω : Set X}
    (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 =ᵐ[μ] χ)
    (hw : ∀ᵐ x ∂μ, |SobolevSpace.toLp μ hQ (q - coordinateQuadratic μ hQ u C) x| ≤ D)
    {δ M L : ℝ} (hδ : 0 ≤ δ) (hM : 0 ≤ M) (hL : 0 ≤ L)
    (hsmall : ∀ᵐ x ∂μ.restrict Ω,
…

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