Coarse-graining support: Support.Book.Ch05.Theorems.Section54.OneStepContraction.CoarseFullBlock

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

Section 5.3-beta full-block fluctuation sums

The public variance lemma uses the Section 5.4 beta. The Section 5.3 coarse-fluctuation RHS uses the slower quarter-beta, so the one-step proof needs the same refined budget argument with that beta.

noncomputable def HCPolySupport.Book.Ch05.Section54.OneStepContraction.oneStepCoarsePairLinearBudgetConst {d : ℕ} [NeZero d] {P : Ch04.RestrictionCoeffLaw d} (hP4 : QuantitativeCoarseGrainedEllipticity P) : ℝ

Linear constant for refined pair budgets summed with the Section 5.3 beta.

Equations

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

theorem HCPolySupport.Book.Ch05.Section54.OneStepContraction.oneStepCoarsePairLinearBudgetConst_nonneg {d : ℕ} [NeZero d] {P : Ch04.RestrictionCoeffLaw d} (hP4 : QuantitativeCoarseGrainedEllipticity P) : 0 ≤ oneStepCoarsePairLinearBudgetConst hP4

theorem HCPolySupport.Book.Ch05.Section54.OneStepContraction.pairPointwiseBudgetConst_nonneg {d : ℕ} [NeZero d] {P : Ch04.RestrictionCoeffLaw d} (hP4 : QuantitativeCoarseGrainedEllipticity P) : 0 ≤ VarianceBoundGoodScale.pairPointwiseBudgetConst hP4

noncomputable def HCPolySupport.Book.Ch05.Section54.OneStepContraction.oneStepWeightedRefinedBudgetConst {d : ℕ} [NeZero d] {P : Ch04.RestrictionCoeffLaw d} (hP4 : QuantitativeCoarseGrainedEllipticity P) : ℝ

Constant controlling the Section 5.3-beta refined scalar budget.

Equations

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

theorem HCPolySupport.Book.Ch05.Section54.OneStepContraction.oneStepWeightedRefinedBudgetConst_nonneg {d : ℕ} [NeZero d] {P : Ch04.RestrictionCoeffLaw d} (hP4 : QuantitativeCoarseGrainedEllipticity P) : 0 ≤ oneStepWeightedRefinedBudgetConst hP4

The Section 5.3-beta refined scalar budget constant is nonnegative.

noncomputable def HCPolySupport.Book.Ch05.Section54.OneStepContraction.oneStepCoarseFullBlockConst {d : ℕ} [NeZero d] {P : Ch04.RestrictionCoeffLaw d} (hP4 : QuantitativeCoarseGrainedEllipticity P) : ℝ

Final constant for the Section 5.3-beta full-block fluctuation sum.

Equations

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

theorem HCPolySupport.Book.Ch05.Section54.OneStepContraction.oneStepCoarseFullBlockConst_nonneg {d : ℕ} [NeZero d] {P : Ch04.RestrictionCoeffLaw d} (hP4 : QuantitativeCoarseGrainedEllipticity P) : 0 ≤ oneStepCoarseFullBlockConst hP4

theorem HCPolySupport.Book.Ch05.Section54.OneStepContraction.sum_Icc_varianceWeight_mul_pairProbeRefinedK_le_section53 {d : ℕ} [NeZero d] {P : Ch04.RestrictionCoeffLaw d} (hP4 : QuantitativeCoarseGrainedEllipticity P) {delta : ℝ} (hdelta_le_half : delta ≤ 1 / 2) (m : ℕ) : ∑ j ∈ Finset.Icc 1 m, VarianceBoundGoodScale.varianceWeight (Section53.JUpperBoundCoarseFluctuations.section53CoarseFluctuationBeta hP4) m j * VarianceBoundGoodScale.pairProbeRefinedDescendantAverageK hP4 delta j ≤ oneStepCoarsePairLinearBudgetConst hP4 * widetildeThetaAtScale P 0 hP4 * Real.rpow 3 (-Section53.JUpperBoundCoarseFluctuations.section53CoarseFluctuationBeta hP4 * ↑m)

theorem HCPolySupport.Book.Ch05.Section54.OneStepContraction.sum_Icc_varianceWeight_mul_pairProbeRefinedK_sq_le_section53 {d : ℕ} [NeZero d] {P : Ch04.RestrictionCoeffLaw d} (hP4 : QuantitativeCoarseGrainedEllipticity P) {delta : ℝ} (hdelta_nonneg : 0 ≤ delta) (hdelta_le_half : delta ≤ 1 / 2) (m : ℕ) : ∑ j ∈ Finset.Icc 1 m, VarianceBoundGoodScale.varianceWeight (Section53.JUpperBoundCoarseFluctuations.section53CoarseFluctuationBeta hP4) m j * VarianceBoundGoodScale.pairProbeRefinedDescendantAverageK hP4 delta j ^ 2 ≤ VarianceBoundGoodScale.pairPointwiseBudgetConst hP4 * oneStepCoarsePairLinearBudgetConst hP4 * widetildeThetaAtScale P 0 hP4 ^ 2 * Real.rpow 3 (-Section53.JUpperBoundCoarseFluctuations.section53CoarseFluctuationBeta hP4 * ↑m)

theorem HCPolySupport.Book.Ch05.Section54.OneStepContraction.oneStepCoarseFullBlockSumAtScale_le_budget {d : ℕ} [NeZero d] {P : Ch04.RestrictionCoeffLaw d} (hP : Ch04.RestrictionLawCarrier P) (hStruct : Ch04.RestrictionStructuralLaw P) (hP4 : QuantitativeCoarseGrainedEllipticity P) {delta : ℝ} (hdelta_pos : 0 < delta) (hdelta_le_half : delta ≤ 1 / 2) (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)⁻¹) : oneStepCoarseFullBlockSumAtScale hP hStruct hP4 m ≤ VarianceBoundGoodScale.refinedMatrixBudgetConst d * (oneStepWeightedRefinedBudgetConst hP4 * (delta + Real.rpow 3 (-Section53.JUpperBoundCoarseFluctuations.section53CoarseFluctuationBeta hP4 * ↑m) * (widetildeThetaAtScale P 0 hP4 + widetildeThetaAtScale P 0 hP4 ^ 2)))

The Section 5.3-beta full-block fluctuation sum is controlled by the refined scalar budget at a good scale.

theorem HCPolySupport.Book.Ch05.Section54.OneStepContraction.oneStepCoarseFullBlockSumAtScale_le_sqrt_delta {d : ℕ} [NeZero d] {P : Ch04.RestrictionCoeffLaw d} (hP : Ch04.RestrictionLawCarrier P) (hStruct : Ch04.RestrictionStructuralLaw P) (hP4 : QuantitativeCoarseGrainedEllipticity P) {C delta : ℝ} {m : ℕ} (hC : oneStepScaleSeparationConst hP4 ≤ C) (hdelta_pos : 0 < delta) (hdelta_le_half : delta ≤ 1 / 2) (hsep : C * ↑hP4.xi * Real.log (2 + delta⁻¹ * ↑hP4.xi * widetildeThetaAtScale P 0 hP4) ≤ ↑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)⁻¹) : oneStepCoarseFullBlockSumAtScale hP hStruct hP4 m ≤ oneStepCoarseFullBlockConst hP4 * √delta

Under the one-step logarithmic scale separation, the Section 5.3-beta full-block fluctuation sum is O(sqrt(delta)).