Coarse-graining support:

Support.Book.Ch05.Theorems.Section54.VarianceBoundGoodScale.NormalizedBlocks

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

Normalized full-block fluctuation wrappers

This file records the Section 5.4-facing consequences of the public Ch4 and Section 5.2 APIs for the normalized full-block fluctuation observable appearing in the variance bound at a good scale.

def HCPolySupport.Book.Ch05.Section54.VarianceBoundGoodScale.fullBlockQuadratic {d : ℕ} (M : FullBlockMat d) (x : FullBlockVec d) : ℝ

The quadratic form associated with a full-block matrix.

Equations

• HCPolySupport.Book.Ch05.Section54.VarianceBoundGoodScale.fullBlockQuadratic M x = x ⬝ᵥ Matrix.mulVec M x

theorem HCPolySupport.Book.Ch05.Section54.VarianceBoundGoodScale.fullBlockQuadratic_one {d : ℕ} (q : FullBlockVec d) : fullBlockQuadratic 1 q = q ⬝ᵥ q

Quadratic form of the identity full-block matrix.

theorem HCPolySupport.Book.Ch05.Section54.VarianceBoundGoodScale.dotProduct_self_nonneg {d : ℕ} (q : FullBlockVec d) : 0 ≤ q ⬝ᵥ q

The Euclidean dot product of a full-block vector with itself is nonnegative.

theorem HCPolySupport.Book.Ch05.Section54.VarianceBoundGoodScale.fullBlockQuadratic_abs_sq_le_operatorNorm_sq_mul_dotProduct_sq {d : ℕ} (M : FullBlockMat d) (q : FullBlockVec d) : |fullBlockQuadratic M q| ^ 2 ≤ ‖Matrix.toEuclideanCLM M‖ ^ 2 * (q ⬝ᵥ q) ^ 2

A scalar full-block quadratic probe is controlled by the squared Euclidean operator norm of the matrix.

theorem HCPolySupport.Book.Ch05.Section54.VarianceBoundGoodScale.fullBlockQuadratic_sub {d : ℕ} (M N : FullBlockMat d) (q : FullBlockVec d) : fullBlockQuadratic (M - N) q = fullBlockQuadratic M q - fullBlockQuadratic N q

Quadratic forms are linear in the matrix argument.

theorem HCPolySupport.Book.Ch05.Section54.VarianceBoundGoodScale.diagonalForm_eq_dotProduct {d : ℕ} (r : BlockCoord d → ℝ) (A : BlockMat d) (q : FullBlockVec d) : fullBlockQuadratic (Matrix.diagonal r * toFullBlockMat A * Matrix.diagonal r) q = blockVecDot (ofFullBlockVec ((Matrix.diagonal r).mulVec q)) (blockMatVecMul A (ofFullBlockVec ((Matrix.diagonal r).mulVec q)))

Diagonal normalization of a block quadratic form is the block quadratic form evaluated on the diagonally normalized vector.

theorem HCPolySupport.Book.Ch05.Section54.VarianceBoundGoodScale.fullBlockQuadratic_diagonal_le_mul_dotProduct {d : ℕ} {r : BlockCoord d → ℝ} {C : ℝ} (q : FullBlockVec d) (hr : ∀ (α : BlockCoord d), r α ≤ C) : fullBlockQuadratic (Matrix.diagonal r) q ≤ C * q ⬝ᵥ q

A diagonal full-block quadratic form is controlled above by the largest diagonal coefficient.

theorem HCPolySupport.Book.Ch05.Section54.VarianceBoundGoodScale.mul_dotProduct_le_fullBlockQuadratic_diagonal {d : ℕ} {r : BlockCoord d → ℝ} {C : ℝ} (q : FullBlockVec d) (hr : ∀ (α : BlockCoord d), C ≤ r α) : C * q ⬝ᵥ q ≤ fullBlockQuadratic (Matrix.diagonal r) q

A diagonal full-block quadratic form is controlled below by the smallest diagonal coefficient.

theorem HCPolySupport.Book.Ch05.Section54.VarianceBoundGoodScale.isSymm_diagonal_mul_fullBlockMat_mul_diagonal {d : ℕ} (r : BlockCoord d → ℝ) {M : FullBlockMat d} (hM : Matrix.IsSymm M) : (Matrix.diagonal r * M * Matrix.diagonal r).IsSymm

