High-contrast homogenization: Provider.Quenched.UnitRangePoweredGauge

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

The powered finite-range gauge

The window mechanism reads the tail of a coarse-ellipticity datum against the μ-powered Gaussian exp(c t^(2μ)), μ = d/2 - g, rather than against the Gaussian itself. This file records the corresponding powered form of the finite-range gauge supplied by unit range of dependence,

Ψ_fr^{(μ)}(t) = exp(c_fr(d) t^(2μ)),

together with the two properties a gauge must have before it can appear in a coarse-ellipticity datum: admissibility and the growth inequality, the latter at a growth witness depending on the dimension and on μ alone. Reading the stopping-radius provider against this gauge makes its domination premise an identity, so the shifted tail the bad-tail engine consumes holds with the dimensional constant c_fr(d).

The gauge and its witness

noncomputable def HCPolySupport.HighContrast.Quenched.frPoweredGauge (d : ℕ) (mu : ℝ) : ℝ → ℝ

The μ-powered finite-range gauge Ψ_fr^{(μ)}(t) = exp(c_fr(d) t^(2μ)).

Equations

• HCPolySupport.HighContrast.Quenched.frPoweredGauge d mu t = Real.exp (HCPolySupport.HighContrast.Quenched.frGaugeConst d * t ^ (2 * mu))

noncomputable def HCPolySupport.HighContrast.Quenched.frPoweredGrowthWitness (d : ℕ) (mu : ℝ) : ℝ

A growth witness for the powered finite-range gauge, depending on the dimension and on μ alone.

Equations

• HCPolySupport.HighContrast.Quenched.frPoweredGrowthWitness d mu = 3 + (1 + (2 * mu * HCPolySupport.HighContrast.Quenched.frGaugeConst d)⁻¹) ^ (2 * mu)⁻¹

Admissibility

theorem HCPolySupport.HighContrast.Quenched.admissiblePsi_frPoweredGauge (d : ℕ) {mu : ℝ} (hmu : 0 < mu) : IndependentSums.AdmissiblePsi (frPoweredGauge d mu)

theorem HCPolySupport.HighContrast.Quenched.three_le_frPoweredGrowthWitness (d : ℕ) {mu : ℝ} (hmu : 0 < mu) : 3 ≤ frPoweredGrowthWitness d mu

The growth inequality

theorem HCPolySupport.HighContrast.Quenched.le_frPoweredGrowthWitness_rpow (d : ℕ) {mu : ℝ} (hmu : 0 < mu) : 1 + (2 * mu * frGaugeConst d)⁻¹ ≤ frPoweredGrowthWitness d mu ^ (2 * mu)

The growth witness dominates the reciprocal of the gauge constant after raising to the power 2μ. This is the only property of the witness the growth inequality uses.

theorem HCPolySupport.HighContrast.Quenched.hasPsiGrowth_frPoweredGauge (d : ℕ) {mu : ℝ} (hmu : 0 < mu) : IndependentSums.HasPsiGrowth (frPoweredGauge d mu) (frPoweredGrowthWitness d mu)

The domination premise is an identity