Representation

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

Coupled representation (Proposition 3.1, existence direction)

Formalization of the EXISTENCE direction of p.coupled.representation (the high-moment paper (Armstrong–Kuusi–Loher, to appear), §3.1) for the pair constructed from the block minimizer, on the centered open triadic cube U = openCubeSet (originCube d m).

The converse (weak solution ⟹ minimizer) and uniqueness-mod-constants are out of scope.

The weak-form predicate CoupledWeakForm (G0) and all algebraic scaffolding live in Coupled/WeakForm.lean. This file assembles the existence package G1: exists_coupledRepresentation.

Vectors are Vec d = Fin d → ℝ; no EuclideanSpace.

Weak-gradient uniqueness under a.e.-equal values

Solenoidality of the constructed field h = a∇v + aᵀ∇v*

Mean-zero of H¹₀ gradients paired with a constant

The weak form of the constructed pair

G1 — the coupled representation existence package

theorem HCPolySupport.exists_coupledRepresentation {d : ℕ} [NeZero d] {m : ℤ} {Θ : ℝ} {a : CoeffField d} (hEll : IsEllipticFieldOn 1 Θ (cubeSet (originCube d m)) a) (P : BlockVec d) : ∃ (Z : BlockState d) (v : H1Function (openCubeSet (originCube d m))) (vstar : H1Function (openCubeSet (originCube d m))), IsBlockMuAdmissible (openCubeSet (originCube d m)) P Z ∧ Mu (openCubeSet (originCube d m)) P a = blockEnergyAverage (openCubeSet (originCube d m)) a Z ∧ BlockResponseSpace a (openCubeSet (originCube d m)) Z ∧ (MemH10 (openCubeSet (originCube d m)) fun (x : Vec d) => v.toFun x + vstar.toFun x - vecDot P.1 x) ∧ (Z.potential =ᵐ[volumeMeasureOn (openCubeSet (originCube d m))] fun (x : Vec d) => v.grad x + vstar.grad x) ∧ (Z.flux =ᵐ[volumeMeasureOn (openCubeSet (originCube d m))] fun (x : Vec d) => matVecMul (a x) (v.grad x) - matVecMul (matTranspose (a x)) (vstar.grad x)) ∧ CoupledWeakForm a (openCubeSet (originCube d m)) P.2 v vstar ∧ (fun (x : Vec d) => blockVecDot (Z.eval x) (blockMatVecMul (blockCoeffField a x) (Z.eval x))) =ᵐ[volumeMeasureOn (openCubeSet (originCube d m))] fun (x : Vec d) => 2 * vecDot (v.grad x) (matVecMul (symmPart (a x)) (v.grad x)) + 2 * vecDot (vstar.grad x) (matVecMul (symmPart (a x)) (vstar.grad x))

G1. Existence direction of the coupled representation (p.coupled.representation) on the centered open triadic cube.

For P = (p, q) there exist the block minimizer Z (transferred to the open cube) and H¹ functions v, v* such that:

• (i) Z is admissible for P, energy-realizing, and in the block response space;
• (ii) trace: v + v* − p·x ∈ H¹₀(U);
• (iii) gradient dictionary a.e.: Z.potential = ∇v + ∇v* and Z.flux = a∇v − aᵗ∇v*;
• (iv) the weak form CoupledWeakForm;
• (v) energy identity a.e.: Z·𝐁 Z = 2∇v·s∇v + 2∇v*·s∇v*.