High-contrast homogenization: Provider.Regularity.CorrectorIntrinsicSlopeDiagonal

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

A summable diagonal principle for intrinsic slope

Uniform summable control of successive finite-volume averages identifies the large-cube diagonal limit. This is the topology/series mechanism needed to turn the good-tail telescope of the corrector into its intrinsic slope.

theorem HCPolySupport.HighContrast.tendsto_zero_of_summable_successive_norm_le_of_diagonal_tendsto {d : ℕ} (x : ℕ → ℕ → Vec d) (L : ℕ → Vec d) (epsilon : ℕ → ℝ) (C : ℝ) (hsum : Summable epsilon) (hrow : ∀ (q : ℕ), Filter.Tendsto (x q) Filter.atTop (nhds (L q))) (hdiag : Filter.Tendsto (fun (q : ℕ) => x q 0) Filter.atTop (nhds 0)) (hstep : ∀ (q k : ℕ), ‖x q (k + 1) - x q k‖ ≤ C * epsilon (q + k)) : Filter.Tendsto L Filter.atTop (nhds 0)

If every row converges, its diagonal tends to zero, and all successive row increments are controlled by one summable sequence shifted by the row index, then the row limits tend to zero along the diagonal.