CubeMonotonicity

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

Cube monotonicity of the multiscale lower ellipticity at the centered cubes

This module supplies it. The centered cube square_{k-1} is the middle child of square_k — CoarseGraining's middleChild_mem_childCubes at a cube with vanishing index — so an induction on the depth places square_m in the descendant tree of square_n.

Main results

• originCube_pred_mem_childCubes: square_{n-1} is a child of square_n.
• originCube_mem_descendantsAtDepth: square_{n-j} is a depth-j descendant of square_n.
• lambdaSq_originCube_le_descendantWeight_mul_lambdaSq: the named cube-monotonicity lemma at the centered pair, lambda_{s,q}(square_n; a) <= 3^{2s(n-m)} lambda_{s,q}(square_m; a).

References

• ABK26, l.bad.event.lemma (decomposition, recombination).
• ABK26, e.ellipticities.monotone.ordered.

The centered cubes form a descendant chain

theorem Algsuperdiff.Section3.Provider.ErrorComparison.originCube_pred_mem_childCubes (d : ℕ) (n : ℤ) : HCPolySupport.originCube d (n - 1) ∈ HCPolySupport.childCubes (HCPolySupport.originCube d n)

The centered cube of scale n - 1 is the middle child of the centered cube of scale n.

theorem Algsuperdiff.Section3.Provider.ErrorComparison.originCube_mem_descendantsAtDepth (d : ℕ) (n : ℤ) (j : ℕ) : HCPolySupport.originCube d (n - ↑j) ∈ HCPolySupport.descendantsAtDepth (HCPolySupport.originCube d n) j

The centered cube of scale n - j is a depth-j triadic descendant of the centered cube of scale n.

theorem Algsuperdiff.Section3.Provider.ErrorComparison.originCube_mem_descendantsAtScale {d : ℕ} {m n : ℤ} (hmn : m ≤ n) : HCPolySupport.originCube d m ∈ HCPolySupport.descendantsAtScale (HCPolySupport.originCube d n) m

The membership. For m <= n the centered cube square_m is a triadic descendant of square_n at scale m.

Cube monotonicity at the centered pair

theorem Algsuperdiff.Section3.Provider.ErrorComparison.lambdaSq_originCube_le_descendantWeight_mul_lambdaSq {d : ℕ} [NeZero d] (a : HCPolySupport.Book.Ch02.TriadicCoeffFamily d) {m n : ℤ} (hmn : m ≤ n) {s : ℝ} {q : HCPolySupport.Book.Ch02.MultiscaleExponent} (hs : 0 < s) (hq : q.IsAdmissible) : HCPolySupport.Book.Ch02.lambdaSq (HCPolySupport.originCube d n) s q a ≤ HCPolySupport.Book.Ch02.multiscaleDescendantWeight (HCPolySupport.originCube d n) m s * HCPolySupport.Book.Ch02.lambdaSq (HCPolySupport.originCube d m) s q a

For m <= n,

lambda_{s,q}(square_n; a) <= 3^{2s(n-m)} lambda_{s,q}(square_m; a).

theorem Algsuperdiff.Section3.Provider.ErrorComparison.multiscaleDescendantWeight_originCube {d : ℕ} (m n : ℤ) (s : ℝ) : HCPolySupport.Book.Ch02.multiscaleDescendantWeight (HCPolySupport.originCube d n) m s = 3 ^ (2 * s * (↑n - ↑m))

The weight of the previous theorem, in closed form.

theorem Algsuperdiff.Section3.Provider.ErrorComparison.lambdaSq_originCube_eighth_le {d : ℕ} [NeZero d] (a : HCPolySupport.Book.Ch02.TriadicCoeffFamily d) {m n : ℤ} (hmn : m ≤ n) : HCPolySupport.Book.Ch02.lambdaSq (HCPolySupport.originCube d n) (1 / 8) (HCPolySupport.Book.Ch02.MultiscaleExponent.finite 2) a ≤ 3 ^ ((↑n - ↑m) / 4) * HCPolySupport.Book.Ch02.lambdaSq (HCPolySupport.originCube d m) (1 / 8) (HCPolySupport.Book.Ch02.MultiscaleExponent.finite 2) a

lambda_{1/8,2}(square_n; a) <= 3^{(n-m)/4} lambda_{1/8,2}(square_m; a).