MeasurableRepresentative

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

Measurable representatives of divergence-forced weak solutions

This file packages the measurable-representative bridge needed by pointwise regularity arguments. The representative remains in H¹₀(U) and satisfies the original divergence-forced weak equation with its own weak gradient.

theorem HCPolySupport.IsZeroTraceDirichletRhsWeakSolution.exists_measurableRep {d : ℕ} {U : Set (Vec d)} (hU : IsOpenBoundedConvexDomain U) {a : CoeffField d} {u : H10Function U} {g : Vec d → Vec d} (hsol : IsZeroTraceDirichletRhsWeakSolution a U u g) : ∃ (w : H1Function U), Measurable w.toFun ∧ w.toFun =ᵐ[volumeMeasureOn U] u.toFun ∧ MemH10 U w.toFun ∧ ∀ (φ : H10Function U), ∫ (x : Vec d) in U, vecDot (matVecMul (a x) (w.grad x)) (φ.grad x) = ∫ (x : Vec d) in U, vecDot (g x) (φ.grad x)

A zero-trace divergence-forced weak solution on an open bounded convex domain has a measurable H¹ representative. The representative is almost everywhere equal to the original solution, remains in H¹₀(U), and satisfies the same weak equation with its own weak gradient.

theorem HCPolySupport.IsZeroTraceDirichletRhsWeakSolution.exists_measurableH10Rep {d : ℕ} {U : Set (Vec d)} (hU : IsOpenBoundedConvexDomain U) {a : CoeffField d} {u : H10Function U} {g : Vec d → Vec d} (hsol : IsZeroTraceDirichletRhsWeakSolution a U u g) : ∃ (v : H10Function U), Measurable v.toFun ∧ v.toFun =ᵐ[volumeMeasureOn U] u.toFun ∧ IsZeroTraceDirichletRhsWeakSolution a U v g

A zero-trace divergence-forced weak solution has a measurable H10Function representative which is almost everywhere equal to the original solution and satisfies the same zero-trace weak-solution predicate.