HomMollifySwap

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 two swaps of the mollifier calculus

What this module proves

Two exchange identities carry the whole mollifier calculus.

(S1) The averaging swap. For a mollifier ψ and a field f,

  (f ⋆ ψ)_{x+□_n}  =  ∫ ψ(z) · (f)_{x-z+□_n} dz.

The box average of a mollification is the ψ-mixture of the box averages — i.e. the mollifier commutes with the sliding average. This is boxAverage_convolution_eq_boxMixture, and it is exactly what turns the manuscript's cube-average gauge into a bound on the mollified gradient: combined with the kernel pairing of HomMollifyPairing it yields norm_boxAverageVec_convolution_le_of_uniformBoxGauge, this file's working form of the core estimate.

(S2) The weak-gradient swap. For w with weak gradient G on the whole space and a smooth compactly supported kernel Θ,

  ∫ w(y) (∂_i Θ)(x - y) dy  =  ∫ G_i(y) Θ(x - y) dy,

i.e. ∂_i(Θ ⋆ w) = Θ ⋆ G_i. This is integral_mul_fderiv_sub_eq_integral_weakGrad; it is the only place where the Sobolev regularity of w is used, and it is a single application of HasWeakPartialDerivOn to the test function y ↦ Θ(x - y).

Together: the gradient of the mollification of w at scale 3^n is the mixture of the scale-n box averages of ∇w, hence is bounded by A · 3^{-ns} under the translate-uniform gauge.

The H¹₀ frame

The hypothesis HasWeakGradientOn Set.univ w G is not an extra assumption on the Step-3 object: for w = u - v ∈ H¹₀(□_m) — which is exactly the manuscript's hypothesis in the paper — CoarseGraining's H10Function.hasWeakGradientOn_univ_zeroExtension supplies it for the extension of w by zero, together with MemLp for w and ∇w, whence their integrability (compact support).

References

• ABK26, Theorem B Step 3.

1. Commutativity of the scalar convolution

theorem Algsuperdiff.Section4.Provider.Homogenization.lsmul_flip_eq_lsmul : (ContinuousLinearMap.lsmul ℝ ℝ).flip = ContinuousLinearMap.lsmul ℝ ℝ

The scalar convolution pairing is its own flip.

theorem Algsuperdiff.Section4.Provider.Homogenization.convolution_comm_real {d : ℕ} (f g : HCPolySupport.Vec d → ℝ) : MeasureTheory.convolution f g (ContinuousLinearMap.lsmul ℝ ℝ) MeasureTheory.volume = MeasureTheory.convolution g f (ContinuousLinearMap.lsmul ℝ ℝ) MeasureTheory.volume

Scalar convolution is commutative.

2. Associativity for a bounded integrable mollifier

theorem Algsuperdiff.Section4.Provider.Homogenization.convolution_assoc_real {d : ℕ} {f g k : HCPolySupport.Vec d → ℝ} {C : ℝ} (hf : MeasureTheory.Integrable f MeasureTheory.volume) (hg : MeasureTheory.Integrable g MeasureTheory.volume) (hk : MeasureTheory.Integrable k MeasureTheory.volume) (hfb : ∀ (t : HCPolySupport.Vec d), ‖f t‖ ≤ C) (x₀ : HCPolySupport.Vec d) : MeasureTheory.convolution (MeasureTheory.convolution f g (ContinuousLinearMap.lsmul ℝ ℝ) MeasureTheory.volume) k (ContinuousLinearMap.lsmul ℝ ℝ) MeasureTheory.volume x₀ = MeasureTheory.convolution f (MeasureTheory.convolution g k (ContinuousLinearMap.lsmul ℝ ℝ) MeasureTheory.volume) (ContinuousLinearMap.lsmul ℝ ℝ) MeasureTheory.volume x₀

Associativity of the scalar convolution when the outer factor is bounded and all three factors are integrable.

3. (S1) The averaging swap

