ZerothOrderSchauderBall

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

Interior Schauder estimate on an arbitrary Euclidean ball

The small-contrast chain proves its interior Hölder estimate on the fixed unit ball smallContrastUnitBall d = euclideanBall 0 1, concluding on the concentric ball of radius 1/2. Every consumer works instead on a ball euclideanBall x₀ r sitting inside a given open set, so the estimate has to be transported along the affine chart

ballChart x₀ r : x ↦ r • x + x₀,

which carries euclideanBall 0 s onto euclideanBall x₀ (r * s) and pushes Lebesgue measure to r ^ d times Lebesgue measure. The normalization used for the transported solution is v x = r⁻¹ * u (r • x + x₀), so that ∇v x = ∇u (r • x + x₀).

The three scalings that produce the explicit radius powers of the conclusion are isolated as named theorems:

• vectorLpSizeOn_two_ballTransfer_grad — the gradient L² size scales by r ^ (-(d : ℝ)/2);
• scalarLInfSizeOn_ballScalarSource — the transported scalar source has L^∞ size r times the original;
• holderBound_of_ballTransfer — the Hölder pull-back |u x - u y| = r * |v (r⁻¹ • (x - x₀)) - v (r⁻¹ • (y - x₀))|.

The vector source of the transported equation is 0, so the factor (1 - alpha)⁻¹ carried by smallContrastDataSize multiplies 0 and does not appear in the constant of the conclusion.

The affine chart

def Algsuperdiff.StochasticProcess.Common.Regularity.Ported.ballChart {d : ℕ} (x₀ : HCPolySupport.Vec d) (r : ℝ) : HCPolySupport.Vec d → HCPolySupport.Vec d

The affine chart carrying the unit ball onto euclideanBall x₀ r.

Equations

• Algsuperdiff.StochasticProcess.Common.Regularity.Ported.ballChart x₀ r x = r • x + x₀

noncomputable def Algsuperdiff.StochasticProcess.Common.Regularity.Ported.ballChartInv {d : ℕ} (x₀ : HCPolySupport.Vec d) (r : ℝ) : HCPolySupport.Vec d → HCPolySupport.Vec d

The inverse of ballChart x₀ r.

Equations

• Algsuperdiff.StochasticProcess.Common.Regularity.Ported.ballChartInv x₀ r y = r⁻¹ • (y - x₀)

@[simp]

theorem Algsuperdiff.StochasticProcess.Common.Regularity.Ported.ballChart_apply {d : ℕ} (x₀ : HCPolySupport.Vec d) (r : ℝ) (x : HCPolySupport.Vec d) : ballChart x₀ r x = r • x + x₀

@[simp]

theorem Algsuperdiff.StochasticProcess.Common.Regularity.Ported.ballChartInv_apply {d : ℕ} (x₀ : HCPolySupport.Vec d) (r : ℝ) (y : HCPolySupport.Vec d) : ballChartInv x₀ r y = r⁻¹ • (y - x₀)

theorem Algsuperdiff.StochasticProcess.Common.Regularity.Ported.ballChart_ballChartInv {d : ℕ} (x₀ : HCPolySupport.Vec d) {r : ℝ} (hr : 0 < r) (y : HCPolySupport.Vec d) : ballChart x₀ r (ballChartInv x₀ r y) = y

theorem Algsuperdiff.StochasticProcess.Common.Regularity.Ported.ballChart_mem_euclideanBall_iff {d : ℕ} (x₀ : HCPolySupport.Vec d) {r s : ℝ} (hr : 0 < r) (x : HCPolySupport.Vec d) : ballChart x₀ r x ∈ HCPolySupport.euclideanBall x₀ (r * s) ↔ x ∈ HCPolySupport.euclideanBall 0 s

Membership in a concentric ball is invariant under the chart, with radii scaled by r.

theorem Algsuperdiff.StochasticProcess.Common.Regularity.Ported.measurableEmbedding_ballChart {d : ℕ} (x₀ : HCPolySupport.Vec d) {r : ℝ} (hr : 0 < r) : MeasurableEmbedding (ballChart x₀ r)

theorem Algsuperdiff.StochasticProcess.Common.Regularity.Ported.continuous_ballChartInv {d : ℕ} (x₀ : HCPolySupport.Vec d) (r : ℝ) : Continuous (ballChartInv x₀ r)

