BoundaryClosedCubeRepresentative

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

Gluing the local representatives on the closed cube

Every point of the closed cube carries a ball on which the solution has a continuous representative vanishing on the part of the cube boundary the ball meets. Averaging over shrinking balls glues the interior data into one function on the open cube; extending it by zero produces a single representative continuous on the closed cube and vanishing on its whole boundary, corners included.

theorem Algsuperdiff.StochasticProcess.Common.Regularity.Freezing.exists_closedCube_representative_continuousCoeff {d : ℕ} [NeZero d] (hd : 2 ≤ d) (z : HCPolySupport.Vec d) {L : ℝ} (hL : 0 < L) {nu : ℝ} (hnu : 0 < nu) {a : HCPolySupport.CoeffField d} (hameas : Measurable a) (hsymm : ∀ (y : HCPolySupport.Vec d), HCPolySupport.symmPart (a y) = nu • 1) (hcont : ContinuousOn (fun (y : HCPolySupport.Vec d) => a y - nu • 1) {x : HCPolySupport.Vec d | MemAxisCubeClosure z L x}) {u : HCPolySupport.H10Function (HCPolySupport.axisCube z L)} {g : HCPolySupport.Vec d → ℝ} {M : ℝ} (hM : 0 ≤ M) (hg : Ported.MemScalarLInfOn (HCPolySupport.axisCube z L) g) (hgM : ∀ᵐ (y : HCPolySupport.Vec d) ∂MeasureTheory.volume.restrict (HCPolySupport.axisCube z L), |g y| ≤ M) (hu : Ported.IsMatrixDivFormWeakSolutionZerothOrderOn a (HCPolySupport.axisCube z L) u.toH1Function g 0) : ∃ (V : HCPolySupport.Vec d → ℝ), ContinuousOn V {x : HCPolySupport.Vec d | MemAxisCubeClosure z L x} ∧ V =ᵐ[MeasureTheory.volume.restrict (HCPolySupport.axisCube z L)] u.toFun ∧ ∀ (x : HCPolySupport.Vec d), MemAxisCubeClosure z L x → x ∉ HCPolySupport.axisCube z L → V x = 0

A representative continuous on the closed cube and vanishing on its boundary. The coefficient is continuous on the closed cube with symmetric part nu • 1 and skew part of arbitrary size; there is no contrast hypothesis.