SkewConst #
Ported from scottnarmstrong/Superdiffusion at 7f20476385d4af418f110303085ad0740c9eba46. Module imports, support namespace and local option directives adapted for Lean Pool.
Freezing a constant skew part #
A constant skew matrix has zero weak pairing against an H¹ gradient and an
H¹₀ test gradient. Consequently it may be subtracted from each weak
coefficient carrier used by the interior regularity argument.
theorem
Algsuperdiff.StochasticProcess.Common.Regularity.Freezing.isMatrixDivFormWeakSolutionZerothOrderOn_sub_skew_const_iff
{d : ℕ}
{U : Set (HCPolySupport.Vec d)}
{a : HCPolySupport.CoeffField d}
{k₀ : HCPolySupport.Mat d}
(hk₀ : HCPolySupport.matTranspose k₀ = -k₀)
{u : HCPolySupport.H1Function U}
{g : HCPolySupport.Vec d → ℝ}
{f : HCPolySupport.Vec d → HCPolySupport.Vec d}
:
Ported.IsMatrixDivFormWeakSolutionZerothOrderOn (fun (x : HCPolySupport.Vec d) => a x - k₀) U u g f ↔ Ported.IsMatrixDivFormWeakSolutionZerothOrderOn a U u g f
Subtracting a constant skew matrix preserves the scalar-plus-divergence matrix weak equation.
theorem
Algsuperdiff.StochasticProcess.Common.Regularity.Freezing.isScalarForcedWeakSolution_sub_skew_const
{d : ℕ}
{U : Set (HCPolySupport.Vec d)}
{a : HCPolySupport.CoeffField d}
{k₀ : HCPolySupport.Mat d}
(hk₀ : HCPolySupport.matTranspose k₀ = -k₀)
{g : HCPolySupport.Vec d → ℝ}
{u : HCPolySupport.H1Function U}
:
DivergenceFormProcess.Form.IsScalarForcedWeakSolution (fun (x : HCPolySupport.Vec d) => a x - k₀) U g u ↔ DivergenceFormProcess.Form.IsScalarForcedWeakSolution a U g u
A scalar-forced weak solution for a is equivalently one for a - k₀
when k₀ is constant and skew.