High-contrast homogenization: Provider.Regularity.CorrectorTelescope

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

Local gradient telescopes

Summable scalar weak-error rows control finite telescopes of local gradient classes. The estimates are stated for normalized centered cubes and retain the slope factor explicitly.

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

The weak-error expression occurring in the finite-corrector slope estimate.

Equations

• HCPolySupport.HighContrast.scalarIdentityCorrectedWeakError a s k = HCPolySupport.HighContrast.scalarIdentityWeakError a s k * (1 + HCPolySupport.HighContrast.scalarIdentityWeakError a s k)

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

The corrected scalar weak error is nonnegative.

def HCPolySupport.HighContrast.intNatShiftEmbedding (n : ℤ) : ℕ ↪ ℤ

The injective indexing map from natural offsets to integer scales, j ↦ n + j.

Equations

• HCPolySupport.HighContrast.intNatShiftEmbedding n = { toFun := fun (j : ℕ) => n + ↑j, inj' := ⋯ }

theorem HCPolySupport.HighContrast.ScalarIdentityGoodTail.summable_nat_shift {d : ℕ} {a : Book.Ch02.TriadicCoeffFamily d} {s δ : ℝ} {n : ℤ} (h : ScalarIdentityGoodTail a s δ n) : Summable fun (j : ℕ) => scalarIdentityWeakError a s (n + ↑j)

An infinite scalar good tail gives a summable sequence after reindexing the integer scales by natural offsets.

theorem HCPolySupport.HighContrast.ScalarIdentityGoodTail.summable_corrected_nat_shift {d : ℕ} {a : Book.Ch02.TriadicCoeffFamily d} {s δ : ℝ} {n : ℤ} (h : ScalarIdentityGoodTail a s δ n) : Summable fun (j : ℕ) => scalarIdentityCorrectedWeakError a s (n + ↑j)

The quadratic correction of a summable good-tail row remains summable.

theorem HCPolySupport.HighContrast.ScalarIdentityGoodTail.sum_Ico_corrected_nat_shift_le {d : ℕ} {a : Book.Ch02.TriadicCoeffFamily d} {s δ : ℝ} {n : ℤ} (h : ScalarIdentityGoodTail a s δ n) (k m : ℕ) : ∑ j ∈ Finset.Ico k m, scalarIdentityCorrectedWeakError a s (n + ↑j) ≤ (1 + δ) * δ

Corrected weak errors on every finite natural-offset interval are bounded by the good-tail budget.

theorem HCPolySupport.HighContrast.norm_sub_le_sum_Ico_of_successive_norm_le {E : Type u_1} [NormedAddCommGroup E] (g : ℕ → E) (ε : ℕ → ℝ) (C R : ℝ) (hstep : ∀ (j : ℕ), ‖g (j + 1) - g j‖ ≤ C * ε j * R) {k m : ℕ} (hkm : k ≤ m) : ‖g m - g k‖ ≤ (C * ∑ j ∈ Finset.Ico k m, ε j) * R

A bound on successive differences gives the corresponding finite interval telescope.

theorem HCPolySupport.HighContrast.cauchySeq_of_summable_successive_norm_le {E : Type u_1} [NormedAddCommGroup E] (g : ℕ → E) (ε : ℕ → ℝ) (C R : ℝ) (hε : Summable ε) (hstep : ∀ (j : ℕ), ‖g (j + 1) - g j‖ ≤ C * ε j * R) : CauchySeq g

Summable bounds on successive differences make a normed-group sequence Cauchy.

theorem HCPolySupport.HighContrast.localGradientL2_cauchySeq_of_summable_successive_norm_le {d q : ℕ} (g : ℕ → ↥(LocalGradientL2 d q)) (ε : ℕ → ℝ) (C : ℝ) (e : Vec d) (hε : Summable ε) (hstep : ∀ (j : ℕ), ‖g (j + 1) - g j‖ ≤ C * ε j * euclideanNorm e) : CauchySeq g

Summable successive bounds make one local-gradient coordinate Cauchy.