Coarse-graining support:

Support.Book.Ch05.Theorems.Section54.VarianceBoundGoodScale.ScalarReduction

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

Scalar form of the variance-bound left-hand side

This file packages the exact beta-weighted scalar expression appearing in the variance bound at a good scale and records the basic order facts needed by the later reduction steps.

noncomputable def HCPolySupport.Book.Ch05.Section54.VarianceBoundGoodScale.varianceGoodScaleFullBlockSumAtScale {d : ℕ} [NeZero d] {P : Ch04.RestrictionCoeffLaw d} (hP : Ch04.RestrictionLawCarrier P) (hStruct : Ch04.RestrictionStructuralLaw P) (hP4 : QuantitativeCoarseGrainedEllipticity P) (m : ℕ) : ℝ

The beta-weighted full-block fluctuation sum appearing in l.variance.bound.good.scale.homogenization.scale.

Equations

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

theorem HCPolySupport.Book.Ch05.Section54.VarianceBoundGoodScale.varianceGoodScaleFullBlockSumAtScale_nonneg {d : ℕ} [NeZero d] {P : Ch04.RestrictionCoeffLaw d} (hP : Ch04.RestrictionLawCarrier P) (hStruct : Ch04.RestrictionStructuralLaw P) (hP4 : QuantitativeCoarseGrainedEllipticity P) (m : ℕ) : 0 ≤ varianceGoodScaleFullBlockSumAtScale hP hStruct hP4 m

The variance-bound left-hand side is nonnegative.

theorem HCPolySupport.Book.Ch05.Section54.VarianceBoundGoodScale.varianceGoodScaleFullBlockSumAtScale_le_weighted_sum {d : ℕ} [NeZero d] {P : Ch04.RestrictionCoeffLaw d} (hP : Ch04.RestrictionLawCarrier P) (hStruct : Ch04.RestrictionStructuralLaw P) (hP4 : QuantitativeCoarseGrainedEllipticity P) (m : ℕ) {F : ℕ → ℝ} (hF : ∀ j ∈ Finset.Icc 1 m, ∫ (a : RegCoeffField d), Ch04.fullBlockNormalizedFluctuationOperatorNormSqAtScale hP hStruct (↑m) (originCube d ↑j) a ∂P ≤ F j) : varianceGoodScaleFullBlockSumAtScale hP hStruct hP4 m ≤ ∑ j ∈ Finset.Icc 1 m, varianceWeight (section54VarianceBeta hP4) m j * F j

Sumwise comparison principle for the variance-bound left-hand side.

theorem HCPolySupport.Book.Ch05.Section54.VarianceBoundGoodScale.varianceGoodScaleFullBlockSumAtScale_le_weighted_const {d : ℕ} [NeZero d] {P : Ch04.RestrictionCoeffLaw d} (hP : Ch04.RestrictionLawCarrier P) (hStruct : Ch04.RestrictionStructuralLaw P) (hP4 : QuantitativeCoarseGrainedEllipticity P) (m : ℕ) {C : ℝ} (hC : ∀ j ∈ Finset.Icc 1 m, ∫ (a : RegCoeffField d), Ch04.fullBlockNormalizedFluctuationOperatorNormSqAtScale hP hStruct (↑m) (originCube d ↑j) a ∂P ≤ C) : varianceGoodScaleFullBlockSumAtScale hP hStruct hP4 m ≤ (∑ j ∈ Finset.Icc 1 m, varianceWeight (section54VarianceBeta hP4) m j) * C

Constant comparison principle for the variance-bound left-hand side.

