Coarse-graining support:

Support.Book.Ch05.Theorems.Section54.VarianceBoundGoodScale.QuadraticProbeBounds

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

Pointwise bounds for normalized quadratic probes

This file supplies the remaining Section 5.4-local bridge from the normalized quadratic probes used in the finite-dimensional upgrade to the unit-scale coarse-grained ellipticity factors controlled by (P4).

noncomputable def HCPolySupport.Book.Ch05.Section54.VarianceBoundGoodScale.unitScaleEllipticityFactorSum {d : ℕ} [NeZero d] {P : Ch04.RestrictionCoeffLaw d} (hP4 : QuantitativeCoarseGrainedEllipticity P) (a : RegCoeffField d) : ℝ

Unit-scale sum of the two coarse-grained ellipticity observables appearing in (P4).

Equations

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

theorem HCPolySupport.Book.Ch05.Section54.VarianceBoundGoodScale.unitScaleEllipticityFactorSum_nonneg {d : ℕ} [NeZero d] {P : Ch04.RestrictionCoeffLaw d} (hP4 : QuantitativeCoarseGrainedEllipticity P) (a : RegCoeffField d) : 0 ≤ unitScaleEllipticityFactorSum hP4 a

theorem HCPolySupport.Book.Ch05.Section54.VarianceBoundGoodScale.blockMatEntry_abs_le_unitScaleEllipticityFactorSum_origin_ae {d : ℕ} [NeZero d] {P : Ch04.RestrictionCoeffLaw d} (hP : Ch04.RestrictionLawCarrier P) (hP4 : QuantitativeCoarseGrainedEllipticity P) (α β : BlockCoord d) : (fun (a : RegCoeffField d) => |blockMatEntry (coarseBlockMatrix (cubeSet (originCube d 0)) a.toFun) α β|) ≤ᵐ[P] fun (a : RegCoeffField d) => unitScaleEllipticityFactorSum hP4 a

Entrywise domination of the unit coarse block matrix by the two unit-scale coarse-grained ellipticity factors from (P4).

theorem HCPolySupport.Book.Ch05.Section54.VarianceBoundGoodScale.isSymm_diagonal_mul_toFullBlockMat_mul_diagonal {d : ℕ} (r : BlockCoord d → ℝ) {A : BlockMat d} (hA : IsSymmetricBlockMat A) : (Matrix.diagonal r * toFullBlockMat A * Matrix.diagonal r).IsSymm

theorem HCPolySupport.Book.Ch05.Section54.VarianceBoundGoodScale.fullBlockQuadratic_diagonal_coordinateProbe {d : ℕ} (r : BlockCoord d → ℝ) (A : BlockMat d) (α : BlockCoord d) : fullBlockQuadratic (Matrix.diagonal r * toFullBlockMat A * Matrix.diagonal r) (fullBlockCoordinateProbe α) = r α * blockMatEntry A α α * r α

theorem HCPolySupport.Book.Ch05.Section54.VarianceBoundGoodScale.fullBlockQuadratic_diagonal_plusProbe_of_ne {d : ℕ} (r : BlockCoord d → ℝ) {A : BlockMat d} (hA : IsSymmetricBlockMat A) {α β : BlockCoord d} (hαβ : α ≠ β) : fullBlockQuadratic (Matrix.diagonal r * toFullBlockMat A * Matrix.diagonal r) (fullBlockPlusProbe α β) = r α * blockMatEntry A α α * r α + 2 * (r α * blockMatEntry A α β * r β) + r β * blockMatEntry A β β * r β

theorem HCPolySupport.Book.Ch05.Section54.VarianceBoundGoodScale.fullBlockQuadratic_diagonal_minusProbe_of_ne {d : ℕ} (r : BlockCoord d → ℝ) {A : BlockMat d} (hA : IsSymmetricBlockMat A) {α β : BlockCoord d} (hαβ : α ≠ β) : fullBlockQuadratic (Matrix.diagonal r * toFullBlockMat A * Matrix.diagonal r) (fullBlockMinusProbe α β) = r α * blockMatEntry A α α * r α - 2 * (r α * blockMatEntry A α β * r β) + r β * blockMatEntry A β β * r β

noncomputable def HCPolySupport.Book.Ch05.Section54.VarianceBoundGoodScale.coordinateProbeFactor {d : ℕ} [NeZero d] {P : Ch04.RestrictionCoeffLaw d} (hP : Ch04.RestrictionLawCarrier P) (hStruct : Ch04.RestrictionStructuralLaw P) (center : ℤ) (α : BlockCoord d) : ℝ

