Coarse-graining support: Support.Book.Ch05.Theorems.Section56.VarianceEstimateQuadratic.Basic

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

Section 5.6: variance triangle for normalized block fluctuations

This file records the part of Lemma l.variance.estimate.quadratic in which the manuscript variance is interpreted by the Section 5.4 squared Euclidean-operator-norm fluctuation observable.

noncomputable def HCPolySupport.Book.Ch05.Section56.descendantsAverageFullBlockMat {d : ℕ} (Q : TriadicCube d) (j : ℕ) (F : TriadicCube d → FullBlockMat d) : FullBlockMat d

Entrywise descendant average of full block matrices.

Equations

• HCPolySupport.Book.Ch05.Section56.descendantsAverageFullBlockMat Q j F α β = HCPolySupport.descendantsAverage Q j fun (R : HCPolySupport.TriadicCube d) => F R α β

noncomputable def HCPolySupport.Book.Ch05.Section56.descendantsAverageNormalizedFluctuationMatrix {d : ℕ} [NeZero d] {P : Ch04.RestrictionCoeffLaw d} (hP : Ch04.RestrictionLawCarrier P) (hStruct : Ch04.RestrictionStructuralLaw P) (center : ℤ) (Q : TriadicCube d) (j : ℕ) (a : RegCoeffField d) : FullBlockMat d

The normalized fluctuation matrix of the descendant-average coarse block.

Equations

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

noncomputable def HCPolySupport.Book.Ch05.Section56.descendantsAverageNormalizedFluctuationOperatorNormSq {d : ℕ} [NeZero d] {P : Ch04.RestrictionCoeffLaw d} (hP : Ch04.RestrictionLawCarrier P) (hStruct : Ch04.RestrictionStructuralLaw P) (center : ℤ) (Q : TriadicCube d) (j : ℕ) (a : RegCoeffField d) : ℝ

Squared operator norm of the normalized descendant-average fluctuation.

Equations

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

noncomputable def HCPolySupport.Book.Ch05.Section56.normalizedCoarseAverageErrorMatrix {d : ℕ} [NeZero d] {P : Ch04.RestrictionCoeffLaw d} (hP : Ch04.RestrictionLawCarrier P) (hStruct : Ch04.RestrictionStructuralLaw P) (center : ℤ) (Q : TriadicCube d) (j : ℕ) (a : RegCoeffField d) : FullBlockMat d

Normalized difference between the parent fluctuation and the descendant average fluctuation. This is the operator-norm error term before it is estimated by block J.

Equations

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

noncomputable def HCPolySupport.Book.Ch05.Section56.normalizedCoarseAveragePositiveErrorMatrix {d : ℕ} [NeZero d] {P : Ch04.RestrictionCoeffLaw d} (hP : Ch04.RestrictionLawCarrier P) (hStruct : Ch04.RestrictionStructuralLaw P) (center : ℤ) (Q : TriadicCube d) (j : ℕ) (a : RegCoeffField d) : FullBlockMat d

The positive coarse-average defect, with the sign used by block subadditivity. Its squared operator norm is the same as normalizedCoarseAverageErrorMatrix.

Equations

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

noncomputable def HCPolySupport.Book.Ch05.Section56.normalizedCoarseAverageErrorOperatorNormSq {d : ℕ} [NeZero d] {P : Ch04.RestrictionCoeffLaw d} (hP : Ch04.RestrictionLawCarrier P) (hStruct : Ch04.RestrictionStructuralLaw P) (center : ℤ) (Q : TriadicCube d) (j : ℕ) (a : RegCoeffField d) : ℝ

Squared operator norm of the normalized parent-minus-descendant-average error.

Equations

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

noncomputable def HCPolySupport.Book.Ch05.Section56.fullBlockFluctuationMatrixWithNormalizer {d : ℕ} [NeZero d] {P : Ch04.RestrictionCoeffLaw d} (hP : Ch04.RestrictionLawCarrier P) (hStruct : Ch04.RestrictionStructuralLaw P) (center : ℤ) (S : FullBlockMat d) (U : Set (Vec d)) (a : RegCoeffField d) : FullBlockMat d

Full-block fluctuation normalized by an arbitrary deterministic matrix. For the manuscript lemma, take S = B^{-1/2}; the congruence is written as Sᵀ M S, which agrees with B^{-1/2} M B^{-1/2} for the symmetric positive definite square root.

Equations

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

noncomputable def HCPolySupport.Book.Ch05.Section56.fullBlockFluctuationOperatorNormSqWithNormalizer {d : ℕ} [NeZero d] {P : Ch04.RestrictionCoeffLaw d} (hP : Ch04.RestrictionLawCarrier P) (hStruct : Ch04.RestrictionStructuralLaw P) (center : ℤ) (S : FullBlockMat d) (U : Set (Vec d)) (a : RegCoeffField d) : ℝ

