Coarse-graining support:

Support.Book.Ch05.Theorems.Section54.VarianceBoundGoodScale.ScalarVariance

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

Scalar variance estimates for the good-scale proof

This file combines the good-scale positive-part comparison, the P4 integrability bridges, and the Rosenthal descendant-average bounds into the per-probe scalar variance estimates used by the finite-dimensional upgrade.

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

The descendant-average bound produced by Rosenthal for a coordinate probe.

Equations

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

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

The descendant-average bound produced by Rosenthal for a plus/minus pair probe.

Equations

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

theorem HCPolySupport.Book.Ch05.Section54.VarianceBoundGoodScale.fullBlockNormalizedQuadraticObservable_scalarVariance_good_origin_le {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 : ℕ) (hj : j ≤ 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) {K : ℝ} (hZ_int : MeasureTheory.Integrable (fun (a : RegCoeffField d) => |Ch04.restrictionCenteredDescendantAverage P 0 (↑j) (fullBlockNormalizedQuadraticObservableR hP hStruct (↑m) q) a|) P ∧ MeasureTheory.Integrable (fun (a : RegCoeffField d) => |Ch04.restrictionCenteredDescendantAverage P 0 (↑j) (fullBlockNormalizedQuadraticObservableR hP hStruct (↑m) q) a| ^ 2) P) (hZ_le : ∫ (a : RegCoeffField d), |Ch04.restrictionCenteredDescendantAverage P 0 (↑j) (fullBlockNormalizedQuadraticObservableR hP hStruct (↑m) q) a| ∂P ≤ K ∧ ∫ (a : RegCoeffField d), |Ch04.restrictionCenteredDescendantAverage P 0 (↑j) (fullBlockNormalizedQuadraticObservableR hP hStruct (↑m) q) a| ^ 2 ∂P ≤ K ^ 2) : ∫ (a : RegCoeffField d), |normalizedQuadraticObservable hP hStruct (↑m) q (cubeSet (originCube d ↑j)) a.toFun - q ⬝ᵥ q| ^ 2 ∂P ≤ 4 * (delta * q ⬝ᵥ q) ^ 2 + 4 * K ^ 2 + 2 * q ⬝ᵥ q * (delta * q ⬝ᵥ q + K)

Scalar variance estimate for a single normalized quadratic probe, assuming the descendant average has already been bounded in L1 and L2.

theorem HCPolySupport.Book.Ch05.Section54.VarianceBoundGoodScale.coordinateProbe_scalarVariance_good_origin_le {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 : ℕ) (hj : j ≤ 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)⁻¹) (α : BlockCoord d) : have K := coordinateProbeDescendantAverageK hP hStruct hP4 (↑m) (↑j) α; ∫ (a : RegCoeffField d), |normalizedQuadraticObservable hP hStruct (↑m) (fullBlockCoordinateProbe α) (cubeSet (originCube d ↑j)) a.toFun - fullBlockCoordinateProbe α ⬝ᵥ fullBlockCoordinateProbe α| ^ 2 ∂P ≤ 4 * (delta * fullBlockCoordinateProbe α ⬝ᵥ fullBlockCoordinateProbe α) ^ 2 + 4 * K ^ 2 + 2 * fullBlockCoordinateProbe α ⬝ᵥ fullBlockCoordinateProbe α * (delta * fullBlockCoordinateProbe α ⬝ᵥ fullBlockCoordinateProbe α + K)

Coordinate-probe scalar variance estimate at a good scale.

theorem HCPolySupport.Book.Ch05.Section54.VarianceBoundGoodScale.plusProbe_scalarVariance_good_origin_le {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 : ℕ) (hj : j ≤ 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)⁻¹) {α β : BlockCoord d} (hαβ : α ≠ β) : have K := pairProbeDescendantAverageK hP hStruct hP4 (↑m) (↑j) α β; ∫ (a : RegCoeffField d), |normalizedQuadraticObservable hP hStruct (↑m) (fullBlockPlusProbe α β) (cubeSet (originCube d ↑j)) a.toFun - fullBlockPlusProbe α β ⬝ᵥ fullBlockPlusProbe α β| ^ 2 ∂P ≤ 4 * (delta * fullBlockPlusProbe α β ⬝ᵥ fullBlockPlusProbe α β) ^ 2 + 4 * K ^ 2 + 2 * fullBlockPlusProbe α β ⬝ᵥ fullBlockPlusProbe α β * (delta * fullBlockPlusProbe α β ⬝ᵥ fullBlockPlusProbe α β + K)

Plus-pair scalar variance estimate at a good scale.

theorem HCPolySupport.Book.Ch05.Section54.VarianceBoundGoodScale.minusProbe_scalarVariance_good_origin_le {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 : ℕ) (hj : j ≤ 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)⁻¹) {α β : BlockCoord d} (hαβ : α ≠ β) : have K := pairProbeDescendantAverageK hP hStruct hP4 (↑m) (↑j) α β; ∫ (a : RegCoeffField d), |normalizedQuadraticObservable hP hStruct (↑m) (fullBlockMinusProbe α β) (cubeSet (originCube d ↑j)) a.toFun - fullBlockMinusProbe α β ⬝ᵥ fullBlockMinusProbe α β| ^ 2 ∂P ≤ 4 * (delta * fullBlockMinusProbe α β ⬝ᵥ fullBlockMinusProbe α β) ^ 2 + 4 * K ^ 2 + 2 * fullBlockMinusProbe α β ⬝ᵥ fullBlockMinusProbe α β * (delta * fullBlockMinusProbe α β ⬝ᵥ fullBlockMinusProbe α β + K)

Minus-pair scalar variance estimate at a good scale.