Coefficient in the unit-scale factor bound for a normalized coordinate probe.

Equations

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

theorem HCPolySupport.Book.Ch05.Section54.VarianceBoundGoodScale.coordinateProbeFactor_nonneg {d : ℕ} [NeZero d] {P : Ch04.RestrictionCoeffLaw d} (hP : Ch04.RestrictionLawCarrier P) (hStruct : Ch04.RestrictionStructuralLaw P) (center : ℤ) (α : BlockCoord d) : 0 ≤ coordinateProbeFactor hP hStruct center α

noncomputable def HCPolySupport.Book.Ch05.Section54.VarianceBoundGoodScale.pairProbeFactor {d : ℕ} [NeZero d] {P : Ch04.RestrictionCoeffLaw d} (hP : Ch04.RestrictionLawCarrier P) (hStruct : Ch04.RestrictionStructuralLaw P) (center : ℤ) (α β : BlockCoord d) : ℝ

Coefficient in the unit-scale factor bound for a normalized plus/minus pair probe.

Equations

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

theorem HCPolySupport.Book.Ch05.Section54.VarianceBoundGoodScale.pairProbeFactor_nonneg {d : ℕ} [NeZero d] {P : Ch04.RestrictionCoeffLaw d} (hP : Ch04.RestrictionLawCarrier P) (hStruct : Ch04.RestrictionStructuralLaw P) (center : ℤ) (α β : BlockCoord d) : 0 ≤ pairProbeFactor hP hStruct center α β

theorem HCPolySupport.Book.Ch05.Section54.VarianceBoundGoodScale.abs_mul_entry_mul_le_factor {F x y e : ℝ} (he : |e| ≤ F) : |x * e * y| ≤ |x| * |y| * F

theorem HCPolySupport.Book.Ch05.Section54.VarianceBoundGoodScale.fullBlockNormalizedQuadraticObservable_coordinateProbe_abs_le_factorSum_ae {d : ℕ} [NeZero d] {P : Ch04.RestrictionCoeffLaw d} (hP : Ch04.RestrictionLawCarrier P) (hStruct : Ch04.RestrictionStructuralLaw P) (hP4 : QuantitativeCoarseGrainedEllipticity P) (center : ℤ) (α : BlockCoord d) : (fun (a : RegCoeffField d) => |normalizedQuadraticObservable hP hStruct center (fullBlockCoordinateProbe α) (cubeSet (originCube d 0)) a.toFun|) ≤ᵐ[P] fun (a : RegCoeffField d) => coordinateProbeFactor hP hStruct center α * unitScaleEllipticityFactorSum hP4 a

The normalized coordinate quadratic probe is pointwise dominated, a.s., by the (P4) unit-scale ellipticity factor sum.

theorem HCPolySupport.Book.Ch05.Section54.VarianceBoundGoodScale.fullBlockNormalizedQuadraticObservable_plusProbe_abs_le_factorSum_ae {d : ℕ} [NeZero d] {P : Ch04.RestrictionCoeffLaw d} (hP : Ch04.RestrictionLawCarrier P) (hStruct : Ch04.RestrictionStructuralLaw P) (hP4 : QuantitativeCoarseGrainedEllipticity P) (center : ℤ) {α β : BlockCoord d} (hαβ : α ≠ β) : (fun (a : RegCoeffField d) => |normalizedQuadraticObservable hP hStruct center (fullBlockPlusProbe α β) (cubeSet (originCube d 0)) a.toFun|) ≤ᵐ[P] fun (a : RegCoeffField d) => pairProbeFactor hP hStruct center α β * unitScaleEllipticityFactorSum hP4 a

The normalized plus-pair quadratic probe is pointwise dominated, a.s., by the (P4) unit-scale ellipticity factor sum.

theorem HCPolySupport.Book.Ch05.Section54.VarianceBoundGoodScale.fullBlockNormalizedQuadraticObservable_minusProbe_abs_le_factorSum_ae {d : ℕ} [NeZero d] {P : Ch04.RestrictionCoeffLaw d} (hP : Ch04.RestrictionLawCarrier P) (hStruct : Ch04.RestrictionStructuralLaw P) (hP4 : QuantitativeCoarseGrainedEllipticity P) (center : ℤ) {α β : BlockCoord d} (hαβ : α ≠ β) : (fun (a : RegCoeffField d) => |normalizedQuadraticObservable hP hStruct center (fullBlockMinusProbe α β) (cubeSet (originCube d 0)) a.toFun|) ≤ᵐ[P] fun (a : RegCoeffField d) => pairProbeFactor hP hStruct center α β * unitScaleEllipticityFactorSum hP4 a