theorem Algsuperdiff.Section4.Provider.Homogenization.boxAverage_convolution_eq_boxMixture {d : ℕ} (n : ℤ) {ψ f : HCPolySupport.Vec d → ℝ} {C : ℝ} (hψ : MeasureTheory.Integrable ψ MeasureTheory.volume) (hf : MeasureTheory.Integrable f MeasureTheory.volume) (hψb : ∀ (t : HCPolySupport.Vec d), ‖ψ t‖ ≤ C) (x : HCPolySupport.Vec d) : boxAverage n x (MeasureTheory.convolution f ψ (ContinuousLinearMap.lsmul ℝ ℝ) MeasureTheory.volume) = boxMixture n ψ f x

The averaging swap. The scale-n box average of the mollification f ⋆ ψ is the ψ-mixture of the scale-n box averages of f:

  (f ⋆ ψ)_{x+□_n} = ∫ ψ(z) (f)_{x-z+□_n} dz.

This is the precise sense in which "a mollifier at scale 3^n is a superposition of translated scale-n box averages", and it is the identity that lets the manuscript's cube-average gauge control a mollified field.

4. The pairing in convolution form

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

The coordinatewise mollification of a vector field.

Equations

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

theorem Algsuperdiff.Section4.Provider.Homogenization.convolutionVec_apply {d : ℕ} (ψ : HCPolySupport.Vec d → ℝ) (F : HCPolySupport.Vec d → HCPolySupport.Vec d) (x : HCPolySupport.Vec d) (i : Fin d) : convolutionVec ψ F x i = MeasureTheory.convolution (fun (y : HCPolySupport.Vec d) => F y i) ψ (ContinuousLinearMap.lsmul ℝ ℝ) MeasureTheory.volume x

theorem Algsuperdiff.Section4.Provider.Homogenization.norm_boxAverageVec_convolution_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 → ℝ} {C : ℝ} (hψ : MeasureTheory.Integrable ψ MeasureTheory.volume) (hψb : ∀ (t : HCPolySupport.Vec d), ‖ψ t‖ ≤ C) (hψ0 : ∀ (z : HCPolySupport.Vec d), 0 ≤ ψ z) (hψ1 : ∫ (z : HCPolySupport.Vec d), ψ z = 1) (hF : ∀ (i : Fin d), MeasureTheory.Integrable (fun (y : HCPolySupport.Vec d) => F y i) MeasureTheory.volume) (x : HCPolySupport.Vec d) : ‖boxAverageVec n x (convolutionVec ψ F)‖ ≤ A * 3 ^ (-(↑n * s))

THE CORE ESTIMATE IN CONVOLUTION FORM.

If the vector field F obeys the translate-uniform negative gauge of order -s on the scales ≤ m, then for every scale n ≤ m, every probability density ψ that is integrable and bounded, and every point x, the scale-n box average of the mollification F ⋆ ψ obeys

  ‖(F ⋆ ψ)_{x+□_n}‖ ≤ A · 3^{-ns}.

The constant is exactly 1: the mollification is a mass-one superposition of translated box averages, each bounded by the gauge.

5. (S2) The weak-gradient swap

theorem Algsuperdiff.Section4.Provider.Homogenization.integral_mul_fderiv_sub_eq_integral_weakGrad {d : ℕ} {w : HCPolySupport.Vec d → ℝ} {G : HCPolySupport.Vec d → HCPolySupport.Vec d} (hw : HCPolySupport.HasWeakGradientOn Set.univ w G) {Θ : HCPolySupport.Vec d → ℝ} (hΘ : ContDiff ℝ (↑⊤) Θ) (hΘc : HasCompactSupport Θ) (i : Fin d) (x : HCPolySupport.Vec d) : ∫ (y : HCPolySupport.Vec d), w y * (fderiv ℝ Θ (x - y)) (HCPolySupport.basisVec i) = ∫ (y : HCPolySupport.Vec d), G y i * Θ (x - y)

The weak-gradient swap. If w has weak gradient G on the whole space and Θ is a smooth compactly supported kernel, then

  ∫ w(y) (∂_i Θ)(x - y) dy = ∫ G_i(y) Θ(x - y) dy,

i.e. differentiating the mollification Θ ⋆ w hits the kernel on the left and the weak gradient on the right. This is a single application of the definition of the weak partial derivative to the test function y ↦ Θ(x - y).

For the Step-3 object w = u - v ∈ H¹₀(□_m) the hypothesis is CoarseGraining's H10Function.hasWeakGradientOn_univ_zeroExtension.