theorem HCPolySupport.Book.Ch05.Section54.VarianceBoundGoodScale.fullBlockNormalizedQuadraticObservable_le_restrictionDescendantAverageOnCube_ae {d : ℕ} [NeZero d] {P : Ch04.RestrictionCoeffLaw d} (hP : Ch04.RestrictionLawCarrier P) (hStruct : Ch04.RestrictionStructuralLaw P) (center : ℤ) (q : FullBlockVec d) (Q : TriadicCube d) {k : ℤ} (hk : k ≤ Q.scale) : (fun (a : RegCoeffField d) => normalizedQuadraticObservable hP hStruct center q (cubeSet Q) a.toFun) ≤ᵐ[P] fun (a : RegCoeffField d) => Ch04.restrictionDescendantAverageOnCube Q k (fullBlockNormalizedQuadraticObservableR hP hStruct center q) a

Block-matrix subadditivity, after scalar normalization and testing against a fixed full-block vector. This is the deterministic bridge from the Ch4 Löwner comparison to the scalar partition average used in the good-scale variance proof.

theorem HCPolySupport.Book.Ch05.Section54.VarianceBoundGoodScale.fullBlockNormalizedQuadraticObservable_positivePart_le_delta_add_centeredAverageOnCube_ae {d : ℕ} [NeZero d] {P : Ch04.RestrictionCoeffLaw d} (hP : Ch04.RestrictionLawCarrier P) (hStruct : Ch04.RestrictionStructuralLaw P) (center : ℤ) (q : FullBlockVec d) (Q : TriadicCube d) {k : ℤ} (hk : k ≤ Q.scale) {delta : ℝ} (hdelta_nonneg : 0 ≤ delta) (hmean_le : ∫ (b : RegCoeffField d), normalizedQuadraticObservable hP hStruct center q (cubeSet (originCube d k)) b.toFun ∂P ≤ 1 + delta) : (fun (a : RegCoeffField d) => max (normalizedQuadraticObservable hP hStruct center q (cubeSet Q) a.toFun - 1) 0) ≤ᵐ[P] fun (a : RegCoeffField d) => delta + |Ch04.restrictionCenteredDescendantAverageOnCube P Q k (fullBlockNormalizedQuadraticObservableR hP hStruct center q) a|

Positive-part control for a normalized quadratic probe. Once the origin scale-k annealed value is at most 1 + delta, the pointwise positive excess over 1 is bounded by delta plus the centered descendant average.

theorem HCPolySupport.Book.Ch05.Section54.VarianceBoundGoodScale.fullBlockNormalizedQuadraticObservable_positivePart_base_le_error_add_centeredAverageOnCube_ae {d : ℕ} [NeZero d] {P : Ch04.RestrictionCoeffLaw d} (hP : Ch04.RestrictionLawCarrier P) (hStruct : Ch04.RestrictionStructuralLaw P) (center : ℤ) (q : FullBlockVec d) (Q : TriadicCube d) {k : ℤ} (hk : k ≤ Q.scale) {base err : ℝ} (herr_nonneg : 0 ≤ err) (hmean_le : ∫ (b : RegCoeffField d), normalizedQuadraticObservable hP hStruct center q (cubeSet (originCube d k)) b.toFun ∂P ≤ base + err) : (fun (a : RegCoeffField d) => max (normalizedQuadraticObservable hP hStruct center q (cubeSet Q) a.toFun - base) 0) ≤ᵐ[P] fun (a : RegCoeffField d) => err + |Ch04.restrictionCenteredDescendantAverageOnCube P Q k (fullBlockNormalizedQuadraticObservableR hP hStruct center q) a|

Base-parameter version of fullBlockNormalizedQuadraticObservable_positivePart_le_delta_add_centeredAverageOnCube_ae. It is used for the non-unit plus/minus probes in the finite-dimensional upgrade.