The normalized minus-pair quadratic probe is pointwise dominated, a.s., by the (P4) unit-scale ellipticity factor sum.

theorem HCPolySupport.Book.Ch05.Section54.VarianceBoundGoodScale.coordinateProbe_centeredOrigin_momentRoot_le_factorSum {d : ℕ} [NeZero d] {P : Ch04.RestrictionCoeffLaw d} (hP : Ch04.RestrictionLawCarrier P) (hStruct : Ch04.RestrictionStructuralLaw P) (hP4 : QuantitativeCoarseGrainedEllipticity P) (center : ℤ) (α : BlockCoord d) : MeasureTheory.Integrable (fun (a : RegCoeffField d) => |Ch04.restrictionCenteredOriginObservable P 0 (fullBlockNormalizedQuadraticObservableR hP hStruct center (fullBlockCoordinateProbe α)) a| ^ hP4.xi) P ∧ (Ch04.annealedMomentRoot P hP4.xi fun (a : RegCoeffField d) => |Ch04.restrictionCenteredOriginObservable P 0 (fullBlockNormalizedQuadraticObservableR hP hStruct center (fullBlockCoordinateProbe α)) a|) ≤ 2 * coordinateProbeFactor hP hStruct center α * (Ch04.LambdaMomentAtScale P 0 hP4.sUpper hP4.xi + Ch04.lambdaInvMomentAtScale P 0 hP4.sLower hP4.xi)

Centered origin moment input for normalized coordinate probes.

theorem HCPolySupport.Book.Ch05.Section54.VarianceBoundGoodScale.plusProbe_centeredOrigin_momentRoot_le_factorSum {d : ℕ} [NeZero d] {P : Ch04.RestrictionCoeffLaw d} (hP : Ch04.RestrictionLawCarrier P) (hStruct : Ch04.RestrictionStructuralLaw P) (hP4 : QuantitativeCoarseGrainedEllipticity P) (center : ℤ) {α β : BlockCoord d} (hαβ : α ≠ β) : MeasureTheory.Integrable (fun (a : RegCoeffField d) => |Ch04.restrictionCenteredOriginObservable P 0 (fullBlockNormalizedQuadraticObservableR hP hStruct center (fullBlockPlusProbe α β)) a| ^ hP4.xi) P ∧ (Ch04.annealedMomentRoot P hP4.xi fun (a : RegCoeffField d) => |Ch04.restrictionCenteredOriginObservable P 0 (fullBlockNormalizedQuadraticObservableR hP hStruct center (fullBlockPlusProbe α β)) a|) ≤ 2 * pairProbeFactor hP hStruct center α β * (Ch04.LambdaMomentAtScale P 0 hP4.sUpper hP4.xi + Ch04.lambdaInvMomentAtScale P 0 hP4.sLower hP4.xi)

Centered origin moment input for normalized plus-pair probes.

theorem HCPolySupport.Book.Ch05.Section54.VarianceBoundGoodScale.minusProbe_centeredOrigin_momentRoot_le_factorSum {d : ℕ} [NeZero d] {P : Ch04.RestrictionCoeffLaw d} (hP : Ch04.RestrictionLawCarrier P) (hStruct : Ch04.RestrictionStructuralLaw P) (hP4 : QuantitativeCoarseGrainedEllipticity P) (center : ℤ) {α β : BlockCoord d} (hαβ : α ≠ β) : MeasureTheory.Integrable (fun (a : RegCoeffField d) => |Ch04.restrictionCenteredOriginObservable P 0 (fullBlockNormalizedQuadraticObservableR hP hStruct center (fullBlockMinusProbe α β)) a| ^ hP4.xi) P ∧ (Ch04.annealedMomentRoot P hP4.xi fun (a : RegCoeffField d) => |Ch04.restrictionCenteredOriginObservable P 0 (fullBlockNormalizedQuadraticObservableR hP hStruct center (fullBlockMinusProbe α β)) a|) ≤ 2 * pairProbeFactor hP hStruct center α β * (Ch04.LambdaMomentAtScale P 0 hP4.sUpper hP4.xi + Ch04.lambdaInvMomentAtScale P 0 hP4.sLower hP4.xi)

Centered origin moment input for normalized minus-pair probes.

