High-contrast homogenization: Provider.Entry.AdapterCellBounds

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

The Euclidean filling of an adapted cell

Both halves of the comparison between adapted and Euclidean cubes read an adapted cell through its filling by the Euclidean cells, which Entry.adaptedCellAt_one identifies with the standard aligned cubes; the printed cross-grid factor is then |q^{-1}|, at most 101/100 by e.rounded.grid.bounds, and carries no eccentricity.

Three readings of that filling are prepared here, all at an arbitrary translate of the cell so that the aligned cells of the grid are covered as well as the centred one.

The pathwise elliptic bound. Every row, read through the widened cell bound of AdapterMajorant, gives a multiple of the reference block whose coefficient is affine in the source scale. This is what makes the adapted mean defined at every generation, with no window hypothesis.

The pathwise rows majorant. The rows of a finite range of generations are kept whole and only the tail below an arbitrary cutoff is paid crudely; this is the form the averaging of e.two.grid.whitney.average consumes.

The annealed cell bound. Averaging the rows against the Euclidean cell bound E[𝐀(z+□_i)] ≤ (1+9K_{Ψ_S}^23^{-i})^g𝐄 and summing the geometric series gives E[𝐀(z+⋄_r^q)] ≤ C_d(1-g)^{-1}(1+9K_{Ψ_S}^23^{-r})^g𝐄 at every generation and every aligned centre. The single factor (1-g)^{-1} is the geometric series of the filling; it is what the composed reading of the reverse comparison spends.

There are no definitions in this file.

The cells of the filling

theorem HCPolySupport.HighContrast.Entry.cell_le {d : ℕ} {g : ℝ} {E : BlockMat d} {S : CoeffSpace d → ℝ} {q : Mat d} {nn M r : ℤ} {y : Vec d} {Z : ℤ → Finset (Fin d → ℤ)} (hZ : ∀ (s : ℤ), ↑(Z s) = Transport.fillingIndex 1 nn (adaptedCellTranslate q nn y) s) (hMsub : adaptedCellTranslate q nn y ⊆ centeredCube d M) {a : CoeffSpace d} (ha : ∀ (j : ℤ) (v : Fin d → ℤ), standardCell d j v ⊆ centeredCube d M → BlockMatLoewnerLE (coarseBlock (standardCell d j v) a) (blockScale ((1 + (3 ^ M + 3 * S a) * 3 ^ (-j)) ^ g) E)) (X : BlockVec d) (w : Fin d → ℤ) : w ∈ Z r → 1 / 2 * blockVecDot X (blockMatVecMul (coarseBlock (adaptedCellAt 1 r w) a) X) ≤ (1 + (3 ^ M + 3 * S a) * 3 ^ (-r)) ^ g * (1 / 2 * blockVecDot X (blockMatVecMul E X))

The cells of the Euclidean filling of a target cell obey the widened cell bound of AdapterMajorant.

The pathwise elliptic bound

theorem HCPolySupport.HighContrast.Entry.coarseBlock_adaptedCellTranslate_le_blockScale {d : ℕ} [NeZero d] {P : MeasureTheory.Measure (CoeffSpace d)} {g : ℝ} {E : BlockMat d} {Ψ : ℝ → ℝ} {K : ℝ} {S : CoeffSpace d → ℝ} (hdag : CoarseEllipticityDagger P g E Ψ K S) {q : Mat d} (hq : Matrix.PosDef q) {nn M : ℤ} {y : Vec d} (hM : 0 ≤ M) (hMsub : adaptedCellTranslate q nn y ⊆ centeredCube d M) {Z : ℤ → Finset (Fin d → ℤ)} (hZ : ∀ (s : ℤ), ↑(Z s) = Transport.fillingIndex 1 nn (adaptedCellTranslate q nn y) s) {a : CoeffSpace d} (ha : ∀ (j : ℤ) (v : Fin d → ℤ), standardCell d j v ⊆ centeredCube d M → BlockMatLoewnerLE (coarseBlock (standardCell d j v) a) (blockScale ((1 + (3 ^ M + 3 * S a) * 3 ^ (-j)) ^ g) E)) : BlockMatLoewnerLE (coarseBlock (adaptedCellTranslate q nn y) a) (blockScale ((2 * (6 * ↑d * √↑d * ‖q⁻¹‖) * (1 - g)⁻¹ + 1) * (3 ^ (-nn)) ^ g * (3 ^ nn + 3 ^ M + 3 * S a)) E)