theorem HCPolySupport.Book.Ch05.Section54.VarianceBoundGoodScale.integral_origin_fullBlockNormalizedQuadraticObservable_eq_annealedBlockMatrixAtScale {d : ℕ} [NeZero d] {P : Ch04.RestrictionCoeffLaw d} (hP : Ch04.RestrictionLawCarrier P) (hStruct : Ch04.RestrictionStructuralLaw P) (center n : ℤ) (q : FullBlockVec d) (hBlock : MeasureTheory.Integrable (Ch04.coarseFullBlockMatrixAtCube (originCube d n)) P) : have b := hP.barSigmaAtScale hStruct center; have c := hP.barSigmaStarAtScale hStruct center; have D := Matrix.diagonal (Ch04.scalarFullBlockInvSqrtDiag b c); ∫ (a : RegCoeffField d), normalizedQuadraticObservable hP hStruct center q (cubeSet (originCube d n)) a.toFun ∂P = fullBlockQuadratic (D * toFullBlockMat (Ch04.annealedBlockMatrixAtScale P n) * D) q

The mean of a normalized quadratic probe on an origin cube is the same quadratic form applied to the corresponding annealed full-block matrix.

theorem HCPolySupport.Book.Ch05.Section54.VarianceBoundGoodScale.integral_origin_fullBlockNormalizedQuadraticObservable_eq_annealedBlockMatrixAtScale_from_P4 {d : ℕ} [NeZero d] {P : Ch04.RestrictionCoeffLaw d} (hP : Ch04.RestrictionLawCarrier P) (hStruct : Ch04.RestrictionStructuralLaw P) (hP4 : QuantitativeCoarseGrainedEllipticity P) (center n : ℤ) (hn : 0 ≤ n) (q : FullBlockVec d) : have b := hP.barSigmaAtScale hStruct center; have c := hP.barSigmaStarAtScale hStruct center; have D := Matrix.diagonal (Ch04.scalarFullBlockInvSqrtDiag b c); ∫ (a : RegCoeffField d), normalizedQuadraticObservable hP hStruct center q (cubeSet (originCube d n)) a.toFun ∂P = fullBlockQuadratic (D * toFullBlockMat (Ch04.annealedBlockMatrixAtScale P n) * D) q

(P4) supplies the integrability in integral_origin_fullBlockNormalizedQuadraticObservable_eq_annealedBlockMatrixAtScale for nonnegative origin scales.

theorem HCPolySupport.Book.Ch05.Section54.VarianceBoundGoodScale.normalizedAnnealedQuadratic_le_one_add_delta_mul_dotProduct_of_good {d : ℕ} [NeZero d] {P : Ch04.RestrictionCoeffLaw d} (hP : Ch04.RestrictionLawCarrier P) (hStruct : Ch04.RestrictionStructuralLaw P) (hP4 : QuantitativeCoarseGrainedEllipticity P) {delta : ℝ} (m k : ℕ) (_hk : k ≤ m) (hgood_upper : hP.barSigmaAtScale hStruct 0 ≤ (1 + delta) * hP.barSigmaAtScale hStruct ↑m) (hgood_lower : (hP.barSigmaStarAtScale hStruct 0)⁻¹ ≤ (1 + delta) * (hP.barSigmaStarAtScale hStruct ↑m)⁻¹) (q : FullBlockVec d) : have bm := hP.barSigmaAtScale hStruct ↑m; have cm := hP.barSigmaStarAtScale hStruct ↑m; have D := Matrix.diagonal (Ch04.scalarFullBlockInvSqrtDiag bm cm); fullBlockQuadratic (D * toFullBlockMat (Ch04.annealedBlockMatrixAtScale P ↑k) * D) q ≤ (1 + delta) * q ⬝ᵥ q

At a good scale, each intermediate annealed block is at most (1+delta) after normalization by the top scale.

theorem HCPolySupport.Book.Ch05.Section54.VarianceBoundGoodScale.dotProduct_le_normalizedAnnealedQuadratic_of_scalarChain {d : ℕ} [NeZero d] {P : Ch04.RestrictionCoeffLaw d} (hP : Ch04.RestrictionLawCarrier P) (hStruct : Ch04.RestrictionStructuralLaw P) (hP4 : QuantitativeCoarseGrainedEllipticity P) (m k : ℕ) (hk : k ≤ m) (q : FullBlockVec d) : have bm := hP.barSigmaAtScale hStruct ↑m; have cm := hP.barSigmaStarAtScale hStruct ↑m; have D := Matrix.diagonal (Ch04.scalarFullBlockInvSqrtDiag bm cm); q ⬝ᵥ q ≤ fullBlockQuadratic (D * toFullBlockMat (Ch04.annealedBlockMatrixAtScale P ↑k) * D) q