Symmetry is preserved by diagonal congruence of a full-block matrix.

theorem HCPolySupport.Book.Ch05.Section54.VarianceBoundGoodScale.normalizedScalarAnnealedBlockMatrix_eq_diagonal {d : ℕ} [NeZero d] {P : Ch04.RestrictionCoeffLaw d} (hP : Ch04.RestrictionLawCarrier P) (hStruct : Ch04.RestrictionStructuralLaw P) (center n : ℤ) : have b := hP.barSigmaAtScale hStruct center; have c := hP.barSigmaStarAtScale hStruct center; have bn := hP.barSigmaAtScale hStruct n; have cn := hP.barSigmaStarAtScale hStruct n; have D := Matrix.diagonal (Ch04.scalarFullBlockInvSqrtDiag b c); D * toFullBlockMat (Ch04.scalarAnnealedBlockMatrixAtScale hP hStruct n) * D = Matrix.diagonal fun (α : BlockCoord d) => match α with | Sum.inl val => (√b)⁻¹ * bn * (√b)⁻¹ | Sum.inr val => √c * cn⁻¹ * √c

Scalar annealed full-block matrices remain diagonal after scalar normalization.

theorem HCPolySupport.Book.Ch05.Section54.VarianceBoundGoodScale.normalizedScalarAnnealedBlockMatrix_self_eq_one {d : ℕ} [NeZero d] {P : Ch04.RestrictionCoeffLaw d} (hP : Ch04.RestrictionLawCarrier P) (hStruct : Ch04.RestrictionStructuralLaw P) (hP4 : QuantitativeCoarseGrainedEllipticity P) (m : ℕ) : have b := hP.barSigmaAtScale hStruct ↑m; have c := hP.barSigmaStarAtScale hStruct ↑m; have D := Matrix.diagonal (Ch04.scalarFullBlockInvSqrtDiag b c); D * toFullBlockMat (Ch04.scalarAnnealedBlockMatrixAtScale hP hStruct ↑m) * D = 1

At the center scale, scalar normalization turns the scalar annealed block into the identity.

theorem HCPolySupport.Book.Ch05.Section54.VarianceBoundGoodScale.annealedBlockMatrixAtScale_eq_scalarAnnealedBlockMatrixAtScale {d : ℕ} [NeZero d] {P : Ch04.RestrictionCoeffLaw d} (hP : Ch04.RestrictionLawCarrier P) (hStruct : Ch04.RestrictionStructuralLaw P) (n : ℤ) : Ch04.annealedBlockMatrixAtScale P n = Ch04.scalarAnnealedBlockMatrixAtScale hP hStruct n

Under the structural law, the annealed full block is exactly the scalar block diagonal used to normalize the manuscript fluctuation observable.

theorem HCPolySupport.Book.Ch05.Section54.VarianceBoundGoodScale.isSymmetricBlockMat_scalarAnnealedBlockMatrixAtScale {d : ℕ} [NeZero d] {P : Ch04.RestrictionCoeffLaw d} (hP : Ch04.RestrictionLawCarrier P) (hStruct : Ch04.RestrictionStructuralLaw P) (center : ℤ) : IsSymmetricBlockMat (Ch04.scalarAnnealedBlockMatrixAtScale hP hStruct center)

The scalar annealed block matrix is symmetric as a doubled block matrix.

theorem HCPolySupport.Book.Ch05.Section54.VarianceBoundGoodScale.normalizedAnnealedBlockMatrix_self_eq_one {d : ℕ} [NeZero d] {P : Ch04.RestrictionCoeffLaw d} (hP : Ch04.RestrictionLawCarrier P) (hStruct : Ch04.RestrictionStructuralLaw P) (hP4 : QuantitativeCoarseGrainedEllipticity P) (m : ℕ) : have b := hP.barSigmaAtScale hStruct ↑m; have c := hP.barSigmaStarAtScale hStruct ↑m; have D := Matrix.diagonal (Ch04.scalarFullBlockInvSqrtDiag b c); D * toFullBlockMat (Ch04.annealedBlockMatrixAtScale P ↑m) * D = 1

At the center scale, scalar normalization turns the annealed block into the identity.