Squared operator norm of the arbitrary-normalizer full-block fluctuation.

Equations

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

noncomputable def HCPolySupport.Book.Ch05.Section56.fullBlockFluctuationOperatorNormSqAtScaleWithNormalizer {d : ℕ} [NeZero d] {P : Ch04.RestrictionCoeffLaw d} (hP : Ch04.RestrictionLawCarrier P) (hStruct : Ch04.RestrictionStructuralLaw P) (center : ℤ) (S : FullBlockMat d) (Q : TriadicCube d) (a : RegCoeffField d) : ℝ

Arbitrary-normalizer full-block fluctuation on a triadic cube.

Equations

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

noncomputable def HCPolySupport.Book.Ch05.Section56.descendantsAverageFluctuationMatrixWithNormalizer {d : ℕ} [NeZero d] {P : Ch04.RestrictionCoeffLaw d} (hP : Ch04.RestrictionLawCarrier P) (hStruct : Ch04.RestrictionStructuralLaw P) (center : ℤ) (S : FullBlockMat d) (Q : TriadicCube d) (j : ℕ) (a : RegCoeffField d) : FullBlockMat d

Descendant average of arbitrary-normalizer full-block fluctuation matrices.

Equations

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

noncomputable def HCPolySupport.Book.Ch05.Section56.descendantsAverageFluctuationOperatorNormSqWithNormalizer {d : ℕ} [NeZero d] {P : Ch04.RestrictionCoeffLaw d} (hP : Ch04.RestrictionLawCarrier P) (hStruct : Ch04.RestrictionStructuralLaw P) (center : ℤ) (S : FullBlockMat d) (Q : TriadicCube d) (j : ℕ) (a : RegCoeffField d) : ℝ

Squared operator norm of the descendant-average arbitrary-normalizer fluctuation matrix.

Equations

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

noncomputable def HCPolySupport.Book.Ch05.Section56.coarseAverageErrorMatrixWithNormalizer {d : ℕ} [NeZero d] {P : Ch04.RestrictionCoeffLaw d} (hP : Ch04.RestrictionLawCarrier P) (hStruct : Ch04.RestrictionStructuralLaw P) (center : ℤ) (S : FullBlockMat d) (Q : TriadicCube d) (j : ℕ) (a : RegCoeffField d) : FullBlockMat d

Parent-minus-descendant-average error for an arbitrary normalizer.

Equations

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

noncomputable def HCPolySupport.Book.Ch05.Section56.coarseAveragePositiveErrorMatrixWithNormalizer {d : ℕ} [NeZero d] {P : Ch04.RestrictionCoeffLaw d} (hP : Ch04.RestrictionLawCarrier P) (hStruct : Ch04.RestrictionStructuralLaw P) (center : ℤ) (S : FullBlockMat d) (Q : TriadicCube d) (j : ℕ) (a : RegCoeffField d) : FullBlockMat d

Descendant-average-minus-parent error for an arbitrary normalizer, with the sign used by block subadditivity.

Equations

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

noncomputable def HCPolySupport.Book.Ch05.Section56.coarseAverageErrorOperatorNormSqWithNormalizer {d : ℕ} [NeZero d] {P : Ch04.RestrictionCoeffLaw d} (hP : Ch04.RestrictionLawCarrier P) (hStruct : Ch04.RestrictionStructuralLaw P) (center : ℤ) (S : FullBlockMat d) (Q : TriadicCube d) (j : ℕ) (a : RegCoeffField d) : ℝ

Squared operator norm of the arbitrary-normalizer parent-minus-descendant average error.

Equations

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

noncomputable def HCPolySupport.Book.Ch05.Section56.blockJObservableCubeSetBlockVec {d : ℕ} (Q : TriadicCube d) (P Qv : BlockVec d) : RegCoeffField d → ℝ

The Ch4 block response observable, repackaged using the two block vectors P and Q. The ordering matches the doubled formalism: BlockJ (p,q) (qStar,pStar) is stored as blockJObservableCubeSet Q p pStar q qStar.

Equations

• HCPolySupport.Book.Ch05.Section56.blockJObservableCubeSetBlockVec Q P Qv = HCPolySupport.Book.Ch04.blockJObservableCubeSet Q P.1 Qv.2 P.2 Qv.1

noncomputable def HCPolySupport.Book.Ch05.Section56.fullBlockMatrixProbe {d : ℕ} (S : FullBlockMat d) (α : BlockCoord d) : BlockVec d

Coordinate probe associated with an arbitrary full-block matrix.

Equations

• HCPolySupport.Book.Ch05.Section56.fullBlockMatrixProbe S α = HCPolySupport.ofFullBlockVec (Matrix.mulVec S (Pi.single α 1))

