High-contrast homogenization: Provider.Quenched.AlgebraicConvergenceAssembly

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

Algebraic convergence at a polynomial scale

This module assembles t.algebraic.convergence from the pieces the provider layer already carries: the polynomial entry generation, the triadic rebase, the small-contrast endgame on the rebased law, the annealed endpoint on the original indexing, and the identification of the limiting doubled block.

The two constants stand outside the law. The exponent of the geometric decay e.algebraic.contrast.decay is the one the small-contrast endgame fixes as soon as the coarse-growth exponent is known, and the constant in the logarithmic bound on the entry generation is the product of the rebase exponent with one plus the delay exponent, that being the exponent at which the two polynomial length accounts absorb.

The limiting doubled block is self-dual, hence the constant doubled block of a coefficient matrix. The first section reads the Schur coefficients of such a block in the parametrization e.annealed.schur: they are σ_* = σ = the symmetric part of the coefficient matrix and k = its antisymmetric part. The limiting block therefore satisfies s_bar_* = s_bar, with s_bar positive definite and k_bar antisymmetric.

The Schur coefficients of a constant doubled block

theorem HCPolySupport.HighContrast.Quenched.constantBlockMatrix_eq_blockMatrixOfCoarseMatrices {d : ℕ} (a : Mat d) : Book.Ch02.constantBlockMatrix a = Book.Ch02.blockMatrixOfCoarseMatrices { sigma := symmPart a, sigmaStarInv := (symmPart a)⁻¹, kappa := skewPart a }

The constant doubled block of a coefficient matrix is the assembled block of its Schur data, in the parametrization e.annealed.schur: the symmetric part plays both σ and σ_*, and the antisymmetric part plays k.

theorem HCPolySupport.HighContrast.Quenched.schurSigmaStar_constantBlockMatrix {d : ℕ} {a : Mat d} (ha : Matrix.PosDef (symmPart a)) : schurSigmaStar (Book.Ch02.constantBlockMatrix a) = symmPart a

The Schur block σ_* of a constant doubled block is the symmetric part of the coefficient matrix.

theorem HCPolySupport.HighContrast.Quenched.schurSkew_constantBlockMatrix {d : ℕ} {a : Mat d} (ha : Matrix.PosDef (symmPart a)) : schurSkew (Book.Ch02.constantBlockMatrix a) = skewPart a

The Schur block k of a constant doubled block is the antisymmetric part of the coefficient matrix.

theorem HCPolySupport.HighContrast.Quenched.schurSigma_constantBlockMatrix {d : ℕ} {a : Mat d} (ha : Matrix.PosDef (symmPart a)) : schurSigma (Book.Ch02.constantBlockMatrix a) = symmPart a

The Schur block σ of a constant doubled block is the symmetric part of the coefficient matrix. Together with the reading of σ_* this says that a constant doubled block is self-dual.

The logarithmic reading of a polynomial length bound

theorem HCPolySupport.HighContrast.Quenched.natCast_le_ceil_mul_logb_of_three_pow_le {b C : ℝ} (hb : 0 < b) {n : ℕ} (hn : 3 ^ n ≤ b ^ C) : ↑n ≤ ⌈C * Real.logb 3 b⌉

A triadic length bounded by a power of a positive base bounds the generation by the ceiling of the corresponding base-three logarithm. This is the equivalence between the two readings of e.algebraic.entry.

The assembled theorem

theorem HCPolySupport.HighContrast.Quenched.algebraic_convergence_assembly (d : ℕ) (hd : 2 ≤ d) (g : ℝ) (hg : g ∈ Set.Ico 0 1) : ∃ (C : ℝ) (κ : ℝ), 0 < C ∧ 0 < κ ∧ ∀ (P : MeasureTheory.Measure (CoeffSpace d)) (E : BlockMat d) (Ψ : ℝ → ℝ) (K : ℝ) (S : CoeffSpace d → ℝ), MeasureTheory.IsProbabilityMeasure P → IsStationaryLaw P → IsUnitRangeLaw P → CoarseEllipticityDagger P g E Ψ K S → ∃ (m₀ : ℕ) (Abar : BlockMat d), ↑m₀ ≤ ⌈C * Real.logb 3 (2 + aspectRatio E * K)⌉ ∧ (∀ (j : ℕ), annealedContrast P ↑(m₀ + j) - 1 ≤ 3 ^ (-κ * ↑j)) ∧ IsSymmetricBlockMat Abar ∧ Book.Ch02.BlockPosDef Abar ∧ (∀ (j : ℕ), BlockMatLoewnerLE Abar (annealedBlock P (centeredCube d ↑(m₀ + j))) ∧ BlockMatLoewnerLE (annealedBlock P (centeredCube d ↑(m₀ + j))) (blockScale (1 + 6 * 3 ^ (-κ * ↑j)) Abar)) ∧ schurSigmaStar Abar = schurSigma Abar ∧ Matrix.PosDef (schurSigma Abar) ∧ IsSkewMat (schurSkew Abar)

Theorem t.algebraic.convergence: algebraic convergence at a polynomial scale. For a dimension at least two and a coarse-growth exponent below one there are a finite constant and a positive exponent, both standing outside the law, the reference block, the gauge, its growth witness and the source variable, such that under the standing assumptions there is a deterministic generation bounded as in e.algebraic.entry, at which the contrast decay e.algebraic.contrast.decay starts, together with a deterministic symmetric positive definite doubled block obeying the two-sided comparison e.algebraic.block.decay. Its Schur coefficients, in the parametrization e.annealed.schur, satisfy s_bar_* = s_bar with s_bar positive definite and k_bar antisymmetric.