Coarse-graining support: Support.Book.Ch05.Theorems.Section54.VarianceBoundGoodScale.FiniteNet

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

Finite-dimensional probes for full-block matrices

This file starts the deterministic finite-dimensional upgrade used in the variance bound. The eventual argument controls the Euclidean operator norm of a symmetric full-block matrix by finitely many quadratic probes.

def HCPolySupport.Book.Ch05.Section54.VarianceBoundGoodScale.fullBlockCoordinateProbe {d : ℕ} (α : BlockCoord d) : FullBlockVec d

Coordinate probe in the full-block space.

Equations

• HCPolySupport.Book.Ch05.Section54.VarianceBoundGoodScale.fullBlockCoordinateProbe α = Pi.single α 1

@[simp]

theorem HCPolySupport.Book.Ch05.Section54.VarianceBoundGoodScale.fullBlockQuadratic_coordinateProbe {d : ℕ} (M : FullBlockMat d) (α : BlockCoord d) : fullBlockQuadratic M (fullBlockCoordinateProbe α) = M α α

The quadratic form on a coordinate probe reads off a diagonal entry.

def HCPolySupport.Book.Ch05.Section54.VarianceBoundGoodScale.fullBlockPlusProbe {d : ℕ} (α β : BlockCoord d) : FullBlockVec d

The plus-pair probe used in the polarization step.

Equations

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

def HCPolySupport.Book.Ch05.Section54.VarianceBoundGoodScale.fullBlockMinusProbe {d : ℕ} (α β : BlockCoord d) : FullBlockVec d

The minus-pair probe used in the polarization step.

Equations

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

theorem HCPolySupport.Book.Ch05.Section54.VarianceBoundGoodScale.fullBlockQuadratic_plusProbe_of_ne {d : ℕ} {M : FullBlockMat d} (hM : Matrix.IsSymm M) {α β : BlockCoord d} (hαβ : α ≠ β) : fullBlockQuadratic M (fullBlockPlusProbe α β) = M α α + 2 * M α β + M β β

Off-diagonal plus-probe expansion for a symmetric full-block matrix.

theorem HCPolySupport.Book.Ch05.Section54.VarianceBoundGoodScale.fullBlockQuadratic_minusProbe_of_ne {d : ℕ} {M : FullBlockMat d} (hM : Matrix.IsSymm M) {α β : BlockCoord d} (hαβ : α ≠ β) : fullBlockQuadratic M (fullBlockMinusProbe α β) = M α α - 2 * M α β + M β β

Off-diagonal minus-probe expansion for a symmetric full-block matrix.

theorem HCPolySupport.Book.Ch05.Section54.VarianceBoundGoodScale.fullBlock_entry_eq_quarter_plus_sub_minus_of_ne {d : ℕ} {M : FullBlockMat d} (hM : Matrix.IsSymm M) {α β : BlockCoord d} (hαβ : α ≠ β) : M α β = 1 / 4 * (fullBlockQuadratic M (fullBlockPlusProbe α β) - fullBlockQuadratic M (fullBlockMinusProbe α β))

Polarization recovers an off-diagonal entry from the plus and minus quadratic probes.

noncomputable def HCPolySupport.Book.Ch05.Section54.VarianceBoundGoodScale.fullBlockProbeAbsSum {d : ℕ} (M : FullBlockMat d) : ℝ

A finite sum of coordinate and pair probes controlling all entries of a symmetric full-block matrix.

Equations

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

theorem HCPolySupport.Book.Ch05.Section54.VarianceBoundGoodScale.fullBlockProbeAbsSum_nonneg {d : ℕ} (M : FullBlockMat d) : 0 ≤ fullBlockProbeAbsSum M

theorem HCPolySupport.Book.Ch05.Section54.VarianceBoundGoodScale.fullBlock_operatorNorm_le_probeAbsSum {d : ℕ} {M : FullBlockMat d} (hM : Matrix.IsSymm M) : ‖Matrix.toEuclideanCLM M‖ ≤ ↑(Fintype.card (BlockCoord d)) * fullBlockProbeAbsSum M

The Euclidean operator norm of a symmetric full-block matrix is controlled by finitely many coordinate and pair quadratic probes.

theorem HCPolySupport.Book.Ch05.Section54.VarianceBoundGoodScale.fullBlock_operatorNorm_sq_le_probeAbsSum_sq {d : ℕ} {M : FullBlockMat d} (hM : Matrix.IsSymm M) : ‖Matrix.toEuclideanCLM M‖ ^ 2 ≤ (↑(Fintype.card (BlockCoord d)) * fullBlockProbeAbsSum M) ^ 2

Squared version of fullBlock_operatorNorm_le_probeAbsSum.

noncomputable def HCPolySupport.Book.Ch05.Section54.VarianceBoundGoodScale.fullBlockProbeSqBudget {d : ℕ} (M : FullBlockMat d) : ℝ

Dimension-weighted square budget for the finite coordinate and pair probes. This is intentionally generous; constants are harmless in the final dimension-dependent variance constant.

Equations

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

theorem HCPolySupport.Book.Ch05.Section54.VarianceBoundGoodScale.fullBlockProbeAbsSum_sq_le_probeSqBudget {d : ℕ} (M : FullBlockMat d) : fullBlockProbeAbsSum M ^ 2 ≤ fullBlockProbeSqBudget M

The finite-probe absolute sum is controlled by the square budget.

theorem HCPolySupport.Book.Ch05.Section54.VarianceBoundGoodScale.fullBlock_operatorNorm_sq_le_probeSqBudget {d : ℕ} {M : FullBlockMat d} (hM : Matrix.IsSymm M) : ‖Matrix.toEuclideanCLM M‖ ^ 2 ≤ ↑(Fintype.card (BlockCoord d)) ^ 2 * fullBlockProbeSqBudget M

Squared operator-norm control by the finite quadratic-probe square budget.

theorem HCPolySupport.Book.Ch05.Section54.VarianceBoundGoodScale.fullBlockNormalizedFluctuationOperatorNormSqAtScale_le_probeSqBudget_ae {d : ℕ} [NeZero d] {P : Ch04.RestrictionCoeffLaw d} (hP : Ch04.RestrictionLawCarrier P) (hStruct : Ch04.RestrictionStructuralLaw P) (center : ℤ) (Q : TriadicCube d) : (fun (a : RegCoeffField d) => Ch04.fullBlockNormalizedFluctuationOperatorNormSqAtScale hP hStruct center Q a) ≤ᵐ[P] fun (a : RegCoeffField d) => ↑(Fintype.card (BlockCoord d)) ^ 2 * fullBlockProbeSqBudget (normalizedFluctuationMatrix hP hStruct center (cubeSet Q) a.toFun)

Almost-sure finite-probe control of the Ch4 normalized full-block fluctuation observable on a cube.