HomMollifyBox

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

Theorem B, §4.5, Step 3c: the translated-box average carrier

What this module supplies

The mollifier calculus is the remaining ingredient of the lifting: the two scale-by-scale estimates

  (L)  |W_n(x) - W_n(y)| ≤ A · 3^{-ns} · |x - y|
  (I)  |W_n(x) - W_{n-1}(x)| ≤ A · 3^{n(1-s)}

for a regularization family W_n of w. Both descend from one bound on the gradient of the regularization, |∇W_n| ≤ A 3^{-ns}; and since ∇(w ⋆ φ) = (∇w) ⋆ φ, that bound is a statement about the pairing of ∇w against the mollifier. The only information about ∇w the manuscript supplies is its negative-order gauge — i.e. its cube averages. This module builds the carrier those averages live on, in the form the mollifier calculus needs: the average over the box of side 3^n centred at an arbitrary point, not only at a triadic grid point.

The sup-norm coincidence

Vec d = Fin d → ℝ carries the supremum norm, so Metric.closedBall x r is exactly the axis-parallel box x + [-r,r]^d. The scale-n box centred at x is therefore Metric.closedBall x (3^n/2), and CoarseGraining's closedBallAverage is already the sliding box average. Everything below is phrased through that identification, which buys the volume formula, the convexity needed for the mean value inequality, and CoarseGraining's Lebesgue differentiation for translated boxes.

