Coarse-graining support: Support.CoarseGraining.CoarseBounds.Sandwich

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

Coarse diagonal sandwich (items C1, C1′)

The coarse block matrix 𝐀(U; a) = coarseBlockMatrix U a on the half-open triadic cube U = cubeSet (originCube d m) is sandwiched between the two scalar-diagonal block matrices blockDiag (½•1) ((2Θ)⁻¹•1) and blockDiag ((2Θ)•1) (2•1) in the block Loewner order, for every coefficient field that is (1, Θ)-elliptic on U. This is Proposition 2.2's coarse ellipticity statement e.coarse.block.ellipticity in the high-moment paper (Armstrong–Kuusi–Loher, to appear).

• C1 upper — the constant competitor X ≡ P is Mu-admissible, and the pointwise A8 upper bound bfA ≤ blockDiag ((2Θ)•1) (2•1) gives Mu ≤ Θ|p|² + |q|².
• C1 lower — for any admissible X, the pointwise A8 lower bound blockDiag (½•1) ((2Θ)⁻¹•1) ≤ bfA, followed by componentwise Jensen (vecNormSq_volumeAverage_le_volumeAverage_vecNormSq) and the mean-zero identities ⨍ X.potential = p, ⨍ X.flux = q (from the a.e. zero-trace averages IsPotentialZeroTraceOn.integral_eq_zero_cubeSet_originCube and IsSolenoidalZeroNormalTraceOn.integral_eq_zero_cubeSet_originCube), gives ¼|p|² + (4Θ)⁻¹|q|² ≤ Mu.

Everything is rewritten through mu_eq_half_coarseBlockMatrix_cube (Mu = ½ P·𝐀 P). Vectors are Vec d = Fin d → ℝ; no EuclideanSpace.

Shared cube data

The pointwise A8 bounds on the block energy density

C1 as Mu bounds

theorem HCPolySupport.diag_lower_le_mu_cube {d : ℕ} {m : ℤ} {Θ : ℝ} {a : CoeffField d} [NeZero d] (hEll : IsEllipticFieldOn 1 Θ (cubeSet (originCube d m)) a) (P : BlockVec d) : 1 / 4 * vecNormSq P.1 + (4 * Θ)⁻¹ * vecNormSq P.2 ≤ Mu (cubeSet (originCube d m)) P a

C1 lower as a Mu bound: ¼|p|² + (4Θ)⁻¹|q|² ≤ Mu (U; P, a).

theorem HCPolySupport.mu_le_diag_upper_cube {d : ℕ} {m : ℤ} {Θ : ℝ} {a : CoeffField d} (hEll : IsEllipticFieldOn 1 Θ (cubeSet (originCube d m)) a) (P : BlockVec d) : Mu (cubeSet (originCube d m)) P a ≤ Θ * vecNormSq P.1 + vecNormSq P.2

C1 upper as a Mu bound: Mu (U; P, a) ≤ Θ|p|² + |q|².

C1 — the block Loewner sandwich

theorem HCPolySupport.blockDiag_blockMatLoewnerLE_coarseBlockMatrix_cube {d : ℕ} {m : ℤ} {Θ : ℝ} {a : CoeffField d} [NeZero d] (hEll : IsEllipticFieldOn 1 Θ (cubeSet (originCube d m)) a) : BlockMatLoewnerLE (Book.Ch02.blockDiag ((1 / 2) • 1) ((2 * Θ)⁻¹ • 1)) (coarseBlockMatrix (cubeSet (originCube d m)) a)

C1 (lower). blockDiag (½•1) ((2Θ)⁻¹•1) ≤ 𝐀(U; a) in the block Loewner order, on the half-open triadic cube.

theorem HCPolySupport.coarseBlockMatrix_blockMatLoewnerLE_blockDiag_cube {d : ℕ} {m : ℤ} {Θ : ℝ} {a : CoeffField d} [NeZero d] (hEll : IsEllipticFieldOn 1 Θ (cubeSet (originCube d m)) a) : BlockMatLoewnerLE (coarseBlockMatrix (cubeSet (originCube d m)) a) (Book.Ch02.blockDiag ((2 * Θ) • 1) (2 • 1))

C1 (upper). 𝐀(U; a) ≤ blockDiag ((2Θ)•1) (2•1) in the block Loewner order, on the half-open triadic cube.

C1′ — scalar corollaries

theorem HCPolySupport.zero_le_blockVecDot_coarseBlockMatrix_cube {d : ℕ} {m : ℤ} {Θ : ℝ} {a : CoeffField d} [NeZero d] (hEll : IsEllipticFieldOn 1 Θ (cubeSet (originCube d m)) a) (P : BlockVec d) : 0 ≤ blockVecDot P (blockMatVecMul (coarseBlockMatrix (cubeSet (originCube d m)) a) P)

C1′ (nonnegativity). 0 ≤ P·𝐀(U; a) P.

theorem HCPolySupport.blockVecDot_coarseBlockMatrix_cube_le {d : ℕ} {m : ℤ} {Θ : ℝ} {a : CoeffField d} [NeZero d] (hEll : IsEllipticFieldOn 1 Θ (cubeSet (originCube d m)) a) (P : BlockVec d) : blockVecDot P (blockMatVecMul (coarseBlockMatrix (cubeSet (originCube d m)) a) P) ≤ 2 * (Θ * vecNormSq P.1 + vecNormSq P.2)

C1′ (upper). P·𝐀(U; a) P ≤ 2 (Θ|p|² + |q|²).