Documentation

LeanPool.HighContrastHomogenization.Support.Book.Ch05.Theorems.Section54.OneStepContraction.ScaleErrors

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

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

Scale-separation errors for the one-step contraction #

The Section 5.3 tail terms contain the square of widetildeTheta_0. This file records the Section 5.4 logarithmic absorption needed to make those tails small. Constants are intentionally harmless: the final theorem will absorb the numerical factors into its existential constant.

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

A scale-separation constant sufficient for the current one-step tail absorption.

Equations
  • One or more equations did not get rendered due to their size.
Instances For
    source
    theorem HCPolySupport.Book.Ch05.Section54.OneStepContraction.oneStepScaleSeparationConst_pos {d : ℕ} [NeZero d] {P : Ch04.RestrictionCoeffLaw d} (hP4 : QuantitativeCoarseGrainedEllipticity P) :
    0 < oneStepScaleSeparationConst hP4

    The one-step scale-separation constant is positive.

    source
    theorem HCPolySupport.Book.Ch05.Section54.OneStepContraction.oneStepScaleSeparation_absorbs_widetildeThetaSq {d : ℕ} [NeZero d] {P : Ch04.RestrictionCoeffLaw d} (hP4 : QuantitativeCoarseGrainedEllipticity P) {C delta : ℝ} {m : ℕ} (hC : oneStepScaleSeparationConst hP4 ≤ C) (hdelta_pos : 0 < delta) (hdelta_le_half : delta ≤ 1 / 2) (hm : C * ↑hP4.xi * Real.log (2 + delta⁻¹ * ↑hP4.xi * widetildeThetaAtScale P 0 hP4) ≤ ↑m) :
    Real.rpow 3 (-VarianceBoundGoodScale.section54VarianceBeta hP4 * ↑m) * widetildeThetaAtScale P 0 hP4 ^ 2 ≤ √delta

    The logarithmic scale separation absorbs the square of widetildeTheta_0.

    source
    theorem HCPolySupport.Book.Ch05.Section54.OneStepContraction.oneStepScaleSeparation_absorbs_section53Beta_widetildeThetaSq {d : ℕ} [NeZero d] {P : Ch04.RestrictionCoeffLaw d} (hP4 : QuantitativeCoarseGrainedEllipticity P) {C delta : ℝ} {m : ℕ} (hC : oneStepScaleSeparationConst hP4 ≤ C) (hdelta_pos : 0 < delta) (hdelta_le_half : delta ≤ 1 / 2) (hm : C * ↑hP4.xi * Real.log (2 + delta⁻¹ * ↑hP4.xi * widetildeThetaAtScale P 0 hP4) ≤ ↑m) :
    Real.rpow 3 (-Section53.JUpperBoundCoarseFluctuations.section53CoarseFluctuationBeta hP4 * ↑m) * widetildeThetaAtScale P 0 hP4 ^ 2 ≤ √delta

    The same logarithmic scale separation absorbs the Section 5.3-beta tail that appears in the final coarse-fluctuation RHS.

    source
    theorem HCPolySupport.Book.Ch05.Section54.OneStepContraction.oneStepScaleSeparation_absorbs_section53Beta_widetildeThetaBudget {d : ℕ} [NeZero d] {P : Ch04.RestrictionCoeffLaw d} (hP4 : QuantitativeCoarseGrainedEllipticity P) {C delta : ℝ} {m : ℕ} (hC : oneStepScaleSeparationConst hP4 ≤ C) (hdelta_pos : 0 < delta) (hdelta_le_half : delta ≤ 1 / 2) (hm : C * ↑hP4.xi * Real.log (2 + delta⁻¹ * ↑hP4.xi * widetildeThetaAtScale P 0 hP4) ≤ ↑m) :
    Real.rpow 3 (-Section53.JUpperBoundCoarseFluctuations.section53CoarseFluctuationBeta hP4 * ↑m) * (widetildeThetaAtScale P 0 hP4 + widetildeThetaAtScale P 0 hP4 ^ 2) ≤ 2 * √delta

    The same logarithmic scale separation absorbs both 3^{-βm} widetildeTheta_0 and 3^{-βm} widetildeTheta_0^2 for the Section 5.3 beta.