noncomputable def HCPolySupport.Book.Ch05.Section56.blockJTraceAverageWithNormalizers {d : ℕ} (S T : FullBlockMat d) (Q : TriadicCube d) (j : ℕ) (a : RegCoeffField d) : ℝ

The trace-type descendant-average J budget with arbitrary deterministic normalizers. In the manuscript case, use S = B^{-1/2} and T = B^{1/2}.

Equations

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

noncomputable def HCPolySupport.Book.Ch05.Section56.blockJTraceAverageSqWithNormalizers {d : ℕ} (S T : FullBlockMat d) (Q : TriadicCube d) (j : ℕ) (a : RegCoeffField d) : ℝ

Squared trace-type descendant-average J budget with arbitrary normalizers.

Equations

• HCPolySupport.Book.Ch05.Section56.blockJTraceAverageSqWithNormalizers S T Q j a = HCPolySupport.Book.Ch05.Section56.blockJTraceAverageWithNormalizers S T Q j a ^ 2

noncomputable def HCPolySupport.Book.Ch05.Section56.scalarFullBlockSqrtDiag {d : ℕ} (b c : ℝ) : BlockCoord d → ℝ

Diagonal square-root multiplier dual to Ch04.scalarFullBlockInvSqrtDiag. For the lower starred block the scalar block is c⁻¹, hence the square-root multiplier is (sqrt c)⁻¹.

Equations

• HCPolySupport.Book.Ch05.Section56.scalarFullBlockSqrtDiag b c (Sum.inl val) = √b
• HCPolySupport.Book.Ch05.Section56.scalarFullBlockSqrtDiag b c (Sum.inr val) = (√c)⁻¹

noncomputable def HCPolySupport.Book.Ch05.Section56.normalizedInvSqrtBlockProbe {d : ℕ} [NeZero d] {P : Ch04.RestrictionCoeffLaw d} (hP : Ch04.RestrictionLawCarrier P) (hStruct : Ch04.RestrictionStructuralLaw P) (center : ℤ) (α : BlockCoord d) : BlockVec d

Coordinate probe B^{-1/2} e_α for the scalar block normalization at the center scale.

Equations

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

noncomputable def HCPolySupport.Book.Ch05.Section56.normalizedSqrtBlockProbe {d : ℕ} [NeZero d] {P : Ch04.RestrictionCoeffLaw d} (hP : Ch04.RestrictionLawCarrier P) (hStruct : Ch04.RestrictionStructuralLaw P) (center : ℤ) (α : BlockCoord d) : BlockVec d

Coordinate probe B^{1/2} e_α for the scalar block normalization at the center scale.

Equations

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

noncomputable def HCPolySupport.Book.Ch05.Section56.normalizedBlockJTraceAverage {d : ℕ} [NeZero d] {P : Ch04.RestrictionCoeffLaw d} (hP : Ch04.RestrictionLawCarrier P) (hStruct : Ch04.RestrictionStructuralLaw P) (center : ℤ) (Q : TriadicCube d) (j : ℕ) (a : RegCoeffField d) : ℝ

The manuscript trace-type descendant average avg_R sum_i J(R,B^{-1/2}e_i,B^{1/2}e_i), written for the scalar block normalization used by the Section 5.4 fluctuation observable.

Equations

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

noncomputable def HCPolySupport.Book.Ch05.Section56.normalizedUpperBlockJTraceAverage {d : ℕ} [NeZero d] {P : Ch04.RestrictionCoeffLaw d} (hP : Ch04.RestrictionLawCarrier P) (hStruct : Ch04.RestrictionStructuralLaw P) (center : ℤ) (Q : TriadicCube d) (j : ℕ) (a : RegCoeffField d) : ℝ

The upper-coordinate part of normalizedBlockJTraceAverage. The wrap-around trace estimate naturally produces this half of the full block trace budget; the lower half is nonnegative and is added back below.

Equations

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

noncomputable def HCPolySupport.Book.Ch05.Section56.normalizedBlockJTraceAverageSq {d : ℕ} [NeZero d] {P : Ch04.RestrictionCoeffLaw d} (hP : Ch04.RestrictionLawCarrier P) (hStruct : Ch04.RestrictionStructuralLaw P) (center : ℤ) (Q : TriadicCube d) (j : ℕ) (a : RegCoeffField d) : ℝ

Squared trace-type descendant average of the normalized block responses.

Equations

• HCPolySupport.Book.Ch05.Section56.normalizedBlockJTraceAverageSq hP hStruct center Q j a = HCPolySupport.Book.Ch05.Section56.normalizedBlockJTraceAverage hP hStruct center Q j a ^ 2

