Coarse-graining support: Support.CoarseGraining.CubeMinimizer

Imported from the Apache-2.0 CoarseGraining development at commit c7ddd76c08ade64fed1b8d2ca51be14dfee8deb4.

Cube minimizer well-posedness (Proposition 2.2, part)

Formalization of the coarse block minimizer well-posedness on a triadic cube originCube d m against the coarse-graining surface of this development.

The half-open observable and the open-cube variational problem coincide, since Mu (cubeSet Q) P a = Mu (openCubeSet Q) P a holds unconditionally (Mu_cubeSet_eq_openCubeSet_of_triadicCube). We therefore work against the pointwise hypothesis IsEllipticFieldOn 1 Θ (cubeSet (originCube d m)) a and transport every open-cube recovery fact to the half-open cube.

Public deliverables (all on U = cubeSet (originCube d m)):

• exists_cubeBlockMinimizer — a Mu-admissible minimizer Z_P realizing the energy and lying in the block response space (item (a); the response-space conjunct carries the Euler orthogonality (c));
• cubeBlockMinimizer_euler_orthogonality — the Euler orthogonality integral (item (c));
• cubeBlockMinimizer_ae_unique — a.e. uniqueness of the minimizer (item (b));
• hasQuadraticMu_cube — quadraticity of Mu (item (d));
• mu_eq_half_coarseBlockMatrix_cube — Mu = ½ P·A P (item (e));
• isBlockTestOn_sub_of_isBlockMuAdmissible — the componentwise difference of two Mu-admissible states for the same P is a block test state (load-bearing for the Y = Z_tilde − Z composition used downstream).

All fields are Vec d = Fin d → ℝ valued; no EuclideanSpace.

Difference of two admissible states is a block test state

theorem HCPolySupport.isBlockTestOn_sub_of_isBlockMuAdmissible {d : ℕ} {U : Set (Vec d)} {P : BlockVec d} {X X' : BlockState d} (hX : IsBlockMuAdmissible U P X) (hX' : IsBlockMuAdmissible U P X') : IsBlockTestOn U { potential := fun (x : Vec d) => X.potential x - X'.potential x, flux := fun (x : Vec d) => X.flux x - X'.flux x }

The componentwise difference X − X' of two Mu-admissible block states for the same parameter P is a block test state: its potential part is zero-trace and its flux part is zero-normal-trace. This is the algebraic closure the downstream stability lemmas need in order to feed Y = Z_tilde − Z into the Euler orthogonality of a minimizer.

Open-cube recovery core

Public deliverables on the half-open cube

theorem HCPolySupport.exists_cubeBlockMinimizer {d : ℕ} [NeZero d] {m : ℤ} {Θ : ℝ} {a : CoeffField d} (hEll : IsEllipticFieldOn 1 Θ (cubeSet (originCube d m)) a) (P : BlockVec d) : ∃ (Z : BlockState d), IsBlockMuAdmissible (cubeSet (originCube d m)) P Z ∧ Mu (cubeSet (originCube d m)) P a = blockEnergyAverage (cubeSet (originCube d m)) a Z ∧ BlockResponseSpace a (cubeSet (originCube d m)) Z

(a) Existence of a Mu-admissible minimizer Z_P on the half-open triadic cube, realizing the energy and lying in the block response space. The BlockResponseSpace conjunct is exactly the Euler orthogonality (c).

theorem HCPolySupport.cubeBlockMinimizer_euler_orthogonality {d : ℕ} {m : ℤ} {a : CoeffField d} {Z : BlockState d} (hResp : BlockResponseSpace a (cubeSet (originCube d m)) Z) {Y : BlockState d} (hY : IsBlockTestOn (cubeSet (originCube d m)) Y) : ∫ (x : Vec d) in cubeSet (originCube d m), blockVecDot (Y.eval x) (blockMatVecMul (blockCoeffField a x) (Z.eval x)) = 0

(c) Euler orthogonality of the coarse block minimizer: for every admissible block test perturbation Y, the pairing of Y against 𝐁 Z = blockCoeffField a · Z integrates to zero.

theorem HCPolySupport.cubeBlockMinimizer_euler_orthogonality_sub {d : ℕ} {m : ℤ} {a : CoeffField d} {P : BlockVec d} {Z X X' : BlockState d} (hResp : BlockResponseSpace a (cubeSet (originCube d m)) Z) (hX : IsBlockMuAdmissible (cubeSet (originCube d m)) P X) (hX' : IsBlockMuAdmissible (cubeSet (originCube d m)) P X') : ∫ (x : Vec d) in cubeSet (originCube d m), blockVecDot (X.eval x - X'.eval x) (blockMatVecMul (blockCoeffField a x) (Z.eval x)) = 0

The Y = Z_tilde − Z instantiation of Euler orthogonality used downstream: the difference of two admissible states for the same P is a valid test perturbation, so it pairs to zero against 𝐁 Z for a minimizer Z.

theorem HCPolySupport.hasQuadraticMu_cube {d : ℕ} [NeZero d] {m : ℤ} {Θ : ℝ} {a : CoeffField d} (hEll : IsEllipticFieldOn 1 Θ (cubeSet (originCube d m)) a) : HasQuadraticMu (cubeSet (originCube d m)) a

(d) Quadraticity of Mu on the half-open triadic cube.

theorem HCPolySupport.mu_eq_half_coarseBlockMatrix_cube {d : ℕ} [NeZero d] {m : ℤ} {Θ : ℝ} {a : CoeffField d} (hEll : IsEllipticFieldOn 1 Θ (cubeSet (originCube d m)) a) (P : BlockVec d) : Mu (cubeSet (originCube d m)) P a = 1 / 2 * blockVecDot P (blockMatVecMul (coarseBlockMatrix (cubeSet (originCube d m)) a) P)

(e) The note-faithful quadratic representation Mu (U; P, a) = ½ P·𝐀(U; a) P on the half-open triadic cube.

Uniqueness

theorem HCPolySupport.cubeBlockMinimizer_ae_unique {d : ℕ} [NeZero d] {m : ℤ} {Θ : ℝ} {a : CoeffField d} (hEll : IsEllipticFieldOn 1 Θ (cubeSet (originCube d m)) a) {P : BlockVec d} {Z Z' : BlockState d} (hZ : IsBlockMuAdmissible (cubeSet (originCube d m)) P Z) (hZ' : IsBlockMuAdmissible (cubeSet (originCube d m)) P Z') (hZe : Mu (cubeSet (originCube d m)) P a = blockEnergyAverage (cubeSet (originCube d m)) a Z) (hZ'e : Mu (cubeSet (originCube d m)) P a = blockEnergyAverage (cubeSet (originCube d m)) a Z') : (fun (x : Vec d) => Z.eval x) =ᵐ[volumeMeasureOn (cubeSet (originCube d m))] fun (x : Vec d) => Z'.eval x

(b) A.e. uniqueness of the coarse block minimizer: any two Mu-admissible states that both realize the minimum energy for the same parameter P agree almost everywhere (as evaluations) on the half-open triadic cube.