OscillationApproxForcing

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

The birth-scale forcing atom on a concentric cube

The second term of e.nablaw.oscillations is

  C shom_{m-h}^{-1} (m-h-n) 3^n || grad (k_m - k_{m-h}) ||_{L^inf (z + cu_{m-h})} .

Its per-scale atom is the normalized L^2 oscillation of the forcing field on the cube of that scale, and the factor 3^{scale} in front of the L^inf gradient is exactly the Poincare constant of the cube in its crudest, sup-norm form. That is what this module proves:

  || F - (F)_{z + cu_m} ||_{L2bar (z + cu_m)}
      <= sqrt d * 3^m * sup_{z + cu_m} || D F || .

The cube is convex (OscillationCubeFamily.convex_openCubeAtScale) and has sup-norm diameter 3^m (OscillationDecayAverage.norm_sub_le_of_mem_openCubeAtScale), so the convex mean-value inequality gives the pointwise bound at once; the only further ingredients are the pointwise-to-mean-square step and the mean recentring of OscillationDecayAverage. No Poincare inequality in Sobolev form and no capacity argument is needed, because the forcing is controlled in L^inf already.

This is one half of the harmonic-approximation step, not the whole of it. The other half -- solving -Delta phi = div ((F - c) 1_U) in H^1_0 (U) so that w - phi becomes harmonic on U, with the energy estimate || grad w - grad (w - phi) ||_{L2bar (U)} <= || F - (F)_U ||_{L2bar (U)} -- is not proved here and is not used here. See the disclosure.

Contents

• meanSquareDeviationVecOn_center_le_of_norm_fderiv_le -- the pointwise mean-value step, in mean-square form and centred at the cube centre.
• sqrt_meanSquareOscillationVecOn_le_of_norm_fderiv_le -- the forcing atom, in the norm form <= sqrt d * M * 3^m that the accumulation of OscillationTelescope consumes as its birth-scale hypothesis hE.

References

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

theorem Algsuperdiff.Section3.Provider.Diffusivity.Corrector.meanSquareDeviationVecOn_center_le_of_norm_fderiv_le {d : ℕ} {F : HCPolySupport.Vec d → HCPolySupport.Vec d} {M : ℝ} (hM : 0 ≤ M) (hF : ∀ (i : Fin d), Differentiable ℝ fun (y : HCPolySupport.Vec d) => F y i) (z : HCPolySupport.Vec d) (m : ℤ) (hbound : ∀ x ∈ HCPolySupport.Book.Ch03.openCubeAtScale z m, ∀ (i : Fin d), ‖fderiv ℝ (fun (y : HCPolySupport.Vec d) => F y i) x‖ ≤ M) : HCPolySupport.Book.Ch01.meanSquareDeviationVecOn (HCPolySupport.Book.Ch03.openCubeAtScale z m) F (F z) ≤ (√↑d * M * 3 ^ m) ^ 2

The mean-value step on the convex cube.

If every coordinate of F has differential of operator norm at most M on the cube z + cu_m, then the mean-square deviation of F from its value at the centre is at most d M^2 3^{2m}.

theorem Algsuperdiff.Section3.Provider.Diffusivity.Corrector.sqrt_meanSquareOscillationVecOn_le_of_norm_fderiv_le {d : ℕ} {F : HCPolySupport.Vec d → HCPolySupport.Vec d} {M : ℝ} (hM : 0 ≤ M) (hF : ∀ (i : Fin d), Differentiable ℝ fun (y : HCPolySupport.Vec d) => F y i) (z : HCPolySupport.Vec d) (m : ℤ) (hbound : ∀ x ∈ HCPolySupport.Book.Ch03.openCubeAtScale z m, ∀ (i : Fin d), ‖fderiv ℝ (fun (y : HCPolySupport.Vec d) => F y i) x‖ ≤ M) : √(HCPolySupport.Book.Ch01.meanSquareOscillationVecOn (HCPolySupport.Book.Ch03.openCubeAtScale z m) F) ≤ √↑d * M * 3 ^ m

The birth-scale forcing atom.

|| F - (F)_{z + cu_m} ||_{L2bar (z + cu_m)} <= sqrt d * M * 3^m whenever the differential of every coordinate of F has operator norm at most M on the cube. With m = n + j this is exactly the birth-scale hypothesis E j <= c * 3^{n+j} of OscillationTelescope.le_zpow_mul_add_nsmul_of_nested_decomposition, with the scale-independent constant c = sqrt d * M; the linear-in-N accumulation of that module is what turns it into the printed (m-h-n) 3^n factor.