HomMollifyPairing

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 mollifier's pairing against the gauge

The core lemma of this file

The mollifier calculus needs one estimate, and this module proves it:

The kernel pairing. If the vector field F obeys the translate-uniform negative gauge ‖(F)_{y+□_n}‖ ≤ A 3^{-ns} at the scale n, then for every probability density ψ (nonnegative, unit mass) the ψ-mixture of the scale-n box averages of F obeys the same bound:

  ‖∫ ψ(z) (F)_{x-z+□_n} dz‖ ≤ A · 3^{-ns}   for every x.

(norm_boxMixtureVec_le_of_uniformBoxGauge, constant exactly 1.)

The mechanism is the manuscript's own: a mollifier at scale 3^n is a superposition of translated scale-n box averages, and the negative gauge is by definition a uniform bound on each of them. No dimensional constant is lost, because a probability density has unit mass; the dimensional factor C(d) of this file enters only later, when the gradient vector is paired against a displacement in the supremum norm (HomMollifyGradient).

The identification of a mollifier with such a superposition is convolution_boxKernel_eq_boxAverage below: convolving with the normalized indicator boxKernel n of the scale-n box is the sliding box average, so convolving with ψ ⋆ boxKernel n is the ψ-mixture of those averages. ψ ⋆ boxKernel n is smooth whenever ψ is, which is what makes the family admissible as a test function against the weak gradient.

The reconstruction residue

The gauge used here is the translate gauge UniformBoxGaugeBound, not the grid gauge negBesovInftyNorm. The missing implication is exactly:

  RECONSTRUCTION.  Let F ∈ L¹_loc(□_m).  Suppose that for every n ≤ m and
  every triadic cube R ⊆ □_m of scale n one has ‖(F)_R‖ ≤ A 3^{-ns}.  Then
  for every n ≤ m and every x with x + □_n ⊆ □_m,
      ‖(F)_{x+□_n}‖ ≤ C(d) · (1 + (1 - 3^{-(1-s)})⁻¹) · A · 3^{-ns}.