theorem HCPolySupport.Book.Ch05.Section56.blockJObservableCubeSetBlockVec_nonneg {d : ℕ} (Q : TriadicCube d) (P Qv : BlockVec d) (a : RegCoeffField d) : 0 ≤ blockJObservableCubeSetBlockVec Q P Qv a

theorem HCPolySupport.Book.Ch05.Section56.normalizedBlockJTraceAverage_nonneg {d : ℕ} [NeZero d] {P : Ch04.RestrictionCoeffLaw d} (hP : Ch04.RestrictionLawCarrier P) (hStruct : Ch04.RestrictionStructuralLaw P) (center : ℤ) (Q : TriadicCube d) (j : ℕ) (a : RegCoeffField d) : 0 ≤ normalizedBlockJTraceAverage hP hStruct center Q j a

theorem HCPolySupport.Book.Ch05.Section56.normalizedUpperBlockJTraceAverage_le_normalizedBlockJTraceAverage {d : ℕ} [NeZero d] {P : Ch04.RestrictionCoeffLaw d} (hP : Ch04.RestrictionLawCarrier P) (hStruct : Ch04.RestrictionStructuralLaw P) (center : ℤ) (Q : TriadicCube d) (j : ℕ) (a : RegCoeffField d) : normalizedUpperBlockJTraceAverage hP hStruct center Q j a ≤ normalizedBlockJTraceAverage hP hStruct center Q j a

theorem HCPolySupport.Book.Ch05.Section56.normalizedBlockJTraceAverageSq_nonneg {d : ℕ} [NeZero d] {P : Ch04.RestrictionCoeffLaw d} (hP : Ch04.RestrictionLawCarrier P) (hStruct : Ch04.RestrictionStructuralLaw P) (center : ℤ) (Q : TriadicCube d) (j : ℕ) (a : RegCoeffField d) : 0 ≤ normalizedBlockJTraceAverageSq hP hStruct center Q j a

theorem HCPolySupport.Book.Ch05.Section56.memLp_two_comp_adjointCoeffField {d : ℕ} {P : Ch04.RestrictionCoeffLaw d} {X : RegCoeffField d → ℝ} (hAdj : Ch04.RestrictionAdjointInvariantLaw P) (hX : MeasureTheory.MemLp X 2 P) : MeasureTheory.MemLp (fun (a : RegCoeffField d) => X (adjointReg a)) 2 P

theorem HCPolySupport.Book.Ch05.Section56.memLp_two_blockJObservableCubeSetBlockVec_from_P4_of_stationary {d : ℕ} [NeZero d] {P : Ch04.RestrictionCoeffLaw d} (hP : Ch04.RestrictionLawCarrier P) (hStruct : Ch04.RestrictionStructuralLaw P) (hP4 : QuantitativeCoarseGrainedEllipticity P) (R : TriadicCube d) (hR_nonneg : 0 ≤ R.scale) (Pvec Qvec : BlockVec d) : MeasureTheory.MemLp (blockJObservableCubeSetBlockVec R Pvec Qvec) 2 P

theorem HCPolySupport.Book.Ch05.Section56.memLp_two_normalizedBlockJTraceAverage_from_P4_of_stationary {d : ℕ} [NeZero d] {P : Ch04.RestrictionCoeffLaw d} (hP : Ch04.RestrictionLawCarrier P) (hStruct : Ch04.RestrictionStructuralLaw P) (hP4 : QuantitativeCoarseGrainedEllipticity P) (m n k : ℕ) (_hk : k ≤ n) : MeasureTheory.MemLp (normalizedBlockJTraceAverage hP hStruct (↑m) (originCube d ↑n) (n - k)) 2 P

theorem HCPolySupport.Book.Ch05.Section56.integrable_normalizedBlockJTraceAverageSq_from_P4_of_stationary {d : ℕ} [NeZero d] {P : Ch04.RestrictionCoeffLaw d} (hP : Ch04.RestrictionLawCarrier P) (hStruct : Ch04.RestrictionStructuralLaw P) (hP4 : QuantitativeCoarseGrainedEllipticity P) (m n k : ℕ) (hk : k ≤ n) : MeasureTheory.Integrable (normalizedBlockJTraceAverageSq hP hStruct (↑m) (originCube d ↑n) (n - k)) P

theorem HCPolySupport.Book.Ch05.Section56.doubledResponseJ_eq_blockJObservableCubeSetBlockVec_of_aelocallyUniformlyEllipticField {d : ℕ} [NeZero d] {a : RegCoeffField d} (ha : Ch04.AELocallyUniformlyEllipticField a) (Q : TriadicCube d) (P Qv : BlockVec d) : Ch02.doubledResponseJ (Ch02.cubeDomain Q) ((Ch04.triadicCoeffFamilyOfAELocallyUniformlyEllipticField a ha).coeffOn Q) P Qv = blockJObservableCubeSetBlockVec Q P Qv a