theorem HCPolySupport.Book.Ch05.Section54.VarianceBoundGoodScale.fluctuationNormSquare_nonneg {d : ℕ} [NeZero d] {P : Ch04.RestrictionCoeffLaw d} (hP : Ch04.RestrictionLawCarrier P) (hStruct : Ch04.RestrictionStructuralLaw P) (center : ℤ) (R : TriadicCube d) (a : RegCoeffField d) : 0 ≤ Ch04.fullBlockNormalizedFluctuationOperatorNormSqAtScale hP hStruct center R a

The normalized full-block fluctuation observable is nonnegative.

noncomputable def HCPolySupport.Book.Ch05.Section54.VarianceBoundGoodScale.normalizedFluctuationMatrix {d : ℕ} [NeZero d] {P : Ch04.RestrictionCoeffLaw d} (hP : Ch04.RestrictionLawCarrier P) (hStruct : Ch04.RestrictionStructuralLaw P) (center : ℤ) (U : Set (Vec d)) (a : CoeffField d) : FullBlockMat d

The normalized full-block fluctuation matrix whose Euclidean operator norm is squared in the manuscript observable.

Equations

• One or more equations did not get rendered due to their size.

theorem HCPolySupport.Book.Ch05.Section54.VarianceBoundGoodScale.normalizedFluctuation_isSymm {d : ℕ} [NeZero d] {P : Ch04.RestrictionCoeffLaw d} (hP : Ch04.RestrictionLawCarrier P) (hStruct : Ch04.RestrictionStructuralLaw P) (center : ℤ) {U : Set (Vec d)} {a : CoeffField d} (hA : IsSymmetricBlockMat (coarseBlockMatrix U a)) : Matrix.IsSymm (normalizedFluctuationMatrix hP hStruct center U a)

The normalized full-block fluctuation matrix is symmetric whenever the underlying coarse block matrix is symmetric.

theorem HCPolySupport.Book.Ch05.Section54.VarianceBoundGoodScale.isSymmetricBlockMat_coarseBlockMatrix_cubeSet_ae {d : ℕ} [NeZero d] {P : Ch04.RestrictionCoeffLaw d} (hP : Ch04.RestrictionLawCarrier P) (Q : TriadicCube d) : ∀ᵐ (a : RegCoeffField d) ∂P, IsSymmetricBlockMat (coarseBlockMatrix (cubeSet Q) a.toFun)

On cube sets, the public coarse block matrix is symmetric almost surely.

theorem HCPolySupport.Book.Ch05.Section54.VarianceBoundGoodScale.fullBlockNormalizedFluctuationMatrix_isSymm_ae {d : ℕ} [NeZero d] {P : Ch04.RestrictionCoeffLaw d} (hP : Ch04.RestrictionLawCarrier P) (hStruct : Ch04.RestrictionStructuralLaw P) (center : ℤ) (Q : TriadicCube d) : ∀ᵐ (a : RegCoeffField d) ∂P, Matrix.IsSymm (normalizedFluctuationMatrix hP hStruct center (cubeSet Q) a.toFun)

On cube sets, the normalized full-block fluctuation matrix is symmetric almost surely.

theorem HCPolySupport.Book.Ch05.Section54.VarianceBoundGoodScale.fullBlockFluctuationNormSquare_eq_matrixNormSquare {d : ℕ} [NeZero d] {P : Ch04.RestrictionCoeffLaw d} (hP : Ch04.RestrictionLawCarrier P) (hStruct : Ch04.RestrictionStructuralLaw P) (center : ℤ) (U : Set (Vec d)) (a : CoeffField d) : Ch04.fullBlockNormalizedFluctuationOperatorNormSq hP hStruct center U a = ‖Matrix.toEuclideanCLM (normalizedFluctuationMatrix hP hStruct center U a)‖ ^ 2

The Ch4 normalized fluctuation observable is the squared operator norm of fullBlockNormalizedFluctuationMatrix.

noncomputable def HCPolySupport.Book.Ch05.Section54.VarianceBoundGoodScale.normalizedQuadraticObservable {d : ℕ} [NeZero d] {P : Ch04.RestrictionCoeffLaw d} (hP : Ch04.RestrictionLawCarrier P) (hStruct : Ch04.RestrictionStructuralLaw P) (center : ℤ) (q : FullBlockVec d) (U : Set (Vec d)) (a : CoeffField d) : ℝ

