High-contrast homogenization: Provider.Quenched.SmallContrastThresholdPolynomial

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

The thresholds are polynomial

The near-reference comparison confines the reference aspect ratio to two scale thresholds; the binder's sanctioned Π-slot is 3^{m_0} ≤ (2 + Π·K)^{C_delay}, so what must be checked is that three raised to each threshold is polynomial in the data. Both are, and both by the same elementary bound 3^{max 1 ⌈y⌉} ≤ 3·max 1 (3^y):

• 3^{euclideanEntryThreshold K cEnt sK} ≤ 3^{sK}·3·max 1 (M₂(K)/cEnt) — linear in the second source moment, i.e. polynomial in K_bar_S; this is's first input, which the rework was predicted to shrink, and it does;
• 3^{tiltGap Cd g cEnt nu G} ≤ 3·max 1 ((2·boundaryConst·3^{gG}/cEnt)^{1/(1-g)}) — and at the fusion's binding nu = canonicalMetric 𝐄, G = canonicalGridEnlargement d Π, the base is polynomial in Π by witnessEccentricity_canonicalMetric_le_aspectRatio, so the whole gap is. The exponent 1/(1-g) is the printed (1-γ)^{-1}.

The elementary ceiling bound

theorem HCPolySupport.HighContrast.Quenched.three_zpow_max_one_intCeil_le (y : ℝ) : 3 ^ max 1 ⌈y⌉ ≤ 3 * max 1 (3 ^ y)

The ceiling bound. 3^{max 1 ⌈y⌉} ≤ 3·max 1 (3^y): the integer-ceiling analogue of three_pow_ceil_logb_le, which the two thresholds share.

The Euclidean entry threshold

theorem HCPolySupport.HighContrast.Quenched.three_zpow_euclideanEntryThreshold_le {K cEnt : ℝ} (hcEnt : 0 < cEnt) (sK : ℤ) : 3 ^ euclideanEntryThreshold K cEnt sK ≤ 3 ^ sK * (3 * max 1 (sourceMomentTwo K / cEnt))

's first input, at the rework's threshold. Three raised to the Euclidean entry threshold is linear in the second source moment.

The tilt gap

theorem HCPolySupport.HighContrast.Quenched.three_zpow_tiltGap_le {d : ℕ} {Cd g cEnt : ℝ} (hg : g ∈ Set.Ico 0 1) (hcEnt : 0 < cEnt) {nu : Mat d} (hbase : 0 < boundaryConst Cd g nu) (G : ℕ) : 3 ^ tiltGap Cd g cEnt nu G ≤ 3 * max 1 ((2 * boundaryConst Cd g nu * 3 ^ (g * ↑G) / cEnt) ^ (1 - g)⁻¹)

Three raised to the tilt gap is polynomial in the boundary envelope, with the printed (1-γ)^{-1} as the exponent.

The tilt gap at the fusion's binding is polynomial in Π

theorem HCPolySupport.HighContrast.Quenched.one_le_aspectRatio_of_coarseEllipticityDagger {d : ℕ} [NeZero d] {P : MeasureTheory.Measure (CoeffSpace d)} [MeasureTheory.IsProbabilityMeasure P] {g : ℝ} {E : BlockMat d} {Ψ : ℝ → ℝ} {K : ℝ} {S : CoeffSpace d → ℝ} (hdag : CoarseEllipticityDagger P g E Ψ K S) : 1 ≤ aspectRatio E

The reference aspect ratio is at least one at a coarse-ellipticity reference.