Stampacchia

Ported from scottnarmstrong/CoarseGraining at c7ddd76c08ade64fed1b8d2ca51be14dfee8deb4. Module imports, support namespace and local option directives adapted for Lean Pool.

The coupled Stampacchia estimate (Proposition 3.3)

The H1 assembly. Given the coupled weak form on the centered open triadic cube U = openCubeSet (originCube d m), there is a constant c (the median of the pair (v − ½p·x, −v* + ½p·x)) such that, almost everywhere on U, |v − ½p·x − c| ≤ C_d · L · M and |v* − ½p·x + c| ≤ C_d · L · M, with L = 3^m, M = √(Θ|p|² + |q|²).

The proof:

• Part C (coupled_levelEnergy) supplies the measurable representatives w₁ ≈ v − ½p·x, w₂ ≈ −v* + ½p·x and, for the negated problem, w₁' ≈ −(v − ½p·x), w₂' ≈ −(−v* + ½p·x), together with the level-energy estimate in the De Giorgi core's shape.
• exists_two_function_median produces a single median m.
• deGiorgi_one_sided_core is applied four times — to (w₁,w₂), (w₂,w₁) (upper tails, median m) and (w₁',w₂'), (w₂',w₁') (lower tails, median −m) — after transporting the core from axisCube to openCubeSet through the set identity openCubeSet (originCube d m) = axisCube (fun _ => −½·3^m) (3^m).

theorem HCPolySupport.openCubeSet_originCube_eq_axisCube {d : ℕ} (m : ℤ) : openCubeSet (originCube d m) = axisCube (fun (x : Fin d) => -(1 / 2) * 3 ^ m) (3 ^ m)

The centered open triadic cube is the axis cube with corner −½·3^m and side 3^m.

theorem HCPolySupport.coupled_stampacchia_uniform {d : ℕ} (hd : 3 ≤ d) : ∃ (Cd : ℝ), 0 ≤ Cd ∧ ∀ {m : ℤ} {Θ : ℝ} {a : CoeffField d}, IsEllipticFieldOn 1 Θ (cubeSet (originCube d m)) a → ∀ {p q : Vec d} {v vstar : H1Function (openCubeSet (originCube d m))}, CoupledWeakForm a (openCubeSet (originCube d m)) q v vstar → (MemH10 (openCubeSet (originCube d m)) fun (x : Vec d) => v.toFun x + vstar.toFun x - vecDot p x) → ∃ (c : ℝ), (∀ᵐ (x : Vec d) ∂volumeMeasureOn (openCubeSet (originCube d m)), |v.toFun x - 1 / 2 * vecDot p x - c| ≤ Cd * 3 ^ m * √(Θ * vecNormSq p + vecNormSq q)) ∧ ∀ᵐ (x : Vec d) ∂volumeMeasureOn (openCubeSet (originCube d m)), |vstar.toFun x - 1 / 2 * vecDot p x + c| ≤ Cd * 3 ^ m * √(Θ * vecNormSq p + vecNormSq q)

Uniform coupled Stampacchia estimate (Prop 3.3, constant-outside form).

Identical to coupled_stampacchia but with the dimensional constant Cd quantified outside all field data. The De Giorgi core's constant is already uniform (deGiorgi_one_sided_core has the shape ∃ Cd, ∀ …), so we obtain it once at the top and then quantify over the coupled weak-form data. The weaker coupled_stampacchia interface specializes this theorem. Consumed by the uniform per-core energy bound.

theorem HCPolySupport.coupled_stampacchia {d : ℕ} (hd : 3 ≤ d) {m : ℤ} {Θ : ℝ} {a : CoeffField d} (hEll : IsEllipticFieldOn 1 Θ (cubeSet (originCube d m)) a) {p q : Vec d} {v vstar : H1Function (openCubeSet (originCube d m))} (hCWF : CoupledWeakForm a (openCubeSet (originCube d m)) q v vstar) (htrace : MemH10 (openCubeSet (originCube d m)) fun (x : Vec d) => v.toFun x + vstar.toFun x - vecDot p x) : ∃ (Cd : ℝ) (c : ℝ), 0 ≤ Cd ∧ (∀ᵐ (x : Vec d) ∂volumeMeasureOn (openCubeSet (originCube d m)), |v.toFun x - 1 / 2 * vecDot p x - c| ≤ Cd * 3 ^ m * √(Θ * vecNormSq p + vecNormSq q)) ∧ ∀ᵐ (x : Vec d) ∂volumeMeasureOn (openCubeSet (originCube d m)), |vstar.toFun x - 1 / 2 * vecDot p x + c| ≤ Cd * 3 ^ m * √(Θ * vecNormSq p + vecNormSq q)

Coupled Stampacchia estimate (Prop 3.3).

Given hEll and the coupled weak form + shared trace (the consumed conjuncts of the representation package), there is a dimensional constant Cd ≥ 0 and a level c with, almost everywhere on U = openCubeSet (originCube d m), |v.toFun x − ½ p·x − c| ≤ Cd · 3^m · √(Θ|p|² + |q|²) and the mirror bound for v*.