A translated adapted cell has a pathwise elliptic bound. Filling it with Euclidean cubes and reading every row through the widened cell bound gives a multiple of the reference block whose coefficient is affine in the source scale.

theorem HCPolySupport.HighContrast.Entry.ae_coarseBlock_adaptedCellTranslate_le_blockScale {d : ℕ} [NeZero d] {P : MeasureTheory.Measure (CoeffSpace d)} {g : ℝ} {E : BlockMat d} {Ψ : ℝ → ℝ} {K : ℝ} {S : CoeffSpace d → ℝ} (hdag : CoarseEllipticityDagger P g E Ψ K S) {q : Mat d} (hq : Matrix.PosDef q) {nn M : ℤ} {y : Vec d} (hM : 0 ≤ M) (hMsub : adaptedCellTranslate q nn y ⊆ centeredCube d M) {Z : ℤ → Finset (Fin d → ℤ)} (hZ : ∀ (s : ℤ), ↑(Z s) = Transport.fillingIndex 1 nn (adaptedCellTranslate q nn y) s) : ∀ᵐ (a : CoeffSpace d) ∂P, BlockMatLoewnerLE (coarseBlock (adaptedCellTranslate q nn y) a) (blockScale ((2 * (6 * ↑d * √↑d * ‖q⁻¹‖) * (1 - g)⁻¹ + 1) * (3 ^ (-nn)) ^ g * (3 ^ nn + 3 ^ M + 3 * S a)) E)

The pathwise elliptic bound, read almost everywhere.

theorem HCPolySupport.HighContrast.Entry.ae_forall_coarseBlock_adaptedCellAt_le_blockScale {d : ℕ} [NeZero d] {P : MeasureTheory.Measure (CoeffSpace d)} {g : ℝ} {E : BlockMat d} {Ψ : ℝ → ℝ} {K : ℝ} {S : CoeffSpace d → ℝ} (hdag : CoarseEllipticityDagger P g E Ψ K S) {q : Mat d} (hq : Matrix.PosDef q) {M : ℤ} (hM : 0 ≤ M) : ∀ᵐ (a : CoeffSpace d) ∂P, ∀ (r : ℤ) (w : Fin d → ℤ), adaptedCellAt q r w ⊆ centeredCube d M → BlockMatLoewnerLE (coarseBlock (adaptedCellAt q r w) a) (blockScale ((2 * (6 * ↑d * √↑d * ‖q⁻¹‖) * (1 - g)⁻¹ + 1) * (3 ^ (-r)) ^ g * (3 ^ r + 3 ^ M + 3 * S a)) E)

The pathwise elliptic bound at every aligned cell at once. The ellipticity of e.coarse.ellipticity is one almost-sure statement quantified over all cubes, so the bound it yields on the adapted cells holds simultaneously for all of them.

Definedness of the adapted mean at an arbitrary aligned cell

theorem HCPolySupport.HighContrast.Entry.hasIntegrableCoarseBlock_adaptedCellTranslate_of_dagger {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) {q : Mat d} (hq : Matrix.PosDef q) {nn : ℤ} {y : Vec d} (hmeas : HasMeasurableCoarseBlock P (adaptedCellTranslate q nn y)) : HasIntegrableCoarseBlock P (adaptedCellTranslate q nn y)

The adapted mean is defined at every generation and every aligned centre. The pathwise elliptic bound dominates the coarse response entrywise by an affine function of the source scale, which the source moment integrates.