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

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

Scalar probe variance inputs

This file records the internal integrability bridge for scalar quadratic probes. It keeps the public variance-bound theorem free of extra measurability or integrability assumptions: (P4) controls the full normalized fluctuation, and the deterministic operator-norm bound controls each scalar quadratic probe.

theorem HCPolySupport.Book.Ch05.Section54.VarianceBoundGoodScale.integrable_abs_sub_dotProduct_sq_fullBlockNormalizedQuadraticObservable_from_P4 {d : ℕ} [NeZero d] {P : Ch04.RestrictionCoeffLaw d} (hP : Ch04.RestrictionLawCarrier P) (hStruct : Ch04.RestrictionStructuralLaw P) (hP4 : QuantitativeCoarseGrainedEllipticity P) (m j : ℕ) (q : FullBlockVec d) : MeasureTheory.Integrable (fun (a : RegCoeffField d) => |normalizedQuadraticObservable hP hStruct (↑m) q (cubeSet (originCube d ↑j)) a.toFun - q ⬝ᵥ q| ^ 2) P

(P4) gives the L2 integrability of a centered normalized scalar quadratic probe on an origin cube.

theorem HCPolySupport.Book.Ch05.Section54.VarianceBoundGoodScale.integrable_fullBlockNormalizedQuadraticObservable_and_abs_sub_dotProduct_from_P4 {d : ℕ} [NeZero d] {P : Ch04.RestrictionCoeffLaw d} (hP : Ch04.RestrictionLawCarrier P) (hStruct : Ch04.RestrictionStructuralLaw P) (hP4 : QuantitativeCoarseGrainedEllipticity P) (m j : ℕ) (q : FullBlockVec d) : MeasureTheory.Integrable (fun (a : RegCoeffField d) => normalizedQuadraticObservable hP hStruct (↑m) q (cubeSet (originCube d ↑j)) a.toFun) P ∧ MeasureTheory.Integrable (fun (a : RegCoeffField d) => |normalizedQuadraticObservable hP hStruct (↑m) q (cubeSet (originCube d ↑j)) a.toFun - q ⬝ᵥ q|) P ∧ MeasureTheory.Integrable (fun (a : RegCoeffField d) => |normalizedQuadraticObservable hP hStruct (↑m) q (cubeSet (originCube d ↑j)) a.toFun - q ⬝ᵥ q| ^ 2) P

(P4) also gives the L1 integrability inputs for one normalized scalar quadratic probe on an origin cube.

theorem HCPolySupport.Book.Ch05.Section54.VarianceBoundGoodScale.centeredQuadraticObservable_abs_and_sq_le_of_root {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) (q : FullBlockVec d) {K : ℝ} (hOriginMoment_int : MeasureTheory.Integrable (fun (a : RegCoeffField d) => |Ch04.restrictionCenteredOriginObservable P n (fullBlockNormalizedQuadraticObservableR hP hStruct center q) a| ^ hP4.xi) P) (hroot : (∫ (a : RegCoeffField d), |Ch04.restrictionCenteredDescendantAverage P n m (fullBlockNormalizedQuadraticObservableR hP hStruct center q) a| ^ hP4.xi ∂P) ^ (1 / ↑hP4.xi) ≤ K) : ∫ (a : RegCoeffField d), |Ch04.restrictionCenteredDescendantAverage P n m (fullBlockNormalizedQuadraticObservableR hP hStruct center q) a| ∂P ≤ K ∧ ∫ (a : RegCoeffField d), |Ch04.restrictionCenteredDescendantAverage P n m (fullBlockNormalizedQuadraticObservableR hP hStruct center q) a| ^ 2 ∂P ≤ K ^ 2

Convert the Section 5.4 Rosenthal root bound for a normalized quadratic probe descendant average into the L1 and L2 estimates used by the scalar variance reduction.