theorem HCPolySupport.Book.Ch05.Section54.VarianceBoundGoodScale.coordinateProbe_restrictionCenteredDescendantAverage_pow_rpow_inv_le {d : ℕ} [NeZero d] {P : Ch04.RestrictionCoeffLaw d} (hP : Ch04.RestrictionLawCarrier P) (hStruct : Ch04.RestrictionStructuralLaw P) (hP4 : QuantitativeCoarseGrainedEllipticity P) {center m : ℤ} (hm : 0 ≤ m) (α : BlockCoord d) : have K := 2 * coordinateProbeFactor hP hStruct center α * (Ch04.LambdaMomentAtScale P 0 hP4.sUpper hP4.xi + Ch04.lambdaInvMomentAtScale P 0 hP4.sLower hP4.xi); (∫ (a : RegCoeffField d), |Ch04.restrictionCenteredDescendantAverage P 0 m (fullBlockNormalizedQuadraticObservableR hP hStruct center (fullBlockCoordinateProbe α)) a| ^ hP4.xi ∂P) ^ (1 / ↑hP4.xi) ≤ (↑(descendantsAtScale (originCube d m) 0).card)⁻¹ * (Ch04.rosenthalDescendantsAtScaleLpConst d 0 hP4.xi * ↑(descendantsAtScale (originCube d m) 0).card ^ (1 / ↑hP4.xi) * K + Ch04.rosenthalDescendantsAtScaleSqrtConst d 0 hP4.xi * √↑(descendantsAtScale (originCube d m) 0).card * K)

Rosenthal partition-average estimate for normalized coordinate probes, with the origin moment supplied internally by (P4).

theorem HCPolySupport.Book.Ch05.Section54.VarianceBoundGoodScale.plusProbe_restrictionCenteredDescendantAverage_pow_rpow_inv_le {d : ℕ} [NeZero d] {P : Ch04.RestrictionCoeffLaw d} (hP : Ch04.RestrictionLawCarrier P) (hStruct : Ch04.RestrictionStructuralLaw P) (hP4 : QuantitativeCoarseGrainedEllipticity P) {center m : ℤ} (hm : 0 ≤ m) {α β : BlockCoord d} (hαβ : α ≠ β) : have K := 2 * pairProbeFactor hP hStruct center α β * (Ch04.LambdaMomentAtScale P 0 hP4.sUpper hP4.xi + Ch04.lambdaInvMomentAtScale P 0 hP4.sLower hP4.xi); (∫ (a : RegCoeffField d), |Ch04.restrictionCenteredDescendantAverage P 0 m (fullBlockNormalizedQuadraticObservableR hP hStruct center (fullBlockPlusProbe α β)) a| ^ hP4.xi ∂P) ^ (1 / ↑hP4.xi) ≤ (↑(descendantsAtScale (originCube d m) 0).card)⁻¹ * (Ch04.rosenthalDescendantsAtScaleLpConst d 0 hP4.xi * ↑(descendantsAtScale (originCube d m) 0).card ^ (1 / ↑hP4.xi) * K + Ch04.rosenthalDescendantsAtScaleSqrtConst d 0 hP4.xi * √↑(descendantsAtScale (originCube d m) 0).card * K)

Rosenthal partition-average estimate for normalized plus-pair probes, with the origin moment supplied internally by (P4).

theorem HCPolySupport.Book.Ch05.Section54.VarianceBoundGoodScale.minusProbe_restrictionCenteredDescendantAverage_pow_rpow_inv_le {d : ℕ} [NeZero d] {P : Ch04.RestrictionCoeffLaw d} (hP : Ch04.RestrictionLawCarrier P) (hStruct : Ch04.RestrictionStructuralLaw P) (hP4 : QuantitativeCoarseGrainedEllipticity P) {center m : ℤ} (hm : 0 ≤ m) {α β : BlockCoord d} (hαβ : α ≠ β) : have K := 2 * pairProbeFactor hP hStruct center α β * (Ch04.LambdaMomentAtScale P 0 hP4.sUpper hP4.xi + Ch04.lambdaInvMomentAtScale P 0 hP4.sLower hP4.xi); (∫ (a : RegCoeffField d), |Ch04.restrictionCenteredDescendantAverage P 0 m (fullBlockNormalizedQuadraticObservableR hP hStruct center (fullBlockMinusProbe α β)) a| ^ hP4.xi ∂P) ^ (1 / ↑hP4.xi) ≤ (↑(descendantsAtScale (originCube d m) 0).card)⁻¹ * (Ch04.rosenthalDescendantsAtScaleLpConst d 0 hP4.xi * ↑(descendantsAtScale (originCube d m) 0).card ^ (1 / ↑hP4.xi) * K + Ch04.rosenthalDescendantsAtScaleSqrtConst d 0 hP4.xi * √↑(descendantsAtScale (originCube d m) 0).card * K)

Rosenthal partition-average estimate for normalized minus-pair probes, with the origin moment supplied internally by (P4).