Coarse-graining support:

Support.Book.Ch05.Theorems.Section54.VarianceBoundGoodScale.RefinedScalarVariance

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

Refined scalar variance estimates

This file reuses the scalar positive-part reduction from ScalarVariance, but feeds it the sharper good-scale Rosenthal inputs from RefinedProbeMoments. The resulting descendant-average budgets are expressed in terms of \widetilde\Theta_0.

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

Refined descendant-average budget for coordinate probes.

Equations

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

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

Refined descendant-average budget for plus/minus pair probes.

Equations

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

noncomputable def HCPolySupport.Book.Ch05.Section54.VarianceBoundGoodScale.refinedScalarProbeVarianceBound {d : ℕ} (delta : ℝ) (q : FullBlockVec d) (K : ℝ) : ℝ

Scalar variance budget for a single probe and refined descendant-average budget K.

Equations

• HCPolySupport.Book.Ch05.Section54.VarianceBoundGoodScale.refinedScalarProbeVarianceBound delta q K = 4 * (delta * q ⬝ᵥ q) ^ 2 + 4 * K ^ 2 + 2 * q ⬝ᵥ q * (delta * q ⬝ᵥ q + K)

theorem HCPolySupport.Book.Ch05.Section54.VarianceBoundGoodScale.coordinateProbe_restrictionCenteredDescendantAverage_abs_and_sq_le_refined {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)⁻¹) (α : BlockCoord d) : have K := coordinateProbeRefinedDescendantAverageK hP4 delta j; ∫ (a : RegCoeffField d), |Ch04.restrictionCenteredDescendantAverage P 0 (↑j) (fullBlockNormalizedQuadraticObservableR hP hStruct (↑m) (fullBlockCoordinateProbe α)) a| ∂P ≤ K ∧ ∫ (a : RegCoeffField d), |Ch04.restrictionCenteredDescendantAverage P 0 (↑j) (fullBlockNormalizedQuadraticObservableR hP hStruct (↑m) (fullBlockCoordinateProbe α)) a| ^ 2 ∂P ≤ K ^ 2

L1/L2 descendant-average bounds for coordinate probes with the refined good-scale moment budget.

theorem HCPolySupport.Book.Ch05.Section54.VarianceBoundGoodScale.plusProbe_restrictionCenteredDescendantAverage_abs_and_sq_le_refined {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)⁻¹) {α β : BlockCoord d} (hαβ : α ≠ β) : have K := pairProbeRefinedDescendantAverageK hP4 delta j; ∫ (a : RegCoeffField d), |Ch04.restrictionCenteredDescendantAverage P 0 (↑j) (fullBlockNormalizedQuadraticObservableR hP hStruct (↑m) (fullBlockPlusProbe α β)) a| ∂P ≤ K ∧ ∫ (a : RegCoeffField d), |Ch04.restrictionCenteredDescendantAverage P 0 (↑j) (fullBlockNormalizedQuadraticObservableR hP hStruct (↑m) (fullBlockPlusProbe α β)) a| ^ 2 ∂P ≤ K ^ 2

L1/L2 descendant-average bounds for plus probes with the refined good-scale moment budget.

theorem HCPolySupport.Book.Ch05.Section54.VarianceBoundGoodScale.minusProbe_restrictionCenteredDescendantAverage_abs_and_sq_le_refined {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)⁻¹) {α β : BlockCoord d} (hαβ : α ≠ β) : have K := pairProbeRefinedDescendantAverageK hP4 delta j; ∫ (a : RegCoeffField d), |Ch04.restrictionCenteredDescendantAverage P 0 (↑j) (fullBlockNormalizedQuadraticObservableR hP hStruct (↑m) (fullBlockMinusProbe α β)) a| ∂P ≤ K ∧ ∫ (a : RegCoeffField d), |Ch04.restrictionCenteredDescendantAverage P 0 (↑j) (fullBlockNormalizedQuadraticObservableR hP hStruct (↑m) (fullBlockMinusProbe α β)) a| ^ 2 ∂P ≤ K ^ 2

L1/L2 descendant-average bounds for minus probes with the refined good-scale moment budget.

theorem HCPolySupport.Book.Ch05.Section54.VarianceBoundGoodScale.coordinateProbe_scalarVariance_good_origin_le_refined {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 := coordinateProbeRefinedDescendantAverageK hP4 delta j; ∫ (a : RegCoeffField d), |normalizedQuadraticObservable hP hStruct (↑m) (fullBlockCoordinateProbe α) (cubeSet (originCube d ↑j)) a.toFun - fullBlockCoordinateProbe α ⬝ᵥ fullBlockCoordinateProbe α| ^ 2 ∂P ≤ refinedScalarProbeVarianceBound delta (fullBlockCoordinateProbe α) K

Coordinate-probe scalar variance estimate using the refined descendant average budget.

theorem HCPolySupport.Book.Ch05.Section54.VarianceBoundGoodScale.plusProbe_scalarVariance_good_origin_le_refined {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 := pairProbeRefinedDescendantAverageK hP4 delta j; ∫ (a : RegCoeffField d), |normalizedQuadraticObservable hP hStruct (↑m) (fullBlockPlusProbe α β) (cubeSet (originCube d ↑j)) a.toFun - fullBlockPlusProbe α β ⬝ᵥ fullBlockPlusProbe α β| ^ 2 ∂P ≤ refinedScalarProbeVarianceBound delta (fullBlockPlusProbe α β) K

Plus-probe scalar variance estimate using the refined descendant-average budget.

theorem HCPolySupport.Book.Ch05.Section54.VarianceBoundGoodScale.minusProbe_scalarVariance_good_origin_le_refined {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 := pairProbeRefinedDescendantAverageK hP4 delta j; ∫ (a : RegCoeffField d), |normalizedQuadraticObservable hP hStruct (↑m) (fullBlockMinusProbe α β) (cubeSet (originCube d ↑j)) a.toFun - fullBlockMinusProbe α β ⬝ᵥ fullBlockMinusProbe α β| ^ 2 ∂P ≤ refinedScalarProbeVarianceBound delta (fullBlockMinusProbe α β) K

Minus-probe scalar variance estimate using the refined descendant-average budget.