Normalized quadratic probe observable used before the finite-probe upgrade in the good-scale variance bound. This is linear in the coarse block matrix; centering is supplied by Ch04.restrictionCenteredOriginObservable.

Equations

• One or more equations did not get rendered due to their size.

noncomputable def HCPolySupport.Book.Ch05.Section54.VarianceBoundGoodScale.fullBlockNormalizedQuadraticObservableR {d : ℕ} [NeZero d] {P : Ch04.RestrictionCoeffLaw d} (hP : Ch04.RestrictionLawCarrier P) (hStruct : Ch04.RestrictionStructuralLaw P) (center : ℤ) (q : FullBlockVec d) (U : Set (Vec d)) (a : RegCoeffField d) : ℝ

Carrier realization of the normalized quadratic probe observable, applied to the honest sample of a carrier field. This is the form consumed by the Ch4 descendant-average machinery.

Equations

• One or more equations did not get rendered due to their size.

theorem HCPolySupport.Book.Ch05.Section54.VarianceBoundGoodScale.normalizedQuadraticIdentity {d : ℕ} [NeZero d] {P : Ch04.RestrictionCoeffLaw d} (hP : Ch04.RestrictionLawCarrier P) (hStruct : Ch04.RestrictionStructuralLaw P) (hP4 : QuantitativeCoarseGrainedEllipticity P) (m : ℕ) (q : FullBlockVec d) (U : Set (Vec d)) (a : CoeffField d) : normalizedQuadraticObservable hP hStruct (↑m) q U a - q ⬝ᵥ q = fullBlockQuadratic (normalizedFluctuationMatrix hP hStruct (↑m) U a) q

Centering a normalized quadratic probe at the center-scale annealed value is the quadratic form of the normalized fluctuation matrix.

theorem HCPolySupport.Book.Ch05.Section54.VarianceBoundGoodScale.fullBlockNormalizedQuadraticObservable_nonneg_ae {d : ℕ} [NeZero d] {P : Ch04.RestrictionCoeffLaw d} (hP : Ch04.RestrictionLawCarrier P) (hStruct : Ch04.RestrictionStructuralLaw P) (center : ℤ) (q : FullBlockVec d) (Q : TriadicCube d) : ∀ᵐ (a : RegCoeffField d) ∂P, 0 ≤ normalizedQuadraticObservable hP hStruct center q (cubeSet Q) a.toFun

Normalized quadratic probes are nonnegative on cube sets, almost surely.

theorem HCPolySupport.Book.Ch05.Section54.VarianceBoundGoodScale.fullBlockNormalizedQuadraticObservable_translation_covariant {d : ℕ} [NeZero d] {P : Ch04.RestrictionCoeffLaw d} (hP : Ch04.RestrictionLawCarrier P) (hStruct : Ch04.RestrictionStructuralLaw P) (center : ℤ) (q : FullBlockVec d) : IsTranslationCovariant fun (U : Set (Vec d)) (a : CoeffField d) => normalizedQuadraticObservable hP hStruct center q U a

Translation covariance of the normalized quadratic probe observable.

theorem HCPolySupport.Book.Ch05.Section54.VarianceBoundGoodScale.integrable_fullBlockFluctuationNormSquare_of_P4_atScale {d : ℕ} [NeZero d] {P : Ch04.RestrictionCoeffLaw d} (hP : Ch04.RestrictionLawCarrier P) (hStruct : Ch04.RestrictionStructuralLaw P) (hP4 : QuantitativeCoarseGrainedEllipticity P) (center : ℤ) (n : ℕ) : MeasureTheory.Integrable (Ch04.fullBlockNormalizedFluctuationOperatorNormSqAtScale hP hStruct center (originCube d ↑n)) P

(P4) supplies integrability of the normalized full-block fluctuation on origin cubes.

theorem HCPolySupport.Book.Ch05.Section54.VarianceBoundGoodScale.integrable_origin_fullBlockNormalizedFluctuationOperatorNormSqAtScale_from_P4_of_nonneg {d : ℕ} [NeZero d] {P : Ch04.RestrictionCoeffLaw d} (hP : Ch04.RestrictionLawCarrier P) (hStruct : Ch04.RestrictionStructuralLaw P) (hP4 : QuantitativeCoarseGrainedEllipticity P) (center n : ℤ) (hn : 0 ≤ n) : MeasureTheory.Integrable (Ch04.fullBlockNormalizedFluctuationOperatorNormSqAtScale hP hStruct center (originCube d n)) P

