High-contrast homogenization: Provider.Entry.AdapterMajorant

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

The crude majorant of the adapted-to-Euclidean comparison

The comparison between adapted and Euclidean cubes fills a target cell with the cells of the other grid and reads the resulting rows. The rows of a finite range of scales carry the printed estimate; what remains is the tail of scales below any cutoff, and the printed proof lets the cutoff descend. The exhaustion of l.two.grid.whitney is consumed against a majorant valid for every partial sum, so the tail has to be paid pathwise, by an estimate that is crude in its constant but summable in the scale.

Two ingredients do that.

The widened cell bound. e.coarse.ellipticity discounts a standard cube by 3^{g(m-k)} only when the cube's centre lies in the macroscopic cube □_m. The cubes of a filling lie wherever the target lies, so the bound of StandardCellMean — which reads at centres in the unit cube — is widened here to centres in □_M at any generation M: the same argument at the macroscopic scale max{M, k+l} gives 𝐀(z+□_k) ≤ (1 + (3^M + 3S)3^{-k})^g𝐄.

The tail series. Weighted by the cross-grid row 3^{r-n} that e.two.grid.whitney.volumes supplies, those bounds sum below a cutoff J to 2(1-g)^{-1}(3^J+3^M+3S)3^{-n}3^{J(1-g)}, which is affine in the source scale — so its mean is the source moment — and tends to zero as the cutoff descends. The cutoff is then chosen once and for all by the archimedean step on 3^{J(1-g)}; no limit is taken. The printed gauge Γ_{g,S} is compared with the geometric series it is built from at the end of the file.

There are no definitions in this file.

A macroscopic cube containing a target cell

theorem HCPolySupport.HighContrast.Entry.exists_containing_centeredCube {d : ℕ} {q : Mat d} (hq : Matrix.PosDef q) (n : ℤ) (y : Vec d) : ∃ (M : ℤ), 1 ≤ M ∧ adaptedCellTranslate q n y ⊆ centeredCube d M

Every adapted cell sits inside a macroscopic cube. A translated adapted cell is a bounded domain, and a triadic generation above its bound encloses it.

The widened cell bound

theorem HCPolySupport.HighContrast.Entry.ae_coarseBlock_standardCell_le_of_mem {d : ℕ} {P : MeasureTheory.Measure (CoeffSpace d)} {g : ℝ} {E : BlockMat d} {Ψ : ℝ → ℝ} {K : ℝ} {S : CoeffSpace d → ℝ} (hdag : CoarseEllipticityDagger P g E Ψ K S) (M : ℤ) : ∀ᵐ (a : CoeffSpace d) ∂P, ∀ (k : ℤ) (v : Fin d → ℤ), standardCellCenter k v ∈ centeredCube d M → BlockMatLoewnerLE (coarseBlock (standardCell d k v) a) (blockScale ((1 + (3 ^ M + 3 * S a) * 3 ^ (-k)) ^ g) E)

The Euclidean cell bound at a centre in a macroscopic cube. The random-source ellipticity of e.coarse.ellipticity, read at the macroscopic generation max{M, k+l} where 3^l brackets 3^{-k}S: a standard aligned cube whose centre lies in □_M is inside every macroscopic cube of generation at least M, so only the fixed generation M — not the target's own — is paid. The bound holds simultaneously at every cube, the ellipticity being one almost-sure statement quantified over all of them.

theorem HCPolySupport.HighContrast.Entry.ae_coarseBlock_standardCell_le_of_subset {d : ℕ} {P : MeasureTheory.Measure (CoeffSpace d)} {g : ℝ} {E : BlockMat d} {Ψ : ℝ → ℝ} {K : ℝ} {S : CoeffSpace d → ℝ} (hdag : CoarseEllipticityDagger P g E Ψ K S) (M : ℤ) : ∀ᵐ (a : CoeffSpace d) ∂P, ∀ (k : ℤ) (v : Fin d → ℤ), standardCell d k v ⊆ centeredCube d M → BlockMatLoewnerLE (coarseBlock (standardCell d k v) a) (blockScale ((1 + (3 ^ M + 3 * S a) * 3 ^ (-k)) ^ g) E)