Its proof is the triadic martingale decomposition F = Σ_k (E_k F - E_{k-1}F) (CoarseGraining's cubeProjection, whose a.e. convergence is ae_tendsto_cubeProjection_of_integrableOn): the term E_n F is bounded by the grid hypothesis directly, and each finer increment E_k F - E_{k-1} F has mean zero on every grid cube of scale k+1, so only the O(3^{(n-k)(d-1)}) cubes straddling ∂(x + □_n) contribute, giving the geometric factor 3^{k-n} and the sum Σ_{k<n} 3^{k(1-s)}·3^{-n} = 3^{-ns}·(1-3^{-(1-s)})⁻¹.

It is not formalized in this file. The ingredients absent from the tree are the boundary-layer count for the straddling cubes and the L¹ convergence of the triadic projections; CoarseGraining supplies cubeProjection and its a.e. convergence but neither of the other two. Consumers must therefore either harvest the Step-3 estimate at all translates (which the coarse-graining machinery does supply — the source estimate is not grid-bound) or discharge the reconstruction separately.

Main definitions and results

• boxKernel n — the normalized indicator of the scale-n box at the origin, with integrable_boxKernel and locallyIntegrable_boxKernel.
• convolution_boxKernel_eq_boxAverage — unconditionally, convolving with boxKernel n is the sliding scale-n box average.
• boxMixture, boxMixtureVec — the ψ-mixture of sliding box averages, and boxMixture_eq_convolution.
• abs_boxMixture_le — a uniform bound on the box averages passes to the mixture, with no integrability hypothesis (the Bochner integral of a non-integrable function is 0, which obeys the bound as well).
• norm_boxMixtureVec_le_of_uniformBoxGauge — the kernel pairing.

References

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

1. The box kernel

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

The scale-n box kernel: the normalized indicator of the box of side 3^n centred at the origin. Convolution with it is the sliding box average (convolution_boxKernel_eq_boxAverage).

Equations

• Algsuperdiff.Section4.Provider.Homogenization.boxKernel n = (Algsuperdiff.Section4.Provider.Homogenization.boxSet n 0).indicator fun (x : HCPolySupport.Vec d) => ((3 ^ ↑n) ^ d)⁻¹

theorem Algsuperdiff.Section4.Provider.Homogenization.boxKernel_def {d : ℕ} (n : ℤ) : boxKernel n = (boxSet n 0).indicator fun (x : HCPolySupport.Vec d) => ((3 ^ ↑n) ^ d)⁻¹

theorem Algsuperdiff.Section4.Provider.Homogenization.boxKernel_apply_of_mem {d : ℕ} {n : ℤ} {z : HCPolySupport.Vec d} (hz : z ∈ boxSet n 0) : boxKernel n z = ((3 ^ ↑n) ^ d)⁻¹

theorem Algsuperdiff.Section4.Provider.Homogenization.boxKernel_apply_of_not_mem {d : ℕ} {n : ℤ} {z : HCPolySupport.Vec d} (hz : z ∉ boxSet n 0) : boxKernel n z = 0

theorem Algsuperdiff.Section4.Provider.Homogenization.integrable_boxKernel {d : ℕ} (n : ℤ) : MeasureTheory.Integrable (boxKernel n) MeasureTheory.volume

theorem Algsuperdiff.Section4.Provider.Homogenization.locallyIntegrable_boxKernel {d : ℕ} (n : ℤ) : MeasureTheory.LocallyIntegrable (boxKernel n) MeasureTheory.volume

2. Convolution with the box kernel is the sliding box average

theorem Algsuperdiff.Section4.Provider.Homogenization.convolution_boxKernel_eq_boxAverage {d : ℕ} (n : ℤ) (f : HCPolySupport.Vec d → ℝ) (x : HCPolySupport.Vec d) : MeasureTheory.convolution (boxKernel n) f (ContinuousLinearMap.lsmul ℝ ℝ) MeasureTheory.volume x = boxAverage n x f

The identification. Convolving f with the scale-n box kernel produces exactly the sliding scale-n box average of f. No hypothesis on f is needed: both sides are the same Bochner integral.

3. The mixture of sliding box averages

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

The ψ-mixture of the sliding scale-n box averages of f: the value at x of the convolution of ψ with the sliding average.

Equations

• Algsuperdiff.Section4.Provider.Homogenization.boxMixture n ψ f x = ∫ (z : HCPolySupport.Vec d), ψ z * Algsuperdiff.Section4.Provider.Homogenization.boxAverage n (x - z) f

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

The coordinatewise mixture of a vector field.

Equations

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

theorem Algsuperdiff.Section4.Provider.Homogenization.boxMixture_def {d : ℕ} (n : ℤ) (ψ f : HCPolySupport.Vec d → ℝ) (x : HCPolySupport.Vec d) : boxMixture n ψ f x = ∫ (z : HCPolySupport.Vec d), ψ z * boxAverage n (x - z) f

theorem Algsuperdiff.Section4.Provider.Homogenization.boxMixtureVec_apply {d : ℕ} (n : ℤ) (ψ : HCPolySupport.Vec d → ℝ) (F : HCPolySupport.Vec d → HCPolySupport.Vec d) (x : HCPolySupport.Vec d) (i : Fin d) : boxMixtureVec n ψ F x i = boxMixture n ψ (fun (y : HCPolySupport.Vec d) => F y i) x

theorem Algsuperdiff.Section4.Provider.Homogenization.boxMixture_eq_convolution {d : ℕ} (n : ℤ) (ψ f : HCPolySupport.Vec d → ℝ) (x : HCPolySupport.Vec d) : boxMixture n ψ f x = MeasureTheory.convolution ψ (fun (y : HCPolySupport.Vec d) => boxAverage n y f) (ContinuousLinearMap.lsmul ℝ ℝ) MeasureTheory.volume x

The mixture is the convolution of ψ with the sliding average.

theorem Algsuperdiff.Section4.Provider.Homogenization.integrable_of_integral_eq_one {d : ℕ} {ψ : HCPolySupport.Vec d → ℝ} (hψ1 : ∫ (z : HCPolySupport.Vec d), ψ z = 1) : MeasureTheory.Integrable ψ MeasureTheory.volume

A density of unit mass is integrable (otherwise its integral would be zero by the junk-value convention).

4. The kernel pairing

theorem Algsuperdiff.Section4.Provider.Homogenization.abs_boxMixture_le {d : ℕ} {n : ℤ} {ψ f : HCPolySupport.Vec d → ℝ} {B : ℝ} (hB : 0 ≤ B) (hψ0 : ∀ (z : HCPolySupport.Vec d), 0 ≤ ψ z) (hψ1 : ∫ (z : HCPolySupport.Vec d), ψ z = 1) (hbd : ∀ (y : HCPolySupport.Vec d), |boxAverage n y f| ≤ B) (x : HCPolySupport.Vec d) : |boxMixture n ψ f x| ≤ B

The scalar kernel pairing. A uniform bound B on the sliding scale-n box averages of f passes to every mixture of them against a probability density, at constant exactly 1.

No integrability hypothesis on the mixture is required: when the mixing integral fails to converge the Bochner integral is 0, which obeys the bound.

theorem Algsuperdiff.Section4.Provider.Homogenization.norm_boxMixtureVec_le_of_uniformBoxGauge {d : ℕ} {m : ℤ} {s A : ℝ} {F : HCPolySupport.Vec d → HCPolySupport.Vec d} (h : UniformBoxGaugeBound m s A F) {n : ℤ} (hn : n ≤ m) {ψ : HCPolySupport.Vec d → ℝ} (hψ0 : ∀ (z : HCPolySupport.Vec d), 0 ≤ ψ z) (hψ1 : ∫ (z : HCPolySupport.Vec d), ψ z = 1) (x : HCPolySupport.Vec d) : ‖boxMixtureVec n ψ F x‖ ≤ A * 3 ^ (-(↑n * s))

THE KERNEL PAIRING.

If the vector field F obeys the translate-uniform negative gauge of order -s on the scales ≤ m, then at every scale n ≤ m and every point x, the mixture of the sliding scale-n box averages of F against any probability density ψ obeys the same bound A · 3^{-ns}.

The constant is exactly 1: a mollifier at scale 3^n is a superposition of translated scale-n box averages of total mass one, and the gauge bounds each of them.