Documentation

LeanPool.HighContrastHomogenization.Entry.Multiscale.SelectionExponentBounds

High-contrast homogenization: Entry.Multiscale.SelectionExponentBounds #

Imported from the Apache-2.0 HighContrastHomogenization development at commit 7a13dbcd8d6609264a713373f5c69ceeac870472.

Bounds for the fixed selection exponents #

On the standing range γ ∈ [0,1) the fixed moment Q = 2⌈2(d+1)/(1-γ)⌉ is even, at least 2 and positive, and the fixed exponent ρ_max = γ + (1/Q)(d + ¼(1-γ)) satisfies γ ≤ ρ_max < 1. The identity ρ_max - d/Q = γ + (1-γ)/(4Q) puts the fluctuation decay exponent d/2 - (1-γ)/(4Q) strictly above 0. The same data give the moment order 2(d + Q) of the source multiplier tail: it is at least 1, and each of the two geometric tails retains the margin d + Q.

These are the arithmetic inputs of the scale-selection alternatives p.scale.selection and of the source multiplier tail e.source.multiplier.

source
theorem HCPolySupport.HighContrast.Multiscale.bigQ_even (d : ℕ) (γ : ℝ) :
Even (bigQ d γ)
source
theorem HCPolySupport.HighContrast.Multiscale.bigQ_two_le (d : ℕ) (γ : ℝ) (hγ : γ ∈ Set.Ico 0 1) :
2 ≤ bigQ d γ
source
theorem HCPolySupport.HighContrast.Multiscale.bigQ_pos (d : ℕ) (γ : ℝ) (hγ : γ ∈ Set.Ico 0 1) :
0 < bigQ d γ
source
theorem HCPolySupport.HighContrast.Multiscale.bigQ_ne_zero (d : ℕ) (_hd : 2 ≤ d) (γ : ℝ) (hγ : γ ∈ Set.Ico 0 1) :
bigQ d γ ≠ 0
source
theorem HCPolySupport.HighContrast.Multiscale.bigQ_real_pos (d : ℕ) (γ : ℝ) (hγ : γ ∈ Set.Ico 0 1) :
0 < ↑(bigQ d γ)
source
theorem HCPolySupport.HighContrast.Multiscale.bigQ_mul_one_sub_ge (d : ℕ) (hd : 2 ≤ d) (γ : ℝ) (hγ : γ ∈ Set.Ico 0 1) :
4 * (↑d + 1) ≤ ↑(bigQ d γ) * (1 - γ)
source
theorem HCPolySupport.HighContrast.Multiscale.rhoMax_lt_one (d : ℕ) (hd : 2 ≤ d) (γ : ℝ) (hγ : γ ∈ Set.Ico 0 1) :
rhoMax d γ < 1
source
theorem HCPolySupport.HighContrast.Multiscale.gamma_le_rhoMax (d : ℕ) (hd : 2 ≤ d) (γ : ℝ) (hγ : γ ∈ Set.Ico 0 1) :
γ ≤ rhoMax d γ
source
theorem HCPolySupport.HighContrast.Multiscale.rhoMax_sub_d_div_bigQ (d : ℕ) (_hd : 2 ≤ d) (γ : ℝ) (hγ : γ ∈ Set.Ico 0 1) :
rhoMax d γ - ↑d / ↑(bigQ d γ) = γ + (1 - γ) / (4 * ↑(bigQ d γ))
source
theorem HCPolySupport.HighContrast.Multiscale.fluctuation_decay_exponent_pos (d : ℕ) (hd : 2 ≤ d) (γ : ℝ) (hγ : γ ∈ Set.Ico 0 1) :
0 < ↑d / 2 - (1 - γ) / (4 * ↑(bigQ d γ))
source
noncomputable def HCPolySupport.HighContrast.Multiscale.sourceMomentExponent (d : ℕ) (γ : ℝ) :
ℕ

The moment order used in the source multiplier tail estimate.

Equations
Instances For
    source
    theorem HCPolySupport.HighContrast.Multiscale.sourceMomentExponent_ge_one (d : ℕ) (hd : 2 ≤ d) (γ : ℝ) (_hγ : γ ∈ Set.Ico 0 1) :
    1 ≤ sourceMomentExponent d γ
    source
    theorem HCPolySupport.HighContrast.Multiscale.sourceMomentExponent_tail_margins (d : ℕ) (_hd : 2 ≤ d) (γ : ℝ) (hγ : γ ∈ Set.Ico 0 1) :
    ↑d + ↑(bigQ d γ) ≤ ↑(sourceMomentExponent d γ) - ↑d ∧ ↑d + ↑(bigQ d γ) ≤ ↑(sourceMomentExponent d γ) - ↑(bigQ d γ) * γ

    Explicit margins for the two geometric tails in the argument for e.source.multiplier.