Lower bounds for the mixed gradient and mirror residual in above-two geometry.

theorem V7.Stage4AboveTwo.scalar_power_deficit_le {p t y : ℝ} (hp : 2 < p) (ht : 0 ≤ t) (hy : 0 ≤ y) : t / 2 * y ^ 2 - aboveUniformConstant p * y ^ p ≤ aboveErrorConstant p * t ^ aboveErrorPower p

theorem V7.Stage4AboveTwo.mixedResidual_lower {p u d x y : ℝ} (hp : 2 < p) (hu : 0 < u) (hy : 0 ≤ y) : u / 2 * x ^ 2 + aboveUniformConstant p * y ^ p - d * x * y ≥ -(aboveErrorConstant p * (d ^ 2 / u) ^ aboveErrorPower p)

theorem V7.Stage4AboveTwo.mixedVectorResidual_lower {m : ℕ} {p u d : ℝ} (hp : 2 < p) (hu : 0 < u) (hd : 0 ≤ d) (a b : Point m) : u / 2 * lpNorm (conjugateExponent p) a ^ 2 + aboveUniformConstant p * lpNorm p b ^ p + d * pairing a b ≥ -(aboveErrorConstant p * (d ^ 2 / u) ^ aboveErrorPower p)

noncomputable def V7.Stage4AboveTwo.aboveMixedResidual {d : ℕ} (p : ℝ) (n : ℕ) (u dw : ScalarSeq) (A B : VectorSeq d) : ℝ

The sum of quadratic gradient, power mirror, and mixed-pairing residual terms.

Equations

• One or more equations did not get rendered due to their size.

theorem V7.Stage4AboveTwo.aboveMixedResidual_lower {d : ℕ} (p : ℝ) (hp : 2 < p) (n : ℕ) (u dw : ScalarSeq) (A B : VectorSeq d) (hu : ∀ k < n, 0 < u k) (hdw : ∀ k < n, 0 ≤ dw k) : aboveMixedResidual p n u dw A B ≥ -aboveErrorSum p n u dw