Measure transport along the chart

theorem Algsuperdiff.StochasticProcess.Common.Regularity.Ported.map_ballChart_volume_restrict {d : ℕ} (x₀ : HCPolySupport.Vec d) {r : ℝ} (hr : 0 < r) : MeasureTheory.Measure.map (ballChart x₀ r) (MeasureTheory.volume.restrict (smallContrastUnitBall d)) = ENNReal.ofReal (r ^ d)⁻¹ • MeasureTheory.volume.restrict (HCPolySupport.euclideanBall x₀ r)

The chart pushes Lebesgue measure restricted to the unit ball forward to (r ^ d)⁻¹ times Lebesgue measure restricted to euclideanBall x₀ r.

theorem Algsuperdiff.StochasticProcess.Common.Regularity.Ported.setIntegral_comp_ballChart {d : ℕ} (x₀ : HCPolySupport.Vec d) {r : ℝ} (hr : 0 < r) (F : HCPolySupport.Vec d → ℝ) : ∫ (x : HCPolySupport.Vec d) in smallContrastUnitBall d, F (r • x + x₀) = (r ^ d)⁻¹ * ∫ (y : HCPolySupport.Vec d) in HCPolySupport.euclideanBall x₀ r, F y

Change of variables for a set integral over the chart.

theorem Algsuperdiff.StochasticProcess.Common.Regularity.Ported.map_ballChartInv_volume_restrict {d : ℕ} (x₀ : HCPolySupport.Vec d) {r : ℝ} (hr : 0 < r) : MeasureTheory.Measure.map (ballChartInv x₀ r) (MeasureTheory.volume.restrict (HCPolySupport.euclideanBall x₀ r)) = ENNReal.ofReal (r ^ d) • MeasureTheory.volume.restrict (smallContrastUnitBall d)

The inverse chart pushes Lebesgue measure restricted to euclideanBall x₀ r forward to r ^ d times Lebesgue measure restricted to the unit ball.

theorem Algsuperdiff.StochasticProcess.Common.Regularity.Ported.quasiMeasurePreserving_ballChart {d : ℕ} (x₀ : HCPolySupport.Vec d) {r : ℝ} (hr : 0 < r) : MeasureTheory.QuasiMeasurePreserving (ballChart x₀ r) (MeasureTheory.volume.restrict (smallContrastUnitBall d)) (MeasureTheory.volume.restrict (HCPolySupport.euclideanBall x₀ r))

The chart is quasi measure preserving, so a.e. statements on euclideanBall x₀ r pull back to the unit ball.

theorem Algsuperdiff.StochasticProcess.Common.Regularity.Ported.quasiMeasurePreserving_ballChartInv {d : ℕ} (x₀ : HCPolySupport.Vec d) {r : ℝ} (hr : 0 < r) : MeasureTheory.QuasiMeasurePreserving (ballChartInv x₀ r) (MeasureTheory.volume.restrict (HCPolySupport.euclideanBall x₀ r)) (MeasureTheory.volume.restrict (smallContrastUnitBall d))

The inverse chart is quasi measure preserving, so a.e. statements on the unit ball push forward to euclideanBall x₀ r.

Transport of Sobolev witnesses

def Algsuperdiff.StochasticProcess.Common.Regularity.Ported.h1OfSetEq {d : ℕ} {U W : Set (HCPolySupport.Vec d)} (h : U = W) (u : HCPolySupport.H1Function U) : HCPolySupport.H1Function W

Transport an H¹ witness along an equality of domains.

Equations

• Algsuperdiff.StochasticProcess.Common.Regularity.Ported.h1OfSetEq h u = h ▸ u

@[simp]

theorem Algsuperdiff.StochasticProcess.Common.Regularity.Ported.h1OfSetEq_toFun {d : ℕ} {U W : Set (HCPolySupport.Vec d)} (h : U = W) (u : HCPolySupport.H1Function U) : (h1OfSetEq h u).toFun = u.toFun

@[simp]

theorem Algsuperdiff.StochasticProcess.Common.Regularity.Ported.h1OfSetEq_grad {d : ℕ} {U W : Set (HCPolySupport.Vec d)} (h : U = W) (u : HCPolySupport.H1Function U) : (h1OfSetEq h u).grad = u.grad

