Documentation

LeanPool.Superdiffusion.Algsuperdiff.Section3.Provider.ErrorComparison.Monotonicity

Monotonicity #

Ported from scottnarmstrong/Superdiffusion at 7f20476385d4af418f110303085ad0740c9eba46. Module imports, support namespace and local option directives adapted for Lean Pool.

Provider: monotonicity of the multiscale homogenization error #

This file proves a local version of the display e.mathcalE.monotone.ordered of ABK26:

For every m ∈ ℤ, p, q ∈ [1,∞] and t, s ∈ (0,∞) with t < s, > max_{|e| = 1} J(□_m, A₀^{-1/2} e, A₀^{1/2} e; a)^{1/2} > ≤ 𝓔_{s,p,q}(□_m; a, a₀) ≤ 𝓔_{t,p,q}(□_m; a, a₀).

The carrier is CoarseGraining's Homogenization.Book.Ch02.HomogenizationErrorOnCube, whose one-cube response max_{|e| = 1} J(□_m, A₀^{-1/2} e, A₀^{1/2} e; a) is Homogenization.Book.Ch02.normalizedBlockResponseMax.

Scope #

Both inequalities are proved here at the endpoint p = ∞, for every admissible q, i.e. for q ∈ [1,∞) (MultiscaleExponent.finite q) and for q = ∞ (MultiscaleExponent.infinity). CoarseGraining previously had only the special case (p, q) = (∞, 1) (Homogenization.Book.Ch02.homogenizationErrorOnCube_infinity_one_le_of_lt and scaleResponseAtScale_infinity_self_le_homogenizationErrorOnCube_infinity_one).

Main results #

References #

The p = ∞ scale response along the descending scales of a cube #

source
theorem Algsuperdiff.Section3.Provider.ErrorComparison.scaleResponse_depth_nonneg {d : ℕ} (Q : HCPolySupport.TriadicCube d) (F : HCPolySupport.Book.Ch02.TriadicCoeffFamily d) (a0 : HCPolySupport.Mat d) (l : ℕ) :
0 ≤ HCPolySupport.Book.Ch02.scaleResponseAtScale Q (Q.scale - ↑l) HCPolySupport.Book.Ch02.MultiscaleExponent.infinity F a0

Nonnegativity of the p = ∞ scale response at depth l below Q.

source
theorem Algsuperdiff.Section3.Provider.ErrorComparison.scaleResponse_depth_le_uniform {d : ℕ} [NeZero d] (Q : HCPolySupport.TriadicCube d) (F : HCPolySupport.Book.Ch02.TriadicCoeffFamily d) (a0 : HCPolySupport.Mat d) (l : ℕ) :
HCPolySupport.Book.Ch02.scaleResponseAtScale Q (Q.scale - ↑l) HCPolySupport.Book.Ch02.MultiscaleExponent.infinity F a0 ≤ (HCPolySupport.Book.Ch02.normalizedBlockResponseUniformBound Q F a0).rpow (1 / 2)

The p = ∞ scale response at depth l below Q is bounded by the uniform deterministic bound of the root cube.

source
theorem Algsuperdiff.Section3.Provider.ErrorComparison.scaleResponse_depth_monotone {d : ℕ} [NeZero d] (Q : HCPolySupport.TriadicCube d) (F : HCPolySupport.Book.Ch02.TriadicCoeffFamily d) (a0 : HCPolySupport.Mat d) :
Monotone fun (l : ℕ) => HCPolySupport.Book.Ch02.scaleResponseAtScale Q (Q.scale - ↑l) HCPolySupport.Book.Ch02.MultiscaleExponent.infinity F a0

The p = ∞ scale response increases as one descends the scales of Q.

source
theorem Algsuperdiff.Section3.Provider.ErrorComparison.scaleResponse_depth_rpow_monotone {d : ℕ} [NeZero d] (Q : HCPolySupport.TriadicCube d) (F : HCPolySupport.Book.Ch02.TriadicCoeffFamily d) (a0 : HCPolySupport.Mat d) {q : ℝ} (hq : 0 ≤ q) :
Monotone fun (l : ℕ) => (HCPolySupport.Book.Ch02.scaleResponseAtScale Q (Q.scale - ↑l) HCPolySupport.Book.Ch02.MultiscaleExponent.infinity F a0).rpow q

