Documentation

LeanPool.HighContrastHomogenization.Support.Book.Ch05.Theorems.Section57.UniformEndpointDenominator

Coarse-graining support: Support.Book.Ch05.Theorems.Section57.UniformEndpointDenominator #

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

Denominator selection at the uniform endpoint #

The endpoint high-bottom branch needs the high denominator squared and the crude cutoff denominator to the power (d - 2t) / t. We deliberately choose a slightly oversized denominator, avoiding roots; the later scale-compression step absorbs this polynomial dependence into the exp(C log^2) envelope.

source
noncomputable def HCPolySupport.Book.Ch05.Section57.uniformEndpointHighDenominator (Dhigh Dcrude t d : ℝ) :
ℝ

Common high-branch denominator for the Γ∞ endpoint.

Equations
Instances For
    source
    theorem HCPolySupport.Book.Ch05.Section57.uniformEndpointHighDenominator_pos {Dhigh Dcrude t d : ℝ} :
    0 < uniformEndpointHighDenominator Dhigh Dcrude t d
    source
    theorem HCPolySupport.Book.Ch05.Section57.one_le_uniformEndpointHighDenominator {Dhigh Dcrude t d : ℝ} :
    1 ≤ uniformEndpointHighDenominator Dhigh Dcrude t d
    source
    theorem HCPolySupport.Book.Ch05.Section57.uniformEndpointHighDenominator_dom_bottom {Dhigh Dcrude t d : ℝ} (hd : 1 ≤ d) :
    Dhigh ^ 2 * max 1 Dcrude ^ ((d - 2 * t) / t) ≤ uniformEndpointHighDenominator Dhigh Dcrude t d ^ d
    source
    theorem HCPolySupport.Book.Ch05.Section57.uniformEndpointHighDenominator_dom_top {Dhigh Dcrude t d : ℝ} (hDhigh : 0 ≤ Dhigh) (ht : 0 < t) (htb : t ≤ d / 2) (hd : 1 ≤ d) :
    Dhigh ^ 2 ≤ uniformEndpointHighDenominator Dhigh Dcrude t d ^ d