Documentation

LeanPool.HighContrastHomogenization.Support.Book.Ch05.Theorems.Section54.VarianceBoundGoodScale.ScaleAbsorption

Coarse-graining support: #

Support.Book.Ch05.Theorems.Section54.VarianceBoundGoodScale.ScaleAbsorption

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

Scale-separation absorption #

This file contains the pure real estimate converting the manuscript scale separation into the decay needed after the refined variance-budget summation.

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

A separation constant large enough to turn the logarithmic scale condition into fourth-power decay of the scale-zero moment parameter.

Equations
Instances For
    source
    theorem HCPolySupport.Book.Ch05.Section54.VarianceBoundGoodScale.scaleSeparation_absorbs_widetildeThetaBudget {d : ℕ} [NeZero d] {P : Ch04.RestrictionCoeffLaw d} (hP4 : QuantitativeCoarseGrainedEllipticity P) {C delta : ℝ} {m : ℕ} (hC : varianceScaleSeparationConst 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 (-section54VarianceBeta hP4 * ↑m) * (widetildeThetaAtScale P 0 hP4 + widetildeThetaAtScale P 0 hP4 ^ 2) ≤ 2 * delta

    Scale separation absorbs the remaining \widetilde\Theta_0 budget.