OscillationNestedTransport

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

Moving the weak equation from the coarse cube to every finer concentric cube

The nested-recentring route of OscillationTelescope builds one harmonic replacement per scale: on each cube U_j = z + cu_{n+j} of the concentric family it subtracts from the corrector w the H^1_0(U_j) potential of the forcing. The construction (HarmonicReplaceForcing) needs the weak equation int <grad w, grad psi> = int <G, grad psi> on U_j, tested against H^1_0(U_j), whereas the corrector solves its equation only on the coarse cube U_N, tested against the larger class H^1_0(U_N).

The passage is a restriction of the test class along the extension by zero. It is already available inside CoarseGraining, in the solenoidality language: CoarseGraining's IsSolenoidalOn U g is literally "int_U <g, grad phi> = 0 for every phi in H^1_0(U)", and Homogenization.IsSolenoidalOn.restrict_of_isOpen_of_memVectorL2 restricts it to any open subset with L^2 control there. Its proof is the extension-by-zero argument in the only form that is needed: a smooth test function supported in the subdomain is already a legal test function upstairs, and the two set integrals agree because the integrand vanishes off the support.

So no new Sobolev extension operator has to be built. What this module supplies is the translation between the two shapes -- the manuscript writes an equation with a right-hand side, CoarseGraining's predicate is homogeneous -- and the specialization to the concentric cube family, packaged so that the per-scale harmonic replacement can be produced directly from the coarse equation.

Contents

• memVectorL2_mono -- L^2 control passes to subsets.
• forall_h10Function_integral_vecDot_grad_eq_of_subset -- the transport: the weak equation with right-hand side, moved to an open subset.
• exists_h10Function_isWeaklyHarmonicOn_sub_sqrt_le_subcube -- the per-scale harmonic replacement on a finer concentric cube, produced from the equation on the coarse one, with the birth-scale defect bound 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. 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_mono {d : ℕ} {U V : Set (HCPolySupport.Vec d)} (hVU : V ⊆ U) {f : HCPolySupport.Vec d → HCPolySupport.Vec d} (hf : HCPolySupport.MemVectorL2 U f) : HCPolySupport.MemVectorL2 V f

Square integrability on a set passes to subsets.

theorem Algsuperdiff.Section3.Provider.Diffusivity.Corrector.forall_h10Function_integral_vecDot_grad_eq_of_subset {d : ℕ} {U V : Set (HCPolySupport.Vec d)} (hU : IsOpen U) (hV : IsOpen V) (hVU : V ⊆ U) {A G : HCPolySupport.Vec d → HCPolySupport.Vec d} (hA : HCPolySupport.MemVectorL2 U A) (hG : HCPolySupport.MemVectorL2 U G) (hw : ∀ (ψ : HCPolySupport.H10Function U), ∫ (x : HCPolySupport.Vec d) in U, HCPolySupport.vecDot (A x) (ψ.grad x) = ∫ (x : HCPolySupport.Vec d) in U, HCPolySupport.vecDot (G x) (ψ.grad x)) (ψ : HCPolySupport.H10Function V) : ∫ (x : HCPolySupport.Vec d) in V, HCPolySupport.vecDot (A x) (ψ.grad x) = ∫ (x : HCPolySupport.Vec d) in V, HCPolySupport.vecDot (G x) (ψ.grad x)

Transport of the weak equation to an open subset.

If a field A solves int_U <A, grad psi> = int_U <G, grad psi> against every H^1_0(U) competitor, then it solves the same equation on every open subset V of U against every H^1_0(V) competitor.

The proof rewrites the equation as the solenoidality of A - G, applies CoarseGraining's restriction of solenoidality along the extension by zero, and splits the pairing back into its two halves.

theorem Algsuperdiff.Section3.Provider.Diffusivity.Corrector.exists_h10Function_isWeaklyHarmonicOn_sub_sqrt_le_subcube {d : ℕ} [NeZero d] (z : HCPolySupport.Vec d) {m m' : ℤ} (hmm : m' ≤ 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.restrict ⋯ ⋯ - φ.toH1Function).toFun ∧ √(HCPolySupport.Book.Ch01.meanSquareDeviationVecOn (HCPolySupport.Book.Ch03.openCubeAtScale z m') φ.grad 0) ≤ √↑d * M * 3 ^ m'

The per-scale harmonic replacement on a finer concentric cube.

Let w be an H^1 function on the cube z + cu_m which weakly solves - Delta w = div G there, and let m' <= m. Then the restriction of w to the concentric cube z + cu_{m'} admits a harmonic replacement whose gradient defect has normalized L^2 size at most sqrt d * M * 3^{m'} on that cube, M being a bound for the differentials of the coordinates of the forcing.

This is the birth-scale atom of HarmonicReplaceForcing, made available at every scale of the concentric family from the single equation on the coarse cube.