The q-th power of the p = ∞ scale response increases as one descends the scales of Q.

source
theorem Algsuperdiff.Section3.Provider.ErrorComparison.summable_geometricWeight_mul_scaleResponse_rpow {d : ℕ} [NeZero d] (Q : HCPolySupport.TriadicCube d) (F : HCPolySupport.Book.Ch02.TriadicCoeffFamily d) (a0 : HCPolySupport.Mat d) {s q : ℝ} (hs : 0 < s) (hq : 0 < q) :
Summable fun (l : ℕ) => HCPolySupport.Book.Ch02.geometricWeight s q l * (HCPolySupport.Book.Ch02.scaleResponseAtScale Q (Q.scale - ↑l) HCPolySupport.Book.Ch02.MultiscaleExponent.infinity F a0).rpow q

Summability of the geometrically weighted q-th powers of the p = ∞ scale responses.

source
theorem Algsuperdiff.Section3.Provider.ErrorComparison.homogenizationErrorOnCube_infinity_finite_eq_rpow_tsum {d : ℕ} (Q : HCPolySupport.TriadicCube d) (F : HCPolySupport.Book.Ch02.TriadicCoeffFamily d) (a0 : HCPolySupport.Mat d) (s q : ℝ) :
HCPolySupport.Book.Ch02.HomogenizationErrorOnCube Q s HCPolySupport.Book.Ch02.MultiscaleExponent.infinity (HCPolySupport.Book.Ch02.MultiscaleExponent.finite q) F a0 = (∑' (l : ℕ), HCPolySupport.Book.Ch02.geometricWeight s q l * (HCPolySupport.Book.Ch02.scaleResponseAtScale Q (Q.scale - ↑l) HCPolySupport.Book.Ch02.MultiscaleExponent.infinity F a0).rpow q).rpow (1 / q)

The finite-q, p = ∞ homogenization error of a cube, written out as the 1/q-th power of a geometrically weighted sum.

The first inequality of e.mathcalE.monotone.ordered #

source
theorem Algsuperdiff.Section3.Provider.ErrorComparison.rpow_half_normalizedBlockResponseMax_le_homogenizationErrorOnCube_infinity_finite {d : ℕ} [NeZero d] (Q : HCPolySupport.TriadicCube d) (F : HCPolySupport.Book.Ch02.TriadicCoeffFamily d) (a0 : HCPolySupport.Mat d) {s q : ℝ} (hs : 0 < s) (hq : 1 ≤ q) :
(HCPolySupport.Book.Ch02.normalizedBlockResponseMax Q F a0).rpow (1 / 2) ≤ HCPolySupport.Book.Ch02.HomogenizationErrorOnCube Q s HCPolySupport.Book.Ch02.MultiscaleExponent.infinity (HCPolySupport.Book.Ch02.MultiscaleExponent.finite q) F a0

First inequality of e.mathcalE.monotone.ordered (ABK26) at p = ∞ and finite q: the square root of the one-cube normalized block response of Q is bounded by 𝓔_{s,∞,q}(Q; a, a₀).

The second inequality of e.mathcalE.monotone.ordered #

source
theorem Algsuperdiff.Section3.Provider.ErrorComparison.homogenizationErrorOnCube_infinity_finite_le_of_lt {d : ℕ} [NeZero d] (Q : HCPolySupport.TriadicCube d) (F : HCPolySupport.Book.Ch02.TriadicCoeffFamily d) (a0 : HCPolySupport.Mat d) {t s q : ℝ} (ht : 0 < t) (hts : t < s) (hq : 1 ≤ q) :
HCPolySupport.Book.Ch02.HomogenizationErrorOnCube Q s HCPolySupport.Book.Ch02.MultiscaleExponent.infinity (HCPolySupport.Book.Ch02.MultiscaleExponent.finite q) F a0 ≤ HCPolySupport.Book.Ch02.HomogenizationErrorOnCube Q t HCPolySupport.Book.Ch02.MultiscaleExponent.infinity (HCPolySupport.Book.Ch02.MultiscaleExponent.finite q) F a0

Second inequality of e.mathcalE.monotone.ordered (ABK26) at p = ∞ and finite q: 𝓔_{s,∞,q} is antitone in the smoothness exponent.