CoarseGaugeNullLagrangian

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

Provider: the constant-skew null Lagrangian, and the shifted harmonic class

The coefficient shift a |-> a - hbar of ABK26 is only useful because it does not move the admissible class: for a constant skew hbar the field x |-> hbar grad u (x) is divergence free in the weak sense, so an a-harmonic function is (a - hbar)-harmonic and conversely. Equivalently,

int_U hbar grad u . grad phi = 0   for  u in H^1(U),  phi in H^1_0(U).

This is the standard null-Lagrangian cancellation: pairing the constant skew matrix against the Hessian of a smooth test kills the integrand by the symmetry of second derivatives, and both sides are L^2-continuous in the test.

• isSolenoidalOn_matVecMul_of_isPotentialOn_of_transpose_eq_neg, the display above, obtained from Homogenization.IsSolenoidalOn.of_test_of_contDiff_of_memVectorL2 by testing against smooth compactly supported functions and integrating by parts once in each slot; and
• isAHarmonicGradient_sub_const_skew, its consequence for the harmonic class of Homogenization.PDE.Harmonic.

Only Homogenization.euclideanCoordSecondDeriv_comm_fun (symmetry of second derivatives of a smooth function) and the weak-gradient identity of Homogenization.H1Function are used; no ellipticity enters.

L² bookkeeping

theorem Algsuperdiff.Section3.Provider.Diffusivity.ApproximateRecurrence.memVectorL2_matVecMul_const {d : ℕ} {U : Set (HCPolySupport.Vec d)} (H : HCPolySupport.Mat d) {w : HCPolySupport.Vec d → HCPolySupport.Vec d} (hw : HCPolySupport.MemVectorL2 U w) : HCPolySupport.MemVectorL2 U fun (x : HCPolySupport.Vec d) => HCPolySupport.matVecMul H (w x)

A constant matrix applied to an L² vector field stays in L².

theorem Algsuperdiff.Section3.Provider.Diffusivity.ApproximateRecurrence.h10FluxIntegrable_of_memVectorL2 {d : ℕ} {U : Set (HCPolySupport.Vec d)} {F : HCPolySupport.Vec d → HCPolySupport.Vec d} (hF : HCPolySupport.MemVectorL2 U F) : HCPolySupport.h10FluxIntegrable U F

An L² vector field pairs integrably against every H^1_0 test gradient.

theorem Algsuperdiff.Section3.Provider.Diffusivity.ApproximateRecurrence.isSolenoidalOn_sub {d : ℕ} {U : Set (HCPolySupport.Vec d)} {F G : HCPolySupport.Vec d → HCPolySupport.Vec d} (hF : HCPolySupport.IsSolenoidalOn U F) (hG : HCPolySupport.IsSolenoidalOn U G) (hFint : HCPolySupport.h10FluxIntegrable U F) (hGint : HCPolySupport.h10FluxIntegrable U G) : HCPolySupport.IsSolenoidalOn U fun (x : HCPolySupport.Vec d) => F x - G x

Difference of two weakly divergence-free fields with integrable pairings.

The null Lagrangian

theorem Algsuperdiff.Section3.Provider.Diffusivity.ApproximateRecurrence.isSolenoidalOn_matVecMul_of_isPotentialOn_of_transpose_eq_neg {d : ℕ} {U : Set (HCPolySupport.Vec d)} (hU : IsOpen U) {H : HCPolySupport.Mat d} (hH : HCPolySupport.matTranspose H = -H) {f : HCPolySupport.Vec d → HCPolySupport.Vec d} (hf : HCPolySupport.IsPotentialOn U f) : HCPolySupport.IsSolenoidalOn U fun (x : HCPolySupport.Vec d) => HCPolySupport.matVecMul H (f x)

The constant-skew null Lagrangian: for constant skew H and a potential field f = grad u on U, the field H f is weakly divergence free on U.

This is the exact vanishing that makes the shift a |-> a - hbar of ABK26 preserve the admissible class.

The shifted harmonic class

theorem Algsuperdiff.Section3.Provider.Diffusivity.ApproximateRecurrence.isAHarmonicGradient_sub_const_skew {d : ℕ} {U : Set (HCPolySupport.Vec d)} (hU : IsOpen U) {H : HCPolySupport.Mat d} (hH : HCPolySupport.matTranspose H = -H) {c : HCPolySupport.CoeffField d} {f : HCPolySupport.Vec d → HCPolySupport.Vec d} (hflux : HCPolySupport.MemVectorL2 U fun (x : HCPolySupport.Vec d) => HCPolySupport.matVecMul (c x) (f x)) (hf : HCPolySupport.IsAHarmonicGradient c U f) : HCPolySupport.IsAHarmonicGradient (fun (x : HCPolySupport.Vec d) => c x - H) U f

Subtracting a constant skew matrix from the coefficient field does not move the harmonic class.