The same bound for cubes contained in the macroscopic cube: a cube contains its own centre.

The tail of the cross-grid series

theorem HCPolySupport.HighContrast.Entry.zpow_mul_rpow_neg (n r : ℤ) (g : ℝ) : 3 ^ (r - n) * (3 ^ (-r)) ^ g = 3 ^ (-n) * 3 ^ (↑r * (1 - g))

The cross-grid row weight against the widened cell bound, in real powers.

theorem HCPolySupport.HighContrast.Entry.sum_crude_below_le {g : ℝ} (hg0 : 0 ≤ g) (hg1 : g < 1) {M : ℤ} (hM : 0 ≤ M) {s : ℝ} (hs : 0 ≤ s) (n J J' : ℤ) : ∑ r ∈ Finset.Ico J' J, 3 ^ (r - n) * (1 + (3 ^ M + 3 * s) * 3 ^ (-r)) ^ g ≤ 2 * (1 - g)⁻¹ * (3 ^ J + 3 ^ M + 3 * s) * (3 ^ (-n) * 3 ^ (↑J * (1 - g)))

The crude tail of the cross-grid series. Below a cutoff J ≤ 0 the widened cell bounds, weighted by the cross-grid row 3^{r-n}, total at most an affine function of the source scale times 3^{-n}3^{J(1-g)}; the bound does not depend on the lower end of the sum, and the last factor tends to zero as the cutoff descends.

theorem HCPolySupport.HighContrast.Entry.zpow_neg_mul_rpow (n : ℤ) (g : ℝ) : 3 ^ (-n) * 3 ^ (↑n * (1 - g)) = (3 ^ (-n)) ^ g

3^{-n}3^{n(1-g)} is the real power (3^{-n})^g.

theorem HCPolySupport.HighContrast.Entry.sum_crude_zpow_below_le {g : ℝ} (hg0 : 0 ≤ g) (hg1 : g < 1) (m J J' : ℤ) : ∑ r ∈ Finset.Ico J' J, 3 ^ (r - m) * (3 ^ (-r)) ^ g ≤ 2 * (1 - g)⁻¹ * (3 ^ (-m) * 3 ^ (↑J * (1 - g)))

The crude tail of the cross-grid series in the adapted regime. The weights 3^{r-m} against the real powers (3^{-r})^g total, below a cutoff, at most 2(1-g)^{-1}3^{-m}3^{J(1-g)}, uniformly in the lower end of the sum.

The archimedean choice of cutoff

theorem HCPolySupport.HighContrast.Entry.exists_tail_cutoff {g : ℝ} (hg1 : g < 1) {eps : ℝ} (heps : 0 < eps) (k : ℤ) : ∃ J ≤ 0, J ≤ k ∧ 3 ^ (↑J * (1 - g)) ≤ eps

The cutoff of the tail, chosen explicitly. For every positive tolerance there is a cutoff below both zero and a prescribed generation at which the tail factor 3^{J(1-g)} is under the tolerance; no limit is taken.

theorem HCPolySupport.HighContrast.Entry.exists_cutoff_mul_le {g : ℝ} (hg1 : g < 1) (U : ℝ) {V : ℝ} (hV : 0 < V) (k : ℤ) : ∃ J ≤ 0, J ≤ k ∧ U * 3 ^ (↑J * (1 - g)) ≤ V

The cutoff chosen against a prescribed bound. For every positive bound there is a cutoff below both zero and a prescribed generation at which a prescribed multiple of the tail factor is under the bound.

The printed gauge against the geometric series

theorem HCPolySupport.HighContrast.Entry.one_le_transferGauge {g K : ℝ} (hg0 : 0 ≤ g) (hg1 : g < 1) (k : ℤ) : 1 ≤ transferGauge g K k

The printed gauge Γ_{g,S} is at least one.

theorem HCPolySupport.HighContrast.Entry.inv_le_transferGauge {g K : ℝ} (hg0 : 0 ≤ g) (hg1 : g < 1) (k : ℤ) : (1 - g)⁻¹ ≤ transferGauge g K k

The printed gauge dominates the geometric series it is built from.