Scalar-chain monotonicity gives the lower normalized annealed bound.

theorem HCPolySupport.Book.Ch05.Section54.VarianceBoundGoodScale.integral_origin_fullBlockNormalizedQuadraticObservable_le_base_add_delta_mul_dotProduct_of_good {d : ℕ} [NeZero d] {P : Ch04.RestrictionCoeffLaw d} (hP : Ch04.RestrictionLawCarrier P) (hStruct : Ch04.RestrictionStructuralLaw P) (hP4 : QuantitativeCoarseGrainedEllipticity P) {delta : ℝ} (m k : ℕ) (hk : k ≤ m) (hgood_upper : hP.barSigmaAtScale hStruct 0 ≤ (1 + delta) * hP.barSigmaAtScale hStruct ↑m) (hgood_lower : (hP.barSigmaStarAtScale hStruct 0)⁻¹ ≤ (1 + delta) * (hP.barSigmaStarAtScale hStruct ↑m)⁻¹) (q : FullBlockVec d) : ∫ (a : RegCoeffField d), normalizedQuadraticObservable hP hStruct (↑m) q (cubeSet (originCube d ↑k)) a.toFun ∂P ≤ q ⬝ᵥ q + delta * q ⬝ᵥ q

Good-scale upper bound for the mean of a normalized quadratic probe.

theorem HCPolySupport.Book.Ch05.Section54.VarianceBoundGoodScale.dotProduct_le_integral_origin_fullBlockNormalizedQuadraticObservable_of_scalarChain {d : ℕ} [NeZero d] {P : Ch04.RestrictionCoeffLaw d} (hP : Ch04.RestrictionLawCarrier P) (hStruct : Ch04.RestrictionStructuralLaw P) (hP4 : QuantitativeCoarseGrainedEllipticity P) (m k : ℕ) (hk : k ≤ m) (q : FullBlockVec d) : q ⬝ᵥ q ≤ ∫ (a : RegCoeffField d), normalizedQuadraticObservable hP hStruct (↑m) q (cubeSet (originCube d ↑k)) a.toFun ∂P

Scalar-chain lower bound for the mean of a normalized quadratic probe.

theorem HCPolySupport.Book.Ch05.Section54.VarianceBoundGoodScale.fullBlockNormalizedQuadraticObservable_positivePart_good_origin_ae {d : ℕ} [NeZero d] {P : Ch04.RestrictionCoeffLaw d} (hP : Ch04.RestrictionLawCarrier P) (hStruct : Ch04.RestrictionStructuralLaw P) (hP4 : QuantitativeCoarseGrainedEllipticity P) {delta : ℝ} (hdelta_nonneg : 0 ≤ delta) (m j : ℕ) (hgood_upper : hP.barSigmaAtScale hStruct 0 ≤ (1 + delta) * hP.barSigmaAtScale hStruct ↑m) (hgood_lower : (hP.barSigmaStarAtScale hStruct 0)⁻¹ ≤ (1 + delta) * (hP.barSigmaStarAtScale hStruct ↑m)⁻¹) (q : FullBlockVec d) : (fun (a : RegCoeffField d) => max (normalizedQuadraticObservable hP hStruct (↑m) q (cubeSet (originCube d ↑j)) a.toFun - q ⬝ᵥ q) 0) ≤ᵐ[P] fun (a : RegCoeffField d) => delta * q ⬝ᵥ q + |Ch04.restrictionCenteredDescendantAverage P 0 (↑j) (fullBlockNormalizedQuadraticObservableR hP hStruct (↑m) q) a|

Good-scale positive-part control for a normalized quadratic probe on an origin cube.