HarmonicReplaceForcing

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

The birth-scale size of the harmonic replacement defect

HarmonicReplaceExistence bounds the normalized mean square of the correction grad phi = grad w - grad h by the normalized mean-square deviation of the forcing field G from an arbitrary constant. OscillationApproxForcing bounds the normalized mean-square oscillation of a Lipschitz forcing field on a cube of scale m by sqrt d * M * 3^m, where M bounds the differentials of the coordinates of G.

Choosing the arbitrary constant to be the cube average of G joins the two: the deviation becomes the oscillation, and the harmonic replacement defect inherits the birth-scale size 3^m. That is exactly the hypothesis hE of OscillationTelescope.le_zpow_mul_add_nsmul_of_nested_decomposition, whose cancellation against the arbitrary-gap factor 3^{-j} is what makes the forcing in e.nablaw.oscillations accumulate linearly in the number of scales.

Contents

• memVectorL2_of_differentiable_coord_openCubeAtScale -- a coordinatewise differentiable field is L^2 on a cube.
• exists_h10Function_isWeaklyHarmonicOn_sub_sqrt_le -- the birth-scale atom in replacement form: the harmonic replacement exists and its gradient defect has normalized L^2 size at most sqrt d * M * 3^m.

Portability

This file depends only on Mathlib, on CoarseGraining (Homogenization.*) and on the harmonic/oscillation layer of this same directory. It mentions no object of the manuscript: no model, no cutoff, no shell, no corrector, no sigmaBar. The manuscript's factor sigmaBar^{-1} enters only when the abstract forcing G of this file is instantiated by the physical forcing, which happens nowhere here. It is intended to be portable into CoarseGraining by a single mechanical namespace rename.

References

• ABK26, e.nablaw.oscillations (the eventual consumer).

theorem Algsuperdiff.Section3.Provider.Diffusivity.Corrector.memVectorL2_of_differentiable_coord_openCubeAtScale {d : ℕ} {G : HCPolySupport.Vec d → HCPolySupport.Vec d} (hG : ∀ (i : Fin d), Differentiable ℝ fun (y : HCPolySupport.Vec d) => G y i) (z : HCPolySupport.Vec d) (m : ℤ) : HCPolySupport.MemVectorL2 (HCPolySupport.Book.Ch03.openCubeAtScale z m) G

A field whose coordinates are differentiable is square integrable on every cube: it is continuous, hence bounded on the compact closure.

theorem Algsuperdiff.Section3.Provider.Diffusivity.Corrector.exists_h10Function_isWeaklyHarmonicOn_sub_sqrt_le {d : ℕ} [NeZero d] (z : HCPolySupport.Vec d) (m : ℤ) (w : HCPolySupport.H1Function (HCPolySupport.Book.Ch03.openCubeAtScale z m)) {G : HCPolySupport.Vec d → HCPolySupport.Vec d} {M : ℝ} (hM : 0 ≤ M) (hGdiff : ∀ (i : Fin d), Differentiable ℝ fun (y : HCPolySupport.Vec d) => G y i) (hGbound : ∀ x ∈ HCPolySupport.Book.Ch03.openCubeAtScale z m, ∀ (i : Fin d), ‖fderiv ℝ (fun (y : HCPolySupport.Vec d) => G y i) x‖ ≤ M) (hw : ∀ (ψ : HCPolySupport.H10Function (HCPolySupport.Book.Ch03.openCubeAtScale z m)), ∫ (x : HCPolySupport.Vec d) in HCPolySupport.Book.Ch03.openCubeAtScale z m, HCPolySupport.vecDot (w.grad x) (ψ.grad x) = ∫ (x : HCPolySupport.Vec d) in HCPolySupport.Book.Ch03.openCubeAtScale z m, HCPolySupport.vecDot (G x) (ψ.grad x)) : ∃ (φ : HCPolySupport.H10Function (HCPolySupport.Book.Ch03.openCubeAtScale z m)), IsWeaklyHarmonicOn (HCPolySupport.Book.Ch03.openCubeAtScale z m) (w - φ.toH1Function).toFun ∧ √(HCPolySupport.Book.Ch01.meanSquareDeviationVecOn (HCPolySupport.Book.Ch03.openCubeAtScale z m) φ.grad 0) ≤ √↑d * M * 3 ^ m

The birth-scale atom in harmonic-replacement form.

Let w be an H^1 function on the cube z + cu_m which weakly solves - Delta w = div G there, and suppose the differential of every coordinate of the forcing G has operator norm at most M on the cube. Then w admits a harmonic replacement w - phi on the cube whose gradient defect obeys

  || grad phi ||_{L2bar (z + cu_m)} <= sqrt d * M * 3^m .

The proof runs the harmonic replacement of HarmonicReplaceExistence with the recentring constant chosen to be the cube average of G, so that the energy bound is stated against the mean-square oscillation of G, and then applies the mean-value forcing atom of OscillationApproxForcing.