FullBlockNormBounds

Ported from scottnarmstrong/Superdiffusion at 7f20476385d4af418f110303085ad0740c9eba46. Module imports, support namespace and local option directives adapted for Lean Pool.

Four-block domination of the full Euclidean block operator norm

The variance carriers of Section 3.5 are stated with the Euclidean operator norm of a 2d × 2d matrix over BlockCoord d = Fin d ⊕ Fin d (‖Matrix.toEuclidean (toFullBlockMat ...)‖), while the block moment inputs available for them are stated with the d × d norm Ch02.matrixOperatorNorm of one of the four blocks. This module supplies that direction of the dictionary.

What is proved

1. norm_toEuclideanCLM_le_sum_matrixOperatorNorm_blocks: for every X: FullBlockMat d, ‖toEuclidean X‖ ≤ ‖UL‖ + ‖UR‖ + ‖LL‖ + ‖LR‖, the summands being the Ch02.matrixOperatorNorm of the four d × d blocks ofFullBlockMat X. No symmetry, definiteness or nondegeneracy hypothesis is used, and the constant is absolute.
2. norm_toEuclideanCLM_sq_le_four_mul_sum_sq_matrixOperatorNorm_blocks: the squared corollary with the absolute constant 4, `‖toEuclidean X‖² ≤ 4 (‖UL‖² + ‖UR‖² + ‖LL‖²
   • ‖LR‖²)`.
3. The two BlockMat-carrier restatements (..._toFullBlockMat_...), the shape in which the block carriers of this directory present their matrices.
4. norm_toEuclideanCLM_diagonal_mul_mul_diagonal_le: conjugating by the two-scalar block gauge diag(s 𝟙, t 𝟙) weights the four block norms by s², |st|, |st|, t².

The squared form is the one an integrability consumer wants: integrability of the full squared operator norm follows from a second moment for each of the four block norms separately. Applied to starredFluctuationMatrix B a it dominates starredFluctuationOperatorNormSq B a with no rewriting at all, that carrier being literally ‖toEuclidean (starredFluctuationMatrix ...)‖².

What is not proved here

The instance of item 4 at the manuscript's own gauge is not taken: it needs the identification of CFC.sqrt (Ch02.constantFullBlockMatrix (Observable.isotropicComparatorMatrix σ)) with Matrix.diagonal (Ch05.Section56.scalarFullBlockSqrtDiag σ σ) -- available as the private cfcSqrt_isotropicComparator_eq_diagonal (VarianceCarrierSeam.lean, second copy at VarianceClosure.lean; a four-line consequence of the public Ch05.Section57.constantFullBlockMatrixSqrt_scalarMatrix_eq_scalarFullBlockSqrt) -- plus the block readings of the reflected difference, and taking it here would import the whole VarianceBridge closure into a pure matrix module. A consumer holding that closure reaches the manuscript weights σ, 1, 1, σ⁻¹ from item 4 at s = √σ, t = (√σ)⁻¹ after Real.sq_sqrt and mul_inv_cancel₀ at σ > 0; the squared gauged form the M7 consumer wants is a six-line re-derivation from item 5 plus pow_le_pow_left₀ (the four-square split as in the squared corollary).

Method

X acts on EuclideanSpace ℝ (BlockCoord d); splitting the argument into its two halves u = x ∘ Sum.inl, v = x ∘ Sum.inr and using (X *ᵥ x) = Sum.elim (UL *ᵥ u + UR *ᵥ v) (LL *ᵥ u + LR *ᵥ v) gives the bound from ContinuousLinearMap.opNorm_le_bound, because the Euclidean norm of a Sum.elim is below the sum of the two halves' norms and each half of x has norm at most ‖x‖. The gauge statement then needs only the four entrywise readings of diag · X · diag and absolute homogeneity of the d × d norm.

Two Euclidean facts about BlockCoord-indexed vectors

The four-block bound

theorem Algsuperdiff.Section3.Provider.Homogenization.norm_toEuclideanCLM_le_sum_matrixOperatorNorm_blocks {d : ℕ} (X : HCPolySupport.FullBlockMat d) : ‖Matrix.toEuclideanCLM X‖ ≤ HCPolySupport.Book.Ch02.matrixOperatorNorm (HCPolySupport.ofFullBlockMat X).upperLeft + HCPolySupport.Book.Ch02.matrixOperatorNorm (HCPolySupport.ofFullBlockMat X).upperRight + HCPolySupport.Book.Ch02.matrixOperatorNorm (HCPolySupport.ofFullBlockMat X).lowerLeft + HCPolySupport.Book.Ch02.matrixOperatorNorm (HCPolySupport.ofFullBlockMat X).lowerRight

The full block operator norm is below the sum of its four block operator norms. For every 2d × 2d real matrix X over BlockCoord d, with no symmetry or positivity hypothesis and with an absolute constant.

The two-scalar block gauge

theorem Algsuperdiff.Section3.Provider.Homogenization.norm_toEuclideanCLM_diagonal_mul_mul_diagonal_le {d : ℕ} (s t : ℝ) (X : HCPolySupport.FullBlockMat d) : ‖Matrix.toEuclideanCLM (Matrix.diagonal (Sum.elim (fun (x : Fin d) => s) fun (x : Fin d) => t) * X * Matrix.diagonal (Sum.elim (fun (x : Fin d) => s) fun (x : Fin d) => t))‖ ≤ s ^ 2 * HCPolySupport.Book.Ch02.matrixOperatorNorm (HCPolySupport.ofFullBlockMat X).upperLeft + |s * t| * HCPolySupport.Book.Ch02.matrixOperatorNorm (HCPolySupport.ofFullBlockMat X).upperRight + |s * t| * HCPolySupport.Book.Ch02.matrixOperatorNorm (HCPolySupport.ofFullBlockMat X).lowerLeft + t ^ 2 * HCPolySupport.Book.Ch02.matrixOperatorNorm (HCPolySupport.ofFullBlockMat X).lowerRight

Conjugation by the two-scalar block gauge diag(s 𝟙, t 𝟙) weights the four block norms by s², |st|, |st|, t². This is the gauge weighting of the manuscript's 𝐁^{1/2} · 𝐁^{1/2} conjugation at an isotropic comparator 𝐁 = 𝐁(σ), whose CFC.sqrt is exactly the diagonal matrix with √σ on the first block coordinates and (√σ)⁻¹ on the second: taking s = √σ and t = (√σ)⁻¹ turns the four weights into σ, 1, 1, σ⁻¹, the asymmetry printed in the manuscript's variance display.