ExitMeanValueIdentificationGreen

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

The Green potential is the zero-trace weak solution of the unshifted Dirichlet problem

The vanishing-shift limit of the Dirichlet resolvents of a bounded measurable datum on an exhaustion cube is here identified analytically: it is the value function of an honest zero-trace Sobolev function on the cube solving -div (a grad w) = f weakly, with zero trace,

and it is the only such value function up to almost-everywhere equality.

The representative is exact: the module produces an H10Function whose value function is the Green potential, not merely a function almost everywhere equal to it. Pointwise arguments downstream read the values of the Green potential, so the exact representative matters.

Two generic transfers

theorem DivergenceFormProcess.Form.exists_h1Function_toFun_eq {d : ℕ} {U : Set (HCPolySupport.Vec d)} (u : HCPolySupport.H1Function U) {g : HCPolySupport.Vec d → ℝ} (hg : HCPolySupport.MemL2On U g) (hgu : g =ᵐ[HCPolySupport.volumeMeasureOn U] u.toFun) : ∃ (w : HCPolySupport.H1Function U), w.toFun = g ∧ w.grad = u.grad

An H¹ function whose value function is replaced by an almost everywhere equal one.

theorem DivergenceFormProcess.Form.IsScalarForcedWeakSolution.congr_datum {d : ℕ} {U : Set (HCPolySupport.Vec d)} {a : HCPolySupport.CoeffField d} {g g' : HCPolySupport.Vec d → ℝ} {u : HCPolySupport.H1Function U} (h : IsScalarForcedWeakSolution a U g u) (hgg : g' =ᵐ[HCPolySupport.volumeMeasureOn U] g) : IsScalarForcedWeakSolution a U g' u

The scalar-forced weak equation only sees the almost-everywhere class of its datum.

theorem DivergenceFormProcess.Form.cubeDatumL2_ae {d : ℕ} (v : ℕ) {f : HCPolySupport.Vec d → ℝ} (hf : Measurable f) {D : ℝ} (hfD : ∀ (x : HCPolySupport.Vec d), |f x| ≤ D) : ↑↑(cubeDatumL2 v hf hfD) =ᵐ[HCPolySupport.volumeMeasureOn (wholeSpaceCube d v)] f

The L² class of the datum agrees almost everywhere on the cube with the datum.