InteriorContinuity

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

Interior continuity by freezing continuous skew coefficients

At each interior point we subtract the constant skew part at that point, normalize by the positive scalar symmetric part, and apply the scale-free small-contrast Schauder estimate on a sufficiently small Euclidean ball. The resulting local representatives are glued by shrinking-ball averages.

theorem Algsuperdiff.StochasticProcess.Common.Regularity.Freezing.isMatrixDivFormWeakSolutionZerothOrderOn_const_smul_zero {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 a zeroth-order weak equation by a constant scales its datum.

theorem Algsuperdiff.StochasticProcess.Common.Regularity.Freezing.memScalarLInfOn_const_mul {d : ℕ} {W : Set (HCPolySupport.Vec d)} {c : ℝ} {g : HCPolySupport.Vec d → ℝ} (hg : Ported.MemScalarLInfOn W g) : Ported.MemScalarLInfOn W fun (x : HCPolySupport.Vec d) => c * g x

A constant multiple of an essentially bounded datum is essentially bounded.

theorem Algsuperdiff.StochasticProcess.Common.Regularity.Freezing.exists_local_holder_representative_of_weakSolution_continuousCoeff {d : ℕ} [NeZero d] (hd : 2 ≤ d) {U : Set (HCPolySupport.Vec d)} (hU : IsOpen U) {nu : ℝ} (hnu : 0 < nu) {a : HCPolySupport.CoeffField d} (hsymm : ∀ (y : HCPolySupport.Vec d), HCPolySupport.symmPart (a y) = nu • 1) (hcont : ContinuousOn (fun (y : HCPolySupport.Vec d) => a y - nu • 1) U) {g : HCPolySupport.Vec d → ℝ} (hg : Ported.MemScalarLInfOn U g) {u : HCPolySupport.H1Function U} (hu : DivergenceFormProcess.Form.IsScalarForcedWeakSolution a U g u) (z : HCPolySupport.Vec d) : z ∈ U → ∃ r > 0, HCPolySupport.euclideanBall z r ⊆ U ∧ ∃ (v : HCPolySupport.Vec d → ℝ), ContinuousOn v (HCPolySupport.euclideanBall z r) ∧ v =ᵐ[MeasureTheory.volume.restrict (HCPolySupport.euclideanBall z r)] u.toFun ∧ ∃ (C : ℝ), Ported.EuclideanHolderBoundOn (HCPolySupport.euclideanBall z r) (1 / 2) C v

A scalar-forced weak solution with bounded forcing has a C^{0,1/2} representative on a ball about each interior point. The coefficient may have continuous skew part of arbitrary size.

theorem Algsuperdiff.StochasticProcess.Common.Regularity.Freezing.continuousOn_of_weakSolution_continuousCoeff {d : ℕ} [NeZero d] (hd : 2 ≤ d) {U : Set (HCPolySupport.Vec d)} (hU : IsOpen U) {nu : ℝ} (hnu : 0 < nu) {a : HCPolySupport.CoeffField d} (hsymm : ∀ (y : HCPolySupport.Vec d), HCPolySupport.symmPart (a y) = nu • 1) (hcont : ContinuousOn (fun (y : HCPolySupport.Vec d) => a y - nu • 1) U) {g : HCPolySupport.Vec d → ℝ} (hg : Ported.MemScalarLInfOn U g) {u : HCPolySupport.H1Function U} (hu : DivergenceFormProcess.Form.IsScalarForcedWeakSolution a U g u) : ∃ (v : HCPolySupport.Vec d → ℝ), ContinuousOn v U ∧ v =ᵐ[MeasureTheory.volume.restrict U] u.toFun ∧ ∀ z ∈ U, ∃ r > 0, HCPolySupport.euclideanBall z r ⊆ U ∧ ∃ (C : ℝ), Ported.EuclideanHolderBoundOn (HCPolySupport.euclideanBall z r) (1 / 2) C v

Interior continuity and local C^{0,1/2} regularity for scalar-forced weak solutions with bounded forcing and continuous coefficients of arbitrary skew size.

theorem Algsuperdiff.StochasticProcess.Common.Regularity.Freezing.continuousOn_alphaShiftedResolvent_continuousCoeff {d : ℕ} [NeZero d] (hd : 2 ≤ d) {U : Set (HCPolySupport.Vec d)} (hU : HCPolySupport.IsOpenBoundedConvexDomain U) (a : HCPolySupport.CoeffField d) {nu : ℝ} (hnu : 0 < nu) (hsymm : ∀ (y : HCPolySupport.Vec d), HCPolySupport.symmPart (a y) = nu • 1) (hcont : ContinuousOn (fun (y : HCPolySupport.Vec d) => a y - nu • 1) U) {mu lam Lam M : ℝ} (hmu : 0 < mu) (hlam : 0 < lam) (hEll : HCPolySupport.IsEllipticFieldOn lam Lam U a) (f : ↥(HCPolySupport.ScalarL2 U)) (hM : 0 ≤ M) (hfM : ∀ᵐ (x : HCPolySupport.Vec d) ∂HCPolySupport.volumeMeasureOn U, |↑↑f x| ≤ M) : ∃ (v : HCPolySupport.Vec d → ℝ), ContinuousOn v U ∧ v =ᵐ[HCPolySupport.volumeMeasureOn U] ↑↑((DivergenceFormProcess.Form.alphaShiftedResolvent a hmu hlam hEll) f) ∧ ∀ z ∈ U, ∃ r > 0, HCPolySupport.euclideanBall z r ⊆ U ∧ ∃ (C : ℝ), Ported.EuclideanHolderBoundOn (HCPolySupport.euclideanBall z r) (1 / 2) C v

A bounded shifted resolvent for the same continuous coefficient has a continuous, locally C^{0,1/2} representative. The bounded residual f - mu*u supplies the zeroth-order datum.