High-contrast homogenization: Provider.Quenched.UnitRangeFiniteRangeDatum

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

The finite-range coarse-ellipticity datum

The Gaussian half of the quenched tail needs the stopping-radius family read against the Gaussian concentration gauge supplied by unit range of dependence rather than against the source gauge of e.coarse.ellipticity. Everything downstream of such a datum is already available; this file names the datum, shows what it delivers, and records why it is a genuine additional input rather than a consequence of the assumptions already carried.

The gauge of a coarse-ellipticity datum occurs in one clause only, the source tail. The other clauses are monotone in the source scale in the unfavourable direction: enlarging the source scale preserves the discounted Loewner bound but enlarges the upper-tail event, so it can only make the tail heavier. A datum at a stronger gauge carried by a larger source scale therefore forces the original source scale to satisfy the stronger tail already. That is the content of the source-tail bound below, and it is why the finite-range datum is carried here as a named hypothesis instead of being derived.

Monotonicity of the two clauses in the source scale

theorem HCPolySupport.HighContrast.Quenched.coarseBound_of_source_le {d : ℕ} {P : MeasureTheory.Measure (CoeffSpace d)} {g : ℝ} {E : BlockMat d} {Psi : ℝ → ℝ} {K : ℝ} {S S' : CoeffSpace d → ℝ} (hdag : CoarseEllipticityDagger P g E Psi K S) (hle : ∀ (a : CoeffSpace d), S a ≤ S' a) : ∀ᵐ (a : CoeffSpace d) ∂P, ∀ (m : ℤ), S' a ≤ 3 ^ m → ∀ k ≤ m, ∀ (w : Fin d → ℤ), standardCellCenter k w ∈ centeredCube d m → BlockMatLoewnerLE (coarseBlock (standardCell d k w) a) (blockScale (3 ^ (g * (↑m - ↑k))) E)

The discounted Loewner bound is monotone in the source scale. Enlarging the source scale shrinks the event on which the bound is asserted, so the bound is inherited.

theorem HCPolySupport.HighContrast.Quenched.coarseEllipticityDagger_of_source_le {d : ℕ} {P : MeasureTheory.Measure (CoeffSpace d)} {g : ℝ} {E : BlockMat d} {Psi Psi' : ℝ → ℝ} {K K' : ℝ} {S S' : CoeffSpace d → ℝ} (hdag : CoarseEllipticityDagger P g E Psi K S) (hle : ∀ (a : CoeffSpace d), S a ≤ S' a) (hmeas : Measurable S') (hnonneg : ∀ (a : CoeffSpace d), 0 ≤ S' a) (hadm : IndependentSums.AdmissiblePsi Psi') (hK' : 1 < K') (hgrowth : IndependentSums.HasPsiGrowth Psi' K') (htail : ∀ (t : ℝ), 0 < t → P.real (IndependentSums.upperTailEvent S' t) ≤ (Psi' t)⁻¹) : CoarseEllipticityDagger P g E Psi' K' S'

The gauge-change interface. A coarse-ellipticity datum may be re-read against any admissible gauge, at any source scale at least the original one, once that scale's tail against the new gauge is supplied. The tail is the only clause that has to be re-proved.

Why the finite-range datum is an additional input

The named datum and what it delivers