High-contrast homogenization: Provider.Regularity.GoodTail

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

Summable weak-error tails on centered cubes

The normalized large-scale regularity argument uses the finite sum of the Chapter 2 homogenization errors on centered Euclidean triadic cubes. This module records the finite-interval and infinite-tail predicates for the identity comparison matrix.

noncomputable def HCPolySupport.HighContrast.scalarIdentityWeakError {d : ℕ} (a : Book.Ch02.TriadicCoeffFamily d) (s : ℝ) (k : ℤ) : ℝ

The multiscale weak error on the centered Euclidean triadic cube at scale k, with identity comparison matrix and the p = infinity, q = 2 exponents.

Equations

• One or more equations did not get rendered due to their size.

theorem HCPolySupport.HighContrast.scalarIdentityWeakError_nonneg {d : ℕ} (a : Book.Ch02.TriadicCoeffFamily d) (s : ℝ) (k : ℤ) : 0 ≤ scalarIdentityWeakError a s k

The identity weak error is nonnegative.

def HCPolySupport.HighContrast.ScalarIdentityGoodTailOnInterval {d : ℕ} (a : Book.Ch02.TriadicCoeffFamily d) (s δ : ℝ) (n m : ℤ) : Prop

The finite l¹ weak-error row between two integer scales.

Equations

• HCPolySupport.HighContrast.ScalarIdentityGoodTailOnInterval a s δ n m = (∑ k ∈ Finset.Icc n m, HCPolySupport.HighContrast.scalarIdentityWeakError a s k ≤ δ)

def HCPolySupport.HighContrast.ScalarIdentityGoodTail {d : ℕ} (a : Book.Ch02.TriadicCoeffFamily d) (s δ : ℝ) (n : ℤ) : Prop

The l¹ weak-error row is bounded on every finite interval beginning at n.

Equations

• HCPolySupport.HighContrast.ScalarIdentityGoodTail a s δ n = ∀ (m : ℤ), n ≤ m → HCPolySupport.HighContrast.ScalarIdentityGoodTailOnInterval a s δ n m

theorem HCPolySupport.HighContrast.ScalarIdentityGoodTailOnInterval.mono {d : ℕ} {a : Book.Ch02.TriadicCoeffFamily d} {s δ δ' : ℝ} {n m : ℤ} (h : ScalarIdentityGoodTailOnInterval a s δ n m) (hδ : δ ≤ δ') : ScalarIdentityGoodTailOnInterval a s δ' n m

Increasing the tolerance preserves a finite good-tail bound.

theorem HCPolySupport.HighContrast.ScalarIdentityGoodTail.interval {d : ℕ} {a : Book.Ch02.TriadicCoeffFamily d} {s δ : ℝ} {n m : ℤ} (h : ScalarIdentityGoodTail a s δ n) (hnm : n ≤ m) : ScalarIdentityGoodTailOnInterval a s δ n m

A good tail supplies its bound on every admissible finite interval.

theorem HCPolySupport.HighContrast.ScalarIdentityGoodTail.mono {d : ℕ} {a : Book.Ch02.TriadicCoeffFamily d} {s δ δ' : ℝ} {n : ℤ} (h : ScalarIdentityGoodTail a s δ n) (hδ : δ ≤ δ') : ScalarIdentityGoodTail a s δ' n

Increasing the tolerance preserves an infinite good-tail bound.

theorem HCPolySupport.HighContrast.ScalarIdentityGoodTailOnInterval.mono_start {d : ℕ} {a : Book.Ch02.TriadicCoeffFamily d} {s δ : ℝ} {n n' m : ℤ} (h : ScalarIdentityGoodTailOnInterval a s δ n m) (hnn' : n ≤ n') : ScalarIdentityGoodTailOnInterval a s δ n' m

Discarding initial scales preserves a finite good-tail bound.

theorem HCPolySupport.HighContrast.ScalarIdentityGoodTail.mono_start {d : ℕ} {a : Book.Ch02.TriadicCoeffFamily d} {s δ : ℝ} {n n' : ℤ} (h : ScalarIdentityGoodTail a s δ n) (hnn' : n ≤ n') : ScalarIdentityGoodTail a s δ n'

Discarding initial scales preserves an infinite good-tail bound.

theorem HCPolySupport.HighContrast.ScalarIdentityGoodTail.weakError_le {d : ℕ} {a : Book.Ch02.TriadicCoeffFamily d} {s δ : ℝ} {n k : ℤ} (h : ScalarIdentityGoodTail a s δ n) (hnk : n ≤ k) : scalarIdentityWeakError a s k ≤ δ

Every weak error in a good tail is bounded by its tolerance.