High-contrast homogenization: Provider.Regularity.FiniteSequenceBounds

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

Finite sequence bounds

This module records elementary finite-interval estimates used in multiscale arguments. The statements are independent of coefficient fields and PDEs.

theorem HCPolySupport.HighContrast.finiteStepErrorSum_le (N : ℕ) (hN : 0 < N) (E F : ℤ → ℝ) (C B : ℝ) {r m : ℤ} (_hrm : r ≤ m) (hE : ∀ (j : ℤ), 0 ≤ E j) (hF : ∀ (j : ℤ), 0 ≤ F j) (hC : 0 ≤ C) (hB : 0 ≤ B) (hstep : ∀ k ∈ Finset.Icc (r + ↑N) m, E (k - ↑N) ≤ 1 / 8 * E k + C * F k) (htop : ∑ j ∈ Finset.Ioc (m - ↑N) m, E j ≤ B) : ∑ j ∈ Finset.Icc r m, E j ≤ 2 * (B + C * ∑ k ∈ Finset.Icc (r + ↑N) m, F k)

A contractive fixed-step recurrence bounds the full error sum by its terminal block and the accumulated forcing.

theorem HCPolySupport.HighContrast.euclideanNorm_le_terminal_add_sum_adjacent {d : ℕ} (p : ℤ → Vec d) {r m : ℤ} (hrm : r ≤ m) : euclideanNorm (p r) ≤ euclideanNorm (p m) + ∑ j ∈ Finset.Ico r m, euclideanNorm (p j - p (j + 1))

The Euclidean norm of the first term of a finite sequence is bounded by the terminal norm plus its successive differences.

theorem HCPolySupport.HighContrast.sum_adjacent_le_two_sum_Icc (E : ℤ → ℝ) {r m : ℤ} (_hrm : r ≤ m) (hE : ∀ (j : ℤ), 0 ≤ E j) : ∑ j ∈ Finset.Ico r m, (E j + E (j + 1)) ≤ 2 * ∑ j ∈ Finset.Icc r m, E j

The two adjacent copies of a nonnegative row over a half-open interval are bounded by twice its sum over the closed interval.