ScalarWeakSolution

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

Pointwise scalar-forced divergence-form weak solutions

This file exposes the variational equation needed by scalar De Giorgi arguments. Our sign convention is

-div (a grad u) = g,

so testing against v gives integral (a grad u) dot grad v = integral g * v. The forcing is an honest pointwise scalar field with an explicit local L^2 witness.

def DivergenceFormProcess.Form.IsScalarForcedWeakSolution {d : ℕ} (a : HCPolySupport.CoeffField d) (U : Set (HCPolySupport.Vec d)) (g : HCPolySupport.Vec d → ℝ) (u : HCPolySupport.H1Function U) : Prop

The pointwise weak equation -div (a grad u) = g on U.

The test space is the existing H10Function U carrier. The first conjunct keeps the pointwise forcing available to subsequent truncation and level-set estimates.

Equations

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

theorem DivergenceFormProcess.Form.IsScalarForcedWeakSolution.const_smul_coefficient {d : ℕ} {W : Set (HCPolySupport.Vec d)} {c : ℝ} {a : HCPolySupport.CoeffField d} {u : HCPolySupport.H1Function W} {g : HCPolySupport.Vec d → ℝ} (hu : IsScalarForcedWeakSolution a W g u) : IsScalarForcedWeakSolution (fun (x : HCPolySupport.Vec d) => c • a x) W (fun (x : HCPolySupport.Vec d) => c * g x) u

Scaling the coefficient and scalar forcing by the same real constant preserves the equation.

theorem DivergenceFormProcess.Form.isScalarForcedWeakSolution_sub_alpha_mul_of_isAlphaShiftedWeakSolution {d : ℕ} {U : Set (HCPolySupport.Vec d)} {a : HCPolySupport.CoeffField d} {alpha : ℝ} {f : ↥(HCPolySupport.ScalarL2 U)} (u : HCPolySupport.H10Function U) (hweak : IsAlphaShiftedWeakSolution a U alpha f (ZeroTraceSobolev.ofH10Function u)) : IsScalarForcedWeakSolution a U (fun (x : HCPolySupport.Vec d) => ↑↑f x - alpha * u.toFun x) u.toH1Function

The alpha-shifted graph-carrier equation gives the pointwise equation -div (a grad u) = f - alpha * u for every honest H10Function representative.