High-contrast homogenization: Provider.Quenched.AnnealedEndpointAssembly

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

The annealed endpoint of the endgame, assembled on the rebased law

The endgame of t.random.homogenization rebases the law once at a generation n_rb and then reads the annealed estimates of the rebased law back through the covariance of the coarse blocks and the contrast under a dilation of the law, established in ss.algebraic.convergence. This file performs that reading: it converts the rebased annealed data at the delay m_0 of e.algebraic.entry into the original indexing at N_ann = n_rb + m_0 of e.algebraic.entry, and accounts the polynomial cost e.algebraic.entry.

Three ingredients are supplied here from the standing assumptions alone: the limit block of the rebased law with its symmetry, its positive definiteness and its lower Loewner bound; the reindexing of the contrast and of the annealed block along the covariance; and the additive absorption of the two polynomial length costs into one exponent. The upper Loewner comparison and the geometric contrast decay are the analytic content of the small-contrast endgame and enter as explicit hypotheses.

The additive absorption of the polynomial length costs

theorem HCPolySupport.HighContrast.Quenched.three_pow_add_le_rpow_of_length_costs {base b : ℝ} {n m : ℕ} {Crebase Cdelay : ℝ} (hbase0 : 0 ≤ base) (hb0 : 0 ≤ b) (hn : 3 ^ n ≤ base ^ Crebase) (hb : b ≤ base ^ Crebase) (hm : 3 ^ m ≤ b ^ Cdelay) (hCdelay : 0 ≤ Cdelay) : 3 ^ (n + m) ≤ base ^ (Crebase * (1 + Cdelay))

The two polynomial length costs absorb additively. A rebase length bounded by base ^ Crebase, a reference size bounded by the same power, and a delay bounded by the Cdelay power of that reference size together bound the total length by the Crebase * (1 + Cdelay) power of the base. Requiring only Crebase ≤ Cann and Cdelay ≤ Cann separately would not suffice.

At the product exponent the base needs no lower bound beyond nonnegativity: the rebase clause already forces the intermediate power to be at least one.

theorem HCPolySupport.HighContrast.Quenched.three_pow_add_le_rpow_of_length_costs_le {base b : ℝ} {n m : ℕ} {Crebase Cdelay Cann : ℝ} (hbase : 1 ≤ base) (hb0 : 0 ≤ b) (hn : 3 ^ n ≤ base ^ Crebase) (hb : b ≤ base ^ Crebase) (hm : 3 ^ m ≤ b ^ Cdelay) (hCdelay : 0 ≤ Cdelay) (hCann : Crebase * (1 + Cdelay) ≤ Cann) : 3 ^ (n + m) ≤ base ^ Cann

The length account at an enlarged exponent, which does require the base to be at least one.

Reindexing along the scale covariance

theorem HCPolySupport.HighContrast.Quenched.annealedContrast_shift_of_covariance {d : ℕ} {P Pbase : MeasureTheory.Measure (CoeffSpace d)} {nBase m : ℕ} (hcov : ∀ (j : ℕ), annealedContrast Pbase ↑j = annealedContrast P ↑(nBase + j)) (j : ℕ) : annealedContrast Pbase ↑(m + j) = annealedContrast P ↑(nBase + m + j)

The rebased contrast at the delayed generation is the original contrast at the annealed entry generation, read through the covariance of the contrast under a dilation of the law.

theorem HCPolySupport.HighContrast.Quenched.annealedBlock_shift_of_covariance {d : ℕ} {P Pbase : MeasureTheory.Measure (CoeffSpace d)} {nBase m : ℕ} (hcov : ∀ (j : ℕ), annealedBlock Pbase (centeredCube d ↑j) = annealedBlock P (centeredCube d ↑(nBase + j))) (j : ℕ) : annealedBlock Pbase (centeredCube d ↑(m + j)) = annealedBlock P (centeredCube d ↑(nBase + m + j))

The rebased annealed block at the delayed generation is the original annealed block at the annealed entry generation.

The assembled endpoint

theorem HCPolySupport.HighContrast.Quenched.exists_annealed_endpoint_of_rebased_decay {d : ℕ} [NeZero d] {P Pbase : MeasureTheory.Measure (CoeffSpace d)} [MeasureTheory.IsProbabilityMeasure Pbase] {E Ebase : BlockMat d} {Ψbase : ℝ → ℝ} {K Kbase gBase : ℝ} {Sbase : CoeffSpace d → ℝ} {alpha Crebase Cdelay Cann : ℝ} {nBase m0 : ℕ} (hstat : IsStationaryLaw Pbase) (hdag : CoarseEllipticityDagger Pbase gBase Ebase Ψbase Kbase Sbase) (hcovContrast : ∀ (j : ℕ), annealedContrast Pbase ↑j = annealedContrast P ↑(nBase + j)) (hcovBlock : ∀ (j : ℕ), annealedBlock Pbase (centeredCube d ↑j) = annealedBlock P (centeredCube d ↑(nBase + j))) (hbase : 1 ≤ 2 + aspectRatio E * K) (hnBase : 3 ^ nBase ≤ (2 + aspectRatio E * K) ^ Crebase) (hrefCost : 2 + aspectRatio Ebase * Kbase ≤ (2 + aspectRatio E * K) ^ Crebase) (hCdelay : 0 ≤ Cdelay) (hCann : Crebase * (1 + Cdelay) ≤ Cann) (hdelay : 3 ^ m0 ≤ (2 + aspectRatio Ebase * Kbase) ^ Cdelay) (hcontrast : ∀ (j : ℕ), annealedContrast Pbase ↑(m0 + j) - 1 ≤ 3 ^ (-alpha * ↑j)) (hupper : ∀ (j : ℕ), BlockMatLoewnerLE (annealedBlock Pbase (centeredCube d ↑(m0 + j))) (blockScale (1 + 6 * 3 ^ (-alpha * ↑j)) (annealedLimitBlock Pbase))) : ∃ (Abar : BlockMat d) (Nann : ℕ), IsSymmetricBlockMat Abar ∧ Book.Ch02.BlockPosDef Abar ∧ 3 ^ Nann ≤ (2 + aspectRatio E * K) ^ Cann ∧ (∀ (j : ℕ), annealedContrast P ↑(Nann + j) - 1 ≤ 3 ^ (-alpha * ↑j)) ∧ (∀ (j : ℕ), BlockMatLoewnerLE Abar (annealedBlock P (centeredCube d ↑(Nann + j))) ∧ BlockMatLoewnerLE (annealedBlock P (centeredCube d ↑(Nann + j))) (blockScale (1 + 6 * 3 ^ (-alpha * ↑j)) Abar)) ∧ Abar = annealedLimitBlock Pbase

The annealed endpoint on the original indexing. From the standing assumptions on the rebased law, the two scale covariances and the two polynomial rebase costs, and the small-contrast conclusions of the endgame on the rebased law, this produces the endgame's annealed package at N_ann = n_rb + m_0: a symmetric positive definite limit block, the polynomial bound on 3^{N_ann}, the geometric contrast decay e.algebraic.contrast.decay, and the two-sided Loewner comparison e.algebraic.block.decay.

The limit block, its symmetry, its lower Loewner bound, the reindexing and the length accounting are proved here. The geometric contrast decay and the upper Loewner comparison are the hypotheses hcontrast and hupper.