High-contrast homogenization:

Provider.PolynomialHomogenization.Root.Corrector.C1FixedProjectionAlgebra

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

Finite geometric control for a fixed affine slope

The affine slope chosen on the smallest cube is compared with the exact minimizer on every larger cube by summing consecutive slope increments. The quarter-power energy growth is summable against any decay exponent at least one half.

theorem HCPolySupport.HighContrast.Root.sqrt_normalizedEnergy_linearMap_sub_le_sum_Ico_int {d : ℕ} {U : Set (Vec d)} {a : CoeffField d} {lam Lam : ℝ} (hEll : IsEllipticFieldOn lam Lam U a) (hvol : 0 < MeasureTheory.volume U) (hvoltop : MeasureTheory.volume U ≠ ⊤) (T : Vec d →ₗ[ℝ] ↥(HilbertVectorL2 U)) (b : ℤ → Vec d) {n q : ℤ} (hnq : n ≤ q) : √(normalizedLocalSymmetricEnergy hEll (T (b q - b n))) ≤ ∑ j ∈ Finset.Ico n q, √(normalizedLocalSymmetricEnergy hEll (T (b (j + 1) - b j)))

A linear family in a coefficient-energy space telescopes over integer scales.

theorem HCPolySupport.HighContrast.Root.sum_quarterGrowth_mul_realRateDecay_le (eta : ℝ) (heta : 1 / 2 ≤ eta) {n q m : ℤ} (_hnq : n ≤ q) (_hqm : q ≤ m) : ∑ j ∈ Finset.Ico n q, Real.rpow 3 ((↑q - ↑j) / 4) * Real.rpow 3 (-eta * (↑m - ↑j)) ≤ Real.rpow 3 (-eta * (↑m - ↑q)) * (1 / (1 - Real.rpow 3 (-(eta - 1 / 4))))

The product of the quarter-power scale growth and the inward excess decay has a uniformly summable geometric tail.