The grid/translate distinction (this file's central structural finding)

The negative Besov seminorm definition sums over z ∈ 3^n ℤ^d ∩ □_m: the depth-j quantity of the negBesovInftyNorm is a maximum over the triadic grid descendantsAtDepth Q j. A mollifier centred at a general point x sees the box x + □_n, which is not a grid cube. The two gauges are related in exactly one elementary direction,

  grid gauge  ≤  √d · translate gauge · 3^{-s·scale},

because every grid cube is a translate. The converse — reconstructing a translate average from the grid averages at all scales — is true, but is a genuine martingale/telescoping argument over the triadic filtration; see the "reconstruction residue" section of HomMollifyPairing. Accordingly the mollifier calculus of this file runs on the translate gauge UniformBoxGaugeBound, which is the stronger of the two hypotheses.

Main definitions and results

• boxRadius n — the half-side 3^n/2; boxSet n x — the scale-n box centred at x, i.e. Metric.closedBall x (boxRadius n).
• volume_boxSet, measurableSet_boxSet, isCompact_boxSet.
• boxAverage, boxAverageVec — the scalar and vector sliding averages, defined through CoarseGraining's closedBallAverage.
• UniformBoxGaugeBound m s A F — the translate-uniform negative gauge of order -s: ‖(F)_{x+□_n}‖ ≤ A 3^{-ns} for every n ≤ m and every x.

References

• ABK26, the negative Besov seminorm definition.
• ABK26, Theorem B Step 3.

1. The translated box

noncomputable def Algsuperdiff.Section4.Provider.Homogenization.boxRadius (n : ℤ) : ℝ

The half-side of the scale-n box.

Equations

• Algsuperdiff.Section4.Provider.Homogenization.boxRadius n = 3 ^ ↑n / 2

theorem Algsuperdiff.Section4.Provider.Homogenization.boxRadius_def (n : ℤ) : boxRadius n = 3 ^ ↑n / 2

theorem Algsuperdiff.Section4.Provider.Homogenization.boxRadius_pos (n : ℤ) : 0 < boxRadius n

theorem Algsuperdiff.Section4.Provider.Homogenization.two_mul_boxRadius (n : ℤ) : 2 * boxRadius n = 3 ^ ↑n

def Algsuperdiff.Section4.Provider.Homogenization.boxSet {d : ℕ} (n : ℤ) (x : HCPolySupport.Vec d) : Set (HCPolySupport.Vec d)

The scale-n box centred at x. In the supremum norm of Vec d the closed metric ball is the axis-parallel box of side 2r, so this is the manuscript's x + □_n.

Equations

• Algsuperdiff.Section4.Provider.Homogenization.boxSet n x = Metric.closedBall x (Algsuperdiff.Section4.Provider.Homogenization.boxRadius n)

theorem Algsuperdiff.Section4.Provider.Homogenization.boxSet_def {d : ℕ} (n : ℤ) (x : HCPolySupport.Vec d) : boxSet n x = Metric.closedBall x (boxRadius n)

theorem Algsuperdiff.Section4.Provider.Homogenization.mem_boxSet_iff {d : ℕ} {n : ℤ} {x y : HCPolySupport.Vec d} : y ∈ boxSet n x ↔ ‖y - x‖ ≤ boxRadius n

theorem Algsuperdiff.Section4.Provider.Homogenization.measurableSet_boxSet {d : ℕ} (n : ℤ) (x : HCPolySupport.Vec d) : MeasurableSet (boxSet n x)

theorem Algsuperdiff.Section4.Provider.Homogenization.isCompact_boxSet {d : ℕ} (n : ℤ) (x : HCPolySupport.Vec d) : IsCompact (boxSet n x)

theorem Algsuperdiff.Section4.Provider.Homogenization.volume_boxSet {d : ℕ} (n : ℤ) (x : HCPolySupport.Vec d) : MeasureTheory.volume (boxSet n x) = ENNReal.ofReal ((3 ^ ↑n) ^ d)

The volume of the box is the d-th power of its side length.

theorem Algsuperdiff.Section4.Provider.Homogenization.boxVolume_pos {d : ℕ} (n : ℤ) : 0 < (3 ^ ↑n) ^ d

theorem Algsuperdiff.Section4.Provider.Homogenization.toReal_volume_boxSet {d : ℕ} (n : ℤ) (x : HCPolySupport.Vec d) : (MeasureTheory.volume (boxSet n x)).toReal = (3 ^ ↑n) ^ d

theorem Algsuperdiff.Section4.Provider.Homogenization.volume_boxSet_lt_top {d : ℕ} (n : ℤ) (x : HCPolySupport.Vec d) : MeasureTheory.volume (boxSet n x) < ⊤

2. The box averages

noncomputable def Algsuperdiff.Section4.Provider.Homogenization.boxAverage {d : ℕ} (n : ℤ) (x : HCPolySupport.Vec d) (f : HCPolySupport.Vec d → ℝ) : ℝ

The average of a scalar field over the scale-n box centred at x, CoarseGraining's sliding closed-ball average at the half-side 3^n/2.

Equations

• Algsuperdiff.Section4.Provider.Homogenization.boxAverage n x f = HCPolySupport.CubeCalderonZygmund.closedBallAverage x (Algsuperdiff.Section4.Provider.Homogenization.boxRadius n) f

noncomputable def Algsuperdiff.Section4.Provider.Homogenization.boxAverageVec {d : ℕ} (n : ℤ) (x : HCPolySupport.Vec d) (F : HCPolySupport.Vec d → HCPolySupport.Vec d) : HCPolySupport.Vec d

The coordinatewise average of a vector field over the same box.

Equations

• Algsuperdiff.Section4.Provider.Homogenization.boxAverageVec n x F i = Algsuperdiff.Section4.Provider.Homogenization.boxAverage n x fun (y : HCPolySupport.Vec d) => F y i

theorem Algsuperdiff.Section4.Provider.Homogenization.boxAverage_def {d : ℕ} (n : ℤ) (x : HCPolySupport.Vec d) (f : HCPolySupport.Vec d → ℝ) : boxAverage n x f = HCPolySupport.CubeCalderonZygmund.closedBallAverage x (boxRadius n) f

theorem Algsuperdiff.Section4.Provider.Homogenization.boxAverageVec_apply {d : ℕ} (n : ℤ) (x : HCPolySupport.Vec d) (F : HCPolySupport.Vec d → HCPolySupport.Vec d) (i : Fin d) : boxAverageVec n x F i = boxAverage n x fun (y : HCPolySupport.Vec d) => F y i

theorem Algsuperdiff.Section4.Provider.Homogenization.boxAverage_eq_inv_mul_integral {d : ℕ} (n : ℤ) (x : HCPolySupport.Vec d) (f : HCPolySupport.Vec d → ℝ) : boxAverage n x f = ((3 ^ ↑n) ^ d)⁻¹ * ∫ (y : HCPolySupport.Vec d) in boxSet n x, f y

The unpacked form: the box integral divided by the box volume.

theorem Algsuperdiff.Section4.Provider.Homogenization.abs_boxAverage_le {d : ℕ} {n : ℤ} {x : HCPolySupport.Vec d} {f : HCPolySupport.Vec d → ℝ} {C : ℝ} (hf : ∀ y ∈ boxSet n x, |f y| ≤ C) : |boxAverage n x f| ≤ C

A uniform pointwise bound on the box passes to the average.

4. The translate-uniform negative gauge

def Algsuperdiff.Section4.Provider.Homogenization.UniformBoxGaugeBound {d : ℕ} (m : ℤ) (s A : ℝ) (F : HCPolySupport.Vec d → HCPolySupport.Vec d) : Prop

The translate-uniform negative gauge of order -s on the scales n ≤ m.

This is the manuscript's (∞,∞) negative Besov gauge with the inner maximum taken over all translates of the scale-n box rather than over the triadic grid alone. It is the carrier the mollifier calculus runs on: a mollifier centred at x averages against x + □_n, and no grid cube is available at a general centre.

Equations

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

theorem Algsuperdiff.Section4.Provider.Homogenization.UniformBoxGaugeBound.nonneg {d : ℕ} {m : ℤ} {s A : ℝ} {F : HCPolySupport.Vec d → HCPolySupport.Vec d} (h : UniformBoxGaugeBound m s A F) : 0 ≤ A

The gauge constant of a nonvacuous gauge is nonnegative.