InftyToQ #

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

Provider: bounding the `p = ∞` error by the finite-`p` error #

This file proves a local version of the display e.mathcalE.infty.to.q of ABK26: for every p, q ∈ [1,∞] and s ∈ (d/p, 1),

𝓔_{s,∞,q}(□_m, n; a, a₀) ≤ 3^{(d/p)(m-n)} (c_{sq} / c_{q(s - d/p)})^{1/q} 𝓔_{s - d/p, p, q}(□_m, n; a, a₀),

where c_{sq} = 1 - 3^{-sq} is Homogenization.Book.Ch02.geometricDiscount s q.

Scope #

The proof printed in the source is the finite-q computation; the endpoint q = ∞ is obtained there by sending q → ∞. Accordingly this file proves the finite-p, finite-q case, which is the case carrying the printed constant. The exponent restriction s ∈ (d/p, 1) of the display is kept verbatim as the pair of hypotheses (d : ℝ) / p < s and s < 1; only the lower restriction is used in the proof, and the upper restriction s < 1 is retained (with the Mathlib underscore name _hs1 for an unused hypothesis) because the source states the display only in that range.

The truncation parameter n of 𝓔_{s,p,q}(□_m, n; ·) is carried explicitly, so the geometric prefactor 3^{(d/p)(m-n)} appears exactly as printed; n ≤ m is required, as in the source, where the sum defining 𝓔 runs over scales l ≤ n inside □_m.

Main results #

scaleResponseAtScale_infinity_rpow_le_card_mul_finite: the one-scale Hölder/counting step max_z ≤ (∑_z)^{...} of the printed proof.
homogenizationError_infinity_le_finite: the display.

References #

ABK26 (e.mathcalE.infty.to.q and its proof).

Real-power bookkeeping #

source

theorem Algsuperdiff.Section3.Provider.ErrorComparison.mul_rpow' {x y : ℝ} (hx : 0 ≤ x) (hy : 0 ≤ y) (z : ℝ) :

(x * y).rpow z = x.rpow z * y.rpow z

Real.mul_rpow, restated with explicit Real.rpow applications so that it is usable by rw against CoarseGraining's Real.rpow spelling.

source

theorem Algsuperdiff.Section3.Provider.ErrorComparison.rpow_natCast' (x : ℝ) (m : ℕ) :

x.rpow ↑m = x ^ m

Real.rpow_natCast, restated with an explicit Real.rpow application.

source

theorem Algsuperdiff.Section3.Provider.ErrorComparison.rpow_rpow {x : ℝ} (hx : 0 ≤ x) (y z : ℝ) :

(x.rpow y).rpow z = x.rpow (y * z)

Iterated real powers of a nonnegative base multiply their exponents.

source

theorem Algsuperdiff.Section3.Provider.ErrorComparison.rpow_rpow_of_mul_eq_one {x y z : ℝ} (hx : 0 ≤ x) (hyz : y * z = 1) :

(x.rpow y).rpow z = x

Iterated real powers with reciprocal exponents cancel.

Averages over a finite set #

source

theorem Algsuperdiff.Section3.Provider.ErrorComparison.finsetAverageReal_nonneg {α : Type u_1} (s : Finset α) {f : α → ℝ} (hf : ∀ x ∈ s, 0 ≤ f x) :

0 ≤ HCPolySupport.Book.Ch02.finsetAverageReal s f

A finsetAverageReal of nonnegative values is nonnegative.

source

theorem Algsuperdiff.Section3.Provider.ErrorComparison.finsetAverageReal_le {α : Type u_1} (s : Finset α) {f : α → ℝ} {C : ℝ} (hC0 : 0 ≤ C) (hC : ∀ x ∈ s, f x ≤ C) :

HCPolySupport.Book.Ch02.finsetAverageReal s f ≤ C

A finsetAverageReal is bounded by any nonnegative pointwise bound.

The finite-`p` one-scale response #

source

theorem Algsuperdiff.Section3.Provider.ErrorComparison.scaleResponseAtScale_finite_eq {d : ℕ} (Q : HCPolySupport.TriadicCube d) (k : ℤ) (p : ℝ) (F : HCPolySupport.Book.Ch02.TriadicCoeffFamily d) (a0 : HCPolySupport.Mat d) :

HCPolySupport.Book.Ch02.scaleResponseAtScale Q k (HCPolySupport.Book.Ch02.MultiscaleExponent.finite p) F a0 = (HCPolySupport.Book.Ch02.finsetAverageReal (HCPolySupport.descendantsAtScale Q k) fun (R : HCPolySupport.TriadicCube d) => (HCPolySupport.Book.Ch02.normalizedBlockResponseMax R F a0).rpow (p / 2)).rpow (1 / p)

Definitional form of the finite-p one-scale response.

source

theorem Algsuperdiff.Section3.Provider.ErrorComparison.finsetAverage_normalizedBlockResponseMax_rpow_nonneg {d : ℕ} (Q : HCPolySupport.TriadicCube d) (k : ℤ) (F : HCPolySupport.Book.Ch02.TriadicCoeffFamily d) (a0 : HCPolySupport.Mat d) (p : ℝ) :

0 ≤ HCPolySupport.Book.Ch02.finsetAverageReal (HCPolySupport.descendantsAtScale Q k) fun (R : HCPolySupport.TriadicCube d) => (HCPolySupport.Book.Ch02.normalizedBlockResponseMax R F a0).rpow (p / 2)

The average appearing in the finite-p one-scale response is nonnegative.

The one-scale counting step #

source

theorem Algsuperdiff.Section3.Provider.ErrorComparison.scaleResponseAtScale_infinity_rpow_le_card_mul_finite {d : ℕ} (Q : HCPolySupport.TriadicCube d) {k : ℤ} (hk : k ≤ Q.scale) (F : HCPolySupport.Book.Ch02.TriadicCoeffFamily d) (a0 : HCPolySupport.Mat d) {p q : ℝ} (hp : 0 < p) (hq : 0 < q) :

(HCPolySupport.Book.Ch02.scaleResponseAtScale Q k HCPolySupport.Book.Ch02.MultiscaleExponent.infinity F a0).rpow q ≤ (↑(HCPolySupport.descendantsAtScale Q k).card).rpow (q / p) * (HCPolySupport.Book.Ch02.scaleResponseAtScale Q k (HCPolySupport.Book.Ch02.MultiscaleExponent.finite p) F a0).rpow q

The one-scale step of the printed proof of e.mathcalE.infty.to.q: the maximum over the descendants at one scale is bounded by the p-average over the same scale, at the cost of the number of descendants.