def Algsuperdiff.StochasticProcess.Common.Regularity.Ported.h10OfSetEq {d : ℕ} {U W : Set (HCPolySupport.Vec d)} (h : U = W) (u : HCPolySupport.H10Function U) : HCPolySupport.H10Function W

Transport an H¹₀ witness along an equality of domains.

Equations

• Algsuperdiff.StochasticProcess.Common.Regularity.Ported.h10OfSetEq h u = h ▸ u

@[simp]

theorem Algsuperdiff.StochasticProcess.Common.Regularity.Ported.h10OfSetEq_toH1Function {d : ℕ} {U W : Set (HCPolySupport.Vec d)} (h : U = W) (u : HCPolySupport.H10Function U) : (h10OfSetEq h u).toH1Function = h1OfSetEq h u.toH1Function

noncomputable def Algsuperdiff.StochasticProcess.Common.Regularity.Ported.ballTransfer {d : ℕ} (x₀ : HCPolySupport.Vec d) {r : ℝ} (hr : 0 < r) (u : HCPolySupport.H1Function (HCPolySupport.euclideanBall x₀ r)) : HCPolySupport.H1Function (smallContrastUnitBall d)

The unit-ball normalization v x = r⁻¹ * u (r • x + x₀) of an H¹ function on euclideanBall x₀ r. With this normalization the gradient is the plain pull-back of the gradient of u.

Equations

• One or more equations did not get rendered due to their size.

@[simp]

theorem Algsuperdiff.StochasticProcess.Common.Regularity.Ported.ballTransfer_toFun {d : ℕ} (x₀ : HCPolySupport.Vec d) {r : ℝ} (hr : 0 < r) (u : HCPolySupport.H1Function (HCPolySupport.euclideanBall x₀ r)) (x : HCPolySupport.Vec d) : (ballTransfer x₀ hr u).toFun x = r⁻¹ * u.toFun (r • x + x₀)

@[simp]

theorem Algsuperdiff.StochasticProcess.Common.Regularity.Ported.ballTransfer_grad {d : ℕ} (x₀ : HCPolySupport.Vec d) {r : ℝ} (hr : 0 < r) (u : HCPolySupport.H1Function (HCPolySupport.euclideanBall x₀ r)) (x : HCPolySupport.Vec d) : (ballTransfer x₀ hr u).grad x = u.grad (r • x + x₀)

noncomputable def Algsuperdiff.StochasticProcess.Common.Regularity.Ported.ballTestTransfer {d : ℕ} (x₀ : HCPolySupport.Vec d) {r : ℝ} (hr : 0 < r) (psi : HCPolySupport.H10Function (smallContrastUnitBall d)) : HCPolySupport.H10Function (HCPolySupport.euclideanBall x₀ r)

The test-function direction of the chart: an H¹₀ witness on the unit ball becomes an H¹₀ witness on euclideanBall x₀ r.

Equations

• One or more equations did not get rendered due to their size.

@[simp]

theorem Algsuperdiff.StochasticProcess.Common.Regularity.Ported.ballTestTransfer_toFun {d : ℕ} (x₀ : HCPolySupport.Vec d) {r : ℝ} (hr : 0 < r) (psi : HCPolySupport.H10Function (smallContrastUnitBall d)) (y : HCPolySupport.Vec d) : (ballTestTransfer x₀ hr psi).toFun y = psi.toFun (r⁻¹ • (y - x₀))

@[simp]

theorem Algsuperdiff.StochasticProcess.Common.Regularity.Ported.ballTestTransfer_grad {d : ℕ} (x₀ : HCPolySupport.Vec d) {r : ℝ} (hr : 0 < r) (psi : HCPolySupport.H10Function (smallContrastUnitBall d)) (y : HCPolySupport.Vec d) : (ballTestTransfer x₀ hr psi).grad y = r⁻¹ • psi.grad (r⁻¹ • (y - x₀))

The transported data and its scalings

def Algsuperdiff.StochasticProcess.Common.Regularity.Ported.ballCoeff {d : ℕ} (a : HCPolySupport.CoeffField d) (x₀ : HCPolySupport.Vec d) (r : ℝ) : HCPolySupport.CoeffField d

The coefficient field read in the chart.

Equations

• Algsuperdiff.StochasticProcess.Common.Regularity.Ported.ballCoeff a x₀ r x = a (Algsuperdiff.StochasticProcess.Common.Regularity.Ported.ballChart x₀ r x)

