High-contrast homogenization: Provider.Quenched.SmallContrastBootstrapReference

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

The Euclidean reference ratio

The tilt scalarization absorbs a Loewner adapter error ≤ c·𝐄 into a multiplicative comparison with the reference mean; the absorbed size is c · |𝐄 relative to that mean|. For the bootstrap the reference mean is the annealed block of a centered cube, so the size that has to be controlled is blockSize 𝐄 (𝐀(□_k)) — and it has to be controlled uniformly in k, since the cube used by the bootstrap moves with the generation.

The terminal comparability chain supplies exactly that: the Dagger envelope bounds the annealed block above by a multiple of 𝐄, the sharp reverses the order, the annealed block dominates its own sharp, and 𝐄 ≤ κ_𝐄 𝐄_#. On the Euclidean grid the enlargement is zero — the adapted cell is the cube — so the resulting factor

κ_𝐄 · C(K) · B_1

carries no generation-dependent power of three. It is a law constant, fixed once, valid at every generation past the source burn.

noncomputable def HCPolySupport.HighContrast.Quenched.euclideanReferenceRatio {d : ℕ} (Cd g K : ℝ) (E : BlockMat d) : ℝ

The Euclidean reference ratio κ_𝐄 · C(K) · B_1: the generation-free comparability constant of the reference block against the annealed block of a centered cube.

Equations

• One or more equations did not get rendered due to their size.

theorem HCPolySupport.HighContrast.Quenched.reference_le_annealedBlock_centeredCube {d : ℕ} [NeZero d] (hd : 2 ≤ d) {g : ℝ} (hg : g ∈ Set.Ico 0 1) {P : MeasureTheory.Measure (CoeffSpace d)} [MeasureTheory.IsProbabilityMeasure P] {E : BlockMat d} {Ψ : ℝ → ℝ} {K : ℝ} {S : CoeffSpace d → ℝ} (hdag : CoarseEllipticityDagger P g E Ψ K S) {Cd : ℝ} (hCd : max 1 (12 * ↑d * √↑d) ≤ Cd) {sK : ℤ} (hsK : growthBar K ≤ 3 ^ sK) {k : ℤ} (hk : sK + 1 ≤ k) : 1 ≤ euclideanReferenceRatio Cd g K E ∧ BlockMatLoewnerLE E (blockScale (euclideanReferenceRatio Cd g K E) (annealedBlock P (centeredCube d k)))

The reference block is dominated by the annealed block of every centered cube past the source burn, with a generation-free factor.

theorem HCPolySupport.HighContrast.Quenched.blockSize_reference_adaptedMean_one_le {d : ℕ} [NeZero d] (hd : 2 ≤ d) {g : ℝ} (hg : g ∈ Set.Ico 0 1) {P : MeasureTheory.Measure (CoeffSpace d)} [MeasureTheory.IsProbabilityMeasure P] {E : BlockMat d} {Ψ : ℝ → ℝ} {K : ℝ} {S : CoeffSpace d → ℝ} (hdag : CoarseEllipticityDagger P g E Ψ K S) {Cd : ℝ} (hCd : max 1 (12 * ↑d * √↑d) ≤ Cd) {sK : ℤ} (hsK : growthBar K ≤ 3 ^ sK) {k : ℤ} (hk : sK + 1 ≤ k) : blockSize E (adaptedMean P 1 k) ≤ euclideanReferenceRatio Cd g K E

The absorbed size of the reference against the Euclidean adapted mean is bounded by the generation-free reference ratio.