ResolventH10Representative

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

Honest Sobolev representatives of the domain resolvent

This file exposes the strongest representative statement currently supplied by the divergence-form foundation. On an open bounded convex domain, the L² resolvent has an honest zero-trace H¹ representative. The theorem also identifies that representative with the canonical graph-carrier weak solution.

No continuity is asserted. Obtaining a continuous, or boundary-vanishing continuous, representative requires a local-to-pointwise and boundary regularity bridge which is not currently available in the declared dependencies. That bridge may be supplied by a model-specific consequence of Theorem C or by classical local regularity.

theorem DivergenceFormProcess.Form.exists_h10Function_alphaShiftedResolvent {d : ℕ} {U : Set (HCPolySupport.Vec d)} (hU : HCPolySupport.IsOpenBoundedConvexDomain U) (a : HCPolySupport.CoeffField d) {alpha lam Lam : ℝ} (hAlpha : 0 < alpha) (hLam : 0 < lam) (hEll : HCPolySupport.IsEllipticFieldOn lam Lam U a) (f : ↥(HCPolySupport.ScalarL2 U)) : ∃ (u : HCPolySupport.H10Function U), ZeroTraceSobolev.ofH10Function u = (alphaShiftedSolution a hAlpha hLam hEll) f ∧ IsAlphaShiftedWeakSolution a U alpha f (ZeroTraceSobolev.ofH10Function u) ∧ u.toScalarL2 = (alphaShiftedResolvent a hAlpha hLam hEll) f

The shifted resolvent has an honest zero-trace Sobolev representative. Both its L² value and its gradient are the components of the canonical graph-carrier solution.