def Algsuperdiff.StochasticProcess.Common.Regularity.Ported.ballScalarSource {d : ℕ} (g : HCPolySupport.Vec d → ℝ) (x₀ : HCPolySupport.Vec d) (r : ℝ) : HCPolySupport.Vec d → ℝ

The scalar source of the transported equation.

Equations

• Algsuperdiff.StochasticProcess.Common.Regularity.Ported.ballScalarSource g x₀ r x = r * g (Algsuperdiff.StochasticProcess.Common.Regularity.Ported.ballChart x₀ r x)

theorem Algsuperdiff.StochasticProcess.Common.Regularity.Ported.measurable_ballCoeff {d : ℕ} {a : HCPolySupport.CoeffField d} (ha : Measurable a) (x₀ : HCPolySupport.Vec d) {r : ℝ} (hr : 0 < r) : Measurable (ballCoeff a x₀ r)

theorem Algsuperdiff.StochasticProcess.Common.Regularity.Ported.coefficientIdentityDistanceLE_ballCoeff {d : ℕ} {a : HCPolySupport.CoeffField d} (x₀ : HCPolySupport.Vec d) {r delta : ℝ} (hr : 0 < r) (ha : CoefficientIdentityDistanceLE (HCPolySupport.euclideanBall x₀ r) a delta) : CoefficientIdentityDistanceLE (smallContrastUnitBall d) (ballCoeff a x₀ r) delta

The identity distance of the coefficient transfers to the unit ball, because the chart pushes Lebesgue measure to a positive multiple of Lebesgue measure.

theorem Algsuperdiff.StochasticProcess.Common.Regularity.Ported.eLpNorm_comp_ballChart {d : ℕ} (x₀ : HCPolySupport.Vec d) {r : ℝ} (hr : 0 < r) (F : HCPolySupport.Vec d → ℝ) (p : ENNReal) : MeasureTheory.eLpNorm (fun (x : HCPolySupport.Vec d) => F (ballChart x₀ r x)) p (MeasureTheory.volume.restrict (smallContrastUnitBall d)) = ENNReal.ofReal (r ^ d)⁻¹ ^ (1 / p).toReal * MeasureTheory.eLpNorm F p (MeasureTheory.volume.restrict (HCPolySupport.euclideanBall x₀ r))

The L^p seminorm read in the chart.

theorem Algsuperdiff.StochasticProcess.Common.Regularity.Ported.memLp_comp_ballChart {d : ℕ} (x₀ : HCPolySupport.Vec d) {r : ℝ} (hr : 0 < r) {F : HCPolySupport.Vec d → ℝ} {p : ENNReal} (hF : MeasureTheory.MemLp F p (MeasureTheory.volume.restrict (HCPolySupport.euclideanBall x₀ r))) : MeasureTheory.MemLp (fun (x : HCPolySupport.Vec d) => F (ballChart x₀ r x)) p (MeasureTheory.volume.restrict (smallContrastUnitBall d))

Membership in L^p read in the chart.

theorem Algsuperdiff.StochasticProcess.Common.Regularity.Ported.vectorLpSizeOn_two_ballTransfer_grad {d : ℕ} (x₀ : HCPolySupport.Vec d) {r : ℝ} (hr : 0 < r) (u : HCPolySupport.H1Function (HCPolySupport.euclideanBall x₀ r)) : vectorLpSizeOn (smallContrastUnitBall d) 2 (ballTransfer x₀ hr u).grad = r ^ (-↑d / 2) * vectorLpSizeOn (HCPolySupport.euclideanBall x₀ r) 2 u.grad

First scaling. The gradient L² size of the transported solution.

theorem Algsuperdiff.StochasticProcess.Common.Regularity.Ported.scalarLInfSizeOn_ballScalarSource {d : ℕ} (x₀ : HCPolySupport.Vec d) {r : ℝ} (hr : 0 < r) (g : HCPolySupport.Vec d → ℝ) : scalarLInfSizeOn (smallContrastUnitBall d) (ballScalarSource g x₀ r) = r * scalarLInfSizeOn (HCPolySupport.euclideanBall x₀ r) g

Second scaling. The L^∞ size of the transported scalar source.

