H10SkewDivergence

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

Weak divergence of an antisymmetric matrix of H¹₀ potentials

This file supplies the model-free analytic core for the G leg of the piecewise-affine competitor. Given scalar potentials u i ∈ H¹₀(U), it represents the weak divergence of

Dᵢⱼ = (d - 1)⁻¹ (qⱼ uᵢ - qᵢ uⱼ)

directly through their weak gradients. Antisymmetry and the commutation of mixed weak derivatives imply that this vector field is in the public L²_sol,0(U) class.

The construction is independent of the Section 3 geometry. A later file may identify particular H¹₀ potentials with the superposed piecewise-affine competitor and then transport the conclusion by almost-everywhere equality.

Algebraic construction and L² membership

noncomputable def Algsuperdiff.Section3.Provider.Affine.h10SkewDimInv (d : ℕ) : ℝ

The manuscript normalization (d - 1)⁻¹ in the antisymmetric matrix Dᵢⱼ = (d - 1)⁻¹ (qⱼ uᵢ - qᵢ uⱼ).

Equations

• Algsuperdiff.Section3.Provider.Affine.h10SkewDimInv d = 1 / (↑d - 1)

def Algsuperdiff.Section3.Provider.Affine.skewGradientField {d : ℕ} (g : HCPolySupport.Vec d → HCPolySupport.Vec d) (a b : Fin d) : HCPolySupport.Vec d → HCPolySupport.Vec d

The skew-gradient vector field (∂_b u) e_a - (∂_a u) e_b.

Equations

• Algsuperdiff.Section3.Provider.Affine.skewGradientField g a b x = g x b • HCPolySupport.basisVec a - g x a • HCPolySupport.basisVec b

noncomputable def Algsuperdiff.Section3.Provider.Affine.h10SkewMatrixDiv {d : ℕ} {U : Set (HCPolySupport.Vec d)} (u : Fin d → HCPolySupport.H10Function U) (q : HCPolySupport.Vec d) : HCPolySupport.Vec d → HCPolySupport.Vec d

The weak divergence of the antisymmetric matrix (q_j u_i - q_i u_j)/(d-1), represented directly by the weak gradients of the zero-trace scalar potentials.

Equations

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

theorem Algsuperdiff.Section3.Provider.Affine.memVectorL2_h10SkewMatrixDiv {d : ℕ} {U : Set (HCPolySupport.Vec d)} (u : Fin d → HCPolySupport.H10Function U) (q : HCPolySupport.Vec d) : HCPolySupport.MemVectorL2 U (h10SkewMatrixDiv u q)

The weak skew-divergence correction is an L² vector field.

theorem Algsuperdiff.Section3.Provider.Affine.h10SkewMatrixDiv_apply {d : ℕ} {U : Set (HCPolySupport.Vec d)} (u : Fin d → HCPolySupport.H10Function U) (q x : HCPolySupport.Vec d) (k : Fin d) : h10SkewMatrixDiv u q x k = h10SkewDimInv d * (q k * ∑ i : Fin d, (u i).grad x i - ∑ i : Fin d, q i * (u k).grad x i)

Coordinate formula for the weak divergence of the antisymmetric matrix.

Commutation of mixed weak gradients

theorem Algsuperdiff.Section3.Provider.Affine.integral_grad_swap {d : ℕ} {U : Set (HCPolySupport.Vec d)} (u : HCPolySupport.H10Function U) (φ : HCPolySupport.H1Function U) (a b : Fin d) : ∫ (x : HCPolySupport.Vec d) in U, φ.grad x a * u.grad x b = ∫ (x : HCPolySupport.Vec d) in U, φ.grad x b * u.grad x a

Mixed weak derivatives commute after pairing an H¹₀ function with an arbitrary H¹ function.

Zero-normal solenoidality

instance Algsuperdiff.Section3.Provider.Affine.instHolderTripleOfNatENNReal_leanPool : ENNReal.HolderTriple 2 2 1

theorem Algsuperdiff.Section3.Provider.Affine.solenoidalZeroNormalTraceFieldOn_h10SkewMatrixDiv {d : ℕ} {U : Set (HCPolySupport.Vec d)} (u : Fin d → HCPolySupport.H10Function U) (q : HCPolySupport.Vec d) : HCPolySupport.Book.Ch01.SolenoidalZeroNormalTraceFieldOn U (h10SkewMatrixDiv u q)

The weak divergence of the antisymmetric H¹₀ matrix belongs to the public L² solenoidal space with zero normal trace.

theorem Algsuperdiff.Section3.Provider.Affine.solenoidalZeroNormalTraceFieldOn_congr_ae {d : ℕ} {U : Set (HCPolySupport.Vec d)} {f g : HCPolySupport.Vec d → HCPolySupport.Vec d} (hfg : f =ᵐ[HCPolySupport.volumeMeasureOn U] g) (hf : HCPolySupport.Book.Ch01.SolenoidalZeroNormalTraceFieldOn U f) : HCPolySupport.Book.Ch01.SolenoidalZeroNormalTraceFieldOn U g

The public zero-normal solenoidal predicate is insensitive to changing the vector field almost everywhere on its domain.