InteriorHolderConstant

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

The interior Hölder constant after freezing

InteriorContinuity.lean proves that a bounded solution with a continuous skew part has a locally C^{0,1/2} representative, but its statements quantify the Hölder constant existentially. Several consumers need the constant itself: one radius and one constant serving a whole family of data is what turns an almost-everywhere statement into a pointwise one.

This file keeps the constant. At an interior point the freezing radius comes from the local contrast radius of LocalContrast.lean, which depends on the coefficient, the point and the fixed Schauder threshold only, never on the solution. On the concentric half ball the constant returned by schauder_holder_euclideanBall_zerothOrder is exactly penalizationInteriorHolderConstant d (1/2) (s/2) G (nu⁻¹ * M), where G is any bound for the gradient size of the solution on the ball of radius s and 2 * M any bound for the essential size of the zeroth-order datum there. The constant therefore depends on the datum only through those two numbers, so it is the same for every family of data with a common bound.

A compact subset of the domain admits one radius serving all of its points.

theorem Algsuperdiff.StochasticProcess.Common.Regularity.Freezing.exists_frozenRadius_holder_of_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) {z : HCPolySupport.Vec d} (hz : z ∈ U) : ∃ s > 0, HCPolySupport.euclideanBall z s ⊆ U ∧ ∀ (G M : ℝ) (u : HCPolySupport.H1Function (HCPolySupport.euclideanBall z s)) (g : HCPolySupport.Vec d → ℝ), Ported.MemScalarLInfOn (HCPolySupport.euclideanBall z s) g → Ported.scalarLInfSizeOn (HCPolySupport.euclideanBall z s) g ≤ 2 * M → Ported.vectorLpSizeOn (HCPolySupport.euclideanBall z s) 2 u.grad ≤ G → Ported.IsMatrixDivFormWeakSolutionZerothOrderOn a (HCPolySupport.euclideanBall z s) u g 0 → ∃ (v : HCPolySupport.Vec d → ℝ), ContinuousOn v (HCPolySupport.euclideanBall z (s / 2)) ∧ v =ᵐ[MeasureTheory.volume.restrict (HCPolySupport.euclideanBall z s)] u.toFun ∧ Ported.EuclideanHolderBoundOn (HCPolySupport.euclideanBall z (s / 2)) (1 / 2) (DivergenceFormProcess.Form.penalizationInteriorHolderConstant d (1 / 2) (s / 2) G (nu⁻¹ * M)) v

Quantitative interior estimate at an interior point. At every point of an open set carrying a coefficient with symmetric part nu • 1 and continuous skew part, one radius — the local contrast radius at that point — serves every bounded zeroth-order weak solution on the ball of that radius: the Hölder constant on the concentric half ball is the Schauder constant of the frozen small-contrast estimate, and it depends on the solution and its datum only through the gradient budget G and the essential budget 2 * M.