BoundaryLocalRepresentative

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

A continuous representative near a point of the closed cube

Freezing the skew part at a point of the closed cube and normalizing by the scalar symmetric part makes the coefficient uniformly close to the identity on a small ball. On that scale the ball meets only the faces through the centre, so the solution unfolds oddly into a small-contrast solution on the whole ball. The scale-free interior estimate then produces a representative continuous on the half ball, odd under every unfolded reflection, hence vanishing on the part of the cube boundary that the ball meets.

theorem Algsuperdiff.StochasticProcess.Common.Regularity.Freezing.isMatrixDivFormWeakSolutionZerothOrderOn_smul_coeff {d : ℕ} {W : Set (HCPolySupport.Vec d)} {c : ℝ} {a : HCPolySupport.CoeffField d} {u : HCPolySupport.H1Function W} {g : HCPolySupport.Vec d → ℝ} (hu : Ported.IsMatrixDivFormWeakSolutionZerothOrderOn a W u g 0) : Ported.IsMatrixDivFormWeakSolutionZerothOrderOn (fun (x : HCPolySupport.Vec d) => c • a x) W u (fun (x : HCPolySupport.Vec d) => c * g x) 0

Scaling the coefficient scales the scalar source.

theorem Algsuperdiff.StochasticProcess.Common.Regularity.Freezing.exists_boundary_local_representative {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) {x₀ : HCPolySupport.Vec d} (hx₀ : MemAxisCubeClosure z L x₀) : ∃ rho > 0, ∃ (V : HCPolySupport.Vec d → ℝ), ContinuousOn V (HCPolySupport.euclideanBall x₀ rho) ∧ V =ᵐ[MeasureTheory.volume.restrict (HCPolySupport.euclideanBall x₀ rho ∩ HCPolySupport.axisCube z L)] u.toFun ∧ ∀ y ∈ HCPolySupport.euclideanBall x₀ rho, MemAxisCubeClosure z L y → y ∉ HCPolySupport.axisCube z L → V y = 0

A continuous representative on a ball about a point of the closed cube. The coefficient is continuous with symmetric part nu • 1 and skew part of arbitrary size; no contrast hypothesis appears.