Integer-scale version of the origin-cube integrability consequence of (P4).

theorem HCPolySupport.Book.Ch05.Section54.VarianceBoundGoodScale.integrable_fluctuationNormSquare {d : ℕ} [NeZero d] {P : Ch04.RestrictionCoeffLaw d} (hP : Ch04.RestrictionLawCarrier P) (hStruct : Ch04.RestrictionStructuralLaw P) (hP4 : QuantitativeCoarseGrainedEllipticity P) (center : ℤ) (R : TriadicCube d) (hR_nonneg : 0 ≤ R.scale) : MeasureTheory.Integrable (Ch04.fullBlockNormalizedFluctuationOperatorNormSqAtScale hP hStruct center R) P

Under (P4) and stationarity, the normalized full-block fluctuation is integrable on every nonnegative-scale cube.

theorem HCPolySupport.Book.Ch05.Section54.VarianceBoundGoodScale.integral_fullBlockNormalizedFluctuationOperatorNormSqAtScale_eq_originCube_from_P4 {d : ℕ} [NeZero d] {P : Ch04.RestrictionCoeffLaw d} (hP : Ch04.RestrictionLawCarrier P) (hStruct : Ch04.RestrictionStructuralLaw P) (hP4 : QuantitativeCoarseGrainedEllipticity P) (center : ℤ) (R : TriadicCube d) (hR_nonneg : 0 ≤ R.scale) : ∫ (a : RegCoeffField d), Ch04.fullBlockNormalizedFluctuationOperatorNormSqAtScale hP hStruct center R a ∂P = ∫ (a : RegCoeffField d), Ch04.fullBlockNormalizedFluctuationOperatorNormSqAtScale hP hStruct center (originCube d R.scale) a ∂P

Stationarity identifies the expectation on a nonnegative-scale cube with the corresponding origin-cube expectation, with integrability supplied by (P4).

theorem HCPolySupport.Book.Ch05.Section54.VarianceBoundGoodScale.integrable_fullBlockNormalizedFluctuationOperatorNormSqAtScale_of_mem_descendants_from_P4 {d : ℕ} [NeZero d] {P : Ch04.RestrictionCoeffLaw d} (hP : Ch04.RestrictionLawCarrier P) (hStruct : Ch04.RestrictionStructuralLaw P) (hP4 : QuantitativeCoarseGrainedEllipticity P) (center : ℤ) {n m : ℤ} (hn : 0 ≤ n) (hnm : n ≤ m) {R : TriadicCube d} (hR : R ∈ descendantsAtScale (originCube d m) n) : MeasureTheory.Integrable (Ch04.fullBlockNormalizedFluctuationOperatorNormSqAtScale hP hStruct center R) P

(P4) supplies the integrability hypothesis needed for descendant averages of the normalized full-block fluctuation observable.

theorem HCPolySupport.Book.Ch05.Section54.VarianceBoundGoodScale.integral_descendantMean_fullBlockFluctuationNormSq_eq_cube_from_P4 {d : ℕ} [NeZero d] {P : Ch04.RestrictionCoeffLaw d} (hP : Ch04.RestrictionLawCarrier P) (hStruct : Ch04.RestrictionStructuralLaw P) (hP4 : QuantitativeCoarseGrainedEllipticity P) (center : ℤ) {n m : ℤ} (hn : 0 ≤ n) (hnm : n ≤ m) : ∫ (a : RegCoeffField d), descendantsAverage (originCube d m) (m - n).toNat fun (R : TriadicCube d) => Ch04.fullBlockNormalizedFluctuationOperatorNormSqAtScale hP hStruct center R a ∂P = ∫ (a : RegCoeffField d), Ch04.fullBlockNormalizedFluctuationOperatorNormSqAtScale hP hStruct center (originCube d n) a ∂P

Expectation of a descendant average of normalized full-block fluctuations collapses to the corresponding origin-cube expectation under stationarity, with integrability supplied by (P4).