theorem Algsuperdiff.StochasticProcess.Common.Regularity.Ported.memScalarLInfOn_ballScalarSource {d : ℕ} (x₀ : HCPolySupport.Vec d) {r : ℝ} (hr : 0 < r) {g : HCPolySupport.Vec d → ℝ} (hg : MemScalarLInfOn (HCPolySupport.euclideanBall x₀ r) g) : MemScalarLInfOn (smallContrastUnitBall d) (ballScalarSource g x₀ r)

The transported scalar source is bounded when the original one is.

The transported equation

theorem Algsuperdiff.StochasticProcess.Common.Regularity.Ported.isMatrixDivFormWeakSolutionZerothOrderOn_ballTransfer {d : ℕ} {a : HCPolySupport.CoeffField d} (x₀ : HCPolySupport.Vec d) {r : ℝ} (hr : 0 < r) {u : HCPolySupport.H1Function (HCPolySupport.euclideanBall x₀ r)} {g : HCPolySupport.Vec d → ℝ} (hu : IsMatrixDivFormWeakSolutionZerothOrderOn a (HCPolySupport.euclideanBall x₀ r) u g 0) : IsMatrixDivFormWeakSolutionZerothOrderOn (ballCoeff a x₀ r) (smallContrastUnitBall d) (ballTransfer x₀ hr u) (ballScalarSource g x₀ r) 0

The zeroth-order weak equation with a vanishing vector source transfers to the unit ball, with coefficient ballCoeff and scalar source ballScalarSource.

The interior estimate on euclideanBall x₀ r

theorem Algsuperdiff.StochasticProcess.Common.Regularity.Ported.holderBound_of_ballTransfer {d : ℕ} (x₀ : HCPolySupport.Vec d) {r : ℝ} (hr : 0 < r) {alpha K : ℝ} {v : HCPolySupport.Vec d → ℝ} (hv : EuclideanHolderBoundOn (smallContrastBall d (1 / 2)) alpha K v) : EuclideanHolderBoundOn (HCPolySupport.euclideanBall x₀ (r / 2)) alpha (r ^ (1 - alpha) * K) fun (y : HCPolySupport.Vec d) => r * v (ballChartInv x₀ r y)

Third scaling. A Hölder bound on the concentric half unit ball becomes, after the pull-back u x = r * v (r⁻¹ • (x - x₀)), a Hölder bound on euclideanBall x₀ (r/2) with the constant multiplied by r ^ (1 - alpha).

theorem Algsuperdiff.StochasticProcess.Common.Regularity.Ported.schauder_holder_euclideanBall_zerothOrder {d : ℕ} [NeZero d] {a : HCPolySupport.CoeffField d} (x₀ : HCPolySupport.Vec d) {r : ℝ} (hr : 0 < r) {u : HCPolySupport.H1Function (HCPolySupport.euclideanBall x₀ r)} {g : HCPolySupport.Vec d → ℝ} {delta alpha : ℝ} (hd : 2 ≤ d) (halpha : alpha ∈ Set.Ico (1 / 2) 1) (hdelta0 : 0 ≤ delta) (hdelta : delta ≤ smallContrastThreshold d alpha) (hameas : Measurable a) (ha : CoefficientIdentityDistanceLE (HCPolySupport.euclideanBall x₀ r) a delta) (hu : IsMatrixDivFormWeakSolutionZerothOrderOn a (HCPolySupport.euclideanBall x₀ r) u g 0) (hg : MemScalarLInfOn (HCPolySupport.euclideanBall x₀ r) g) : ∃ (v : HCPolySupport.Vec d → ℝ), ContinuousOn v (HCPolySupport.euclideanBall x₀ (r / 2)) ∧ v =ᵐ[MeasureTheory.volume.restrict (HCPolySupport.euclideanBall x₀ r)] u.toFun ∧ EuclideanHolderBoundOn (HCPolySupport.euclideanBall x₀ (r / 2)) alpha (smallContrastZerothSchauderConstant d * (r ^ (1 - alpha - ↑d / 2) * vectorLpSizeOn (HCPolySupport.euclideanBall x₀ r) 2 u.grad + r ^ (2 - alpha) * scalarLInfSizeOn (HCPolySupport.euclideanBall x₀ r) g)) v

Interior Hölder estimate on an arbitrary Euclidean ball, with a bounded scalar source and no vector source. The constant is the explicit dimensional coefficient of the unit-ball estimate times the two scaled data terms; because the vector source vanishes, the factor (1 - alpha)⁻¹ of the general estimate is absent.