theorem HCPolySupport.Book.Ch05.Section54.VarianceBoundGoodScale.centeredQuadraticObservable_abs_and_sq_integrable {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) (q : FullBlockVec d) (hOriginMoment_int : MeasureTheory.Integrable (fun (a : RegCoeffField d) => |Ch04.restrictionCenteredOriginObservable P n (fullBlockNormalizedQuadraticObservableR hP hStruct center q) a| ^ hP4.xi) P) : MeasureTheory.Integrable (fun (a : RegCoeffField d) => |Ch04.restrictionCenteredDescendantAverage P n m (fullBlockNormalizedQuadraticObservableR hP hStruct center q) a|) P ∧ MeasureTheory.Integrable (fun (a : RegCoeffField d) => |Ch04.restrictionCenteredDescendantAverage P n m (fullBlockNormalizedQuadraticObservableR hP hStruct center q) a| ^ 2) P

Integrability of the L1 and L2 sizes of the normalized quadratic-probe descendant average, derived internally from the origin L^ξ moment supplied by (P4).

theorem HCPolySupport.Book.Ch05.Section54.VarianceBoundGoodScale.coordinateProbe_restrictionCenteredDescendantAverage_abs_and_sq_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 := (↑(descendantsAtScale (originCube d m) 0).card)⁻¹ * (Ch04.rosenthalDescendantsAtScaleLpConst d 0 hP4.xi * ↑(descendantsAtScale (originCube d m) 0).card ^ (1 / ↑hP4.xi) * (2 * coordinateProbeFactor hP hStruct center α * (Ch04.LambdaMomentAtScale P 0 hP4.sUpper hP4.xi + Ch04.lambdaInvMomentAtScale P 0 hP4.sLower hP4.xi)) + Ch04.rosenthalDescendantsAtScaleSqrtConst d 0 hP4.xi * √↑(descendantsAtScale (originCube d m) 0).card * (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| ∂P ≤ K ∧ ∫ (a : RegCoeffField d), |Ch04.restrictionCenteredDescendantAverage P 0 m (fullBlockNormalizedQuadraticObservableR hP hStruct center (fullBlockCoordinateProbe α)) a| ^ 2 ∂P ≤ K ^ 2

L1/L2 descendant-average bounds for normalized coordinate probes.

theorem HCPolySupport.Book.Ch05.Section54.VarianceBoundGoodScale.plusProbe_restrictionCenteredDescendantAverage_abs_and_sq_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 := (↑(descendantsAtScale (originCube d m) 0).card)⁻¹ * (Ch04.rosenthalDescendantsAtScaleLpConst d 0 hP4.xi * ↑(descendantsAtScale (originCube d m) 0).card ^ (1 / ↑hP4.xi) * (2 * pairProbeFactor hP hStruct center α β * (Ch04.LambdaMomentAtScale P 0 hP4.sUpper hP4.xi + Ch04.lambdaInvMomentAtScale P 0 hP4.sLower hP4.xi)) + Ch04.rosenthalDescendantsAtScaleSqrtConst d 0 hP4.xi * √↑(descendantsAtScale (originCube d m) 0).card * (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| ∂P ≤ K ∧ ∫ (a : RegCoeffField d), |Ch04.restrictionCenteredDescendantAverage P 0 m (fullBlockNormalizedQuadraticObservableR hP hStruct center (fullBlockPlusProbe α β)) a| ^ 2 ∂P ≤ K ^ 2

L1/L2 descendant-average bounds for normalized plus-pair probes.

theorem HCPolySupport.Book.Ch05.Section54.VarianceBoundGoodScale.minusProbe_restrictionCenteredDescendantAverage_abs_and_sq_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 := (↑(descendantsAtScale (originCube d m) 0).card)⁻¹ * (Ch04.rosenthalDescendantsAtScaleLpConst d 0 hP4.xi * ↑(descendantsAtScale (originCube d m) 0).card ^ (1 / ↑hP4.xi) * (2 * pairProbeFactor hP hStruct center α β * (Ch04.LambdaMomentAtScale P 0 hP4.sUpper hP4.xi + Ch04.lambdaInvMomentAtScale P 0 hP4.sLower hP4.xi)) + Ch04.rosenthalDescendantsAtScaleSqrtConst d 0 hP4.xi * √↑(descendantsAtScale (originCube d m) 0).card * (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| ∂P ≤ K ∧ ∫ (a : RegCoeffField d), |Ch04.restrictionCenteredDescendantAverage P 0 m (fullBlockNormalizedQuadraticObservableR hP hStruct center (fullBlockMinusProbe α β)) a| ^ 2 ∂P ≤ K ^ 2

L1/L2 descendant-average bounds for normalized minus-pair probes.