Coarse-graining support:

Support.Book.Ch05.Theorems.Section54.VarianceBoundGoodScale.RefinedAssembly

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

Refined matrix assembly

This file plugs the refined scalar probe estimates into the finite-dimensional matrix upgrade. The per-scale budget is now expressed in terms of delta and \widetilde\Theta_0.

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

Refined coordinate-probe scalar variance budget at scale j.

Equations

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

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

Refined plus-pair scalar variance budget at scale j.

Equations

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

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

Refined minus-pair scalar variance budget at scale j.

Equations

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

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

Refined finite-probe matrix variance budget at one scale.

Equations

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

theorem HCPolySupport.Book.Ch05.Section54.VarianceBoundGoodScale.fluctuationNormSq_integral_le_refinedMatrixVarianceBound {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)⁻¹) : ∫ (a : RegCoeffField d), Ch04.fullBlockNormalizedFluctuationOperatorNormSqAtScale hP hStruct (↑m) (originCube d ↑j) a ∂P ≤ refinedMatrixVarianceScaleBound hP4 delta j

Per-scale matrix variance bound using the refined scalar probe estimates.

theorem HCPolySupport.Book.Ch05.Section54.VarianceBoundGoodScale.varianceGoodScaleFullBlockSumAtScale_le_weighted_refinedMatrixVarianceScaleBound {d : ℕ} [NeZero d] {P : Ch04.RestrictionCoeffLaw d} (hP : Ch04.RestrictionLawCarrier P) (hStruct : Ch04.RestrictionStructuralLaw P) (hP4 : QuantitativeCoarseGrainedEllipticity P) {delta : ℝ} (hdelta_nonneg : 0 ≤ delta) (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)⁻¹) : varianceGoodScaleFullBlockSumAtScale hP hStruct hP4 m ≤ ∑ j ∈ Finset.Icc 1 m, varianceWeight (section54VarianceBeta hP4) m j * refinedMatrixVarianceScaleBound hP4 delta j

The variance sum is bounded by the beta-weighted refined per-scale budgets.