Pointwise

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

Pointwise interior bound from a local L² bound

The interior Hölder estimate for small contrast turns the local L² size of a solution into a pointwise bound at the centre of a ball: the value at the centre is bounded by the L² average on any concentric sub-ball plus the Hölder modulus at that radius. Shrinking the sub-ball trades the two terms against each other.

The small-contrast hypothesis is the price of using the interior Schauder chain of the regularity layer. A general elliptic field would need a De Giorgi--Nash--Moser local boundedness estimate, which the layer does not carry.

Main results

• DivergenceFormProcess.Decay.zerothOrderOn_restrict_of_isScalarForcedWeakSolution
• DivergenceFormProcess.Decay.exists_representative_abs_center_le

theorem DivergenceFormProcess.Decay.setIntegral_mul_extendByZero {d : ℕ} {W V : Set (HCPolySupport.Vec d)} (hW : IsOpen W) (hV : IsOpen V) (hVW : V ⊆ W) (g : HCPolySupport.Vec d → ℝ) (phi : HCPolySupport.H10Function V) : ∫ (p : HCPolySupport.Vec d) in W, g p * (phi.extendByZeroToOpenSuperset ⋯ hW hVW).toFun p = ∫ (p : HCPolySupport.Vec d) in V, g p * phi.toFun p

The zero extension of a test function pairs with a fixed scalar field exactly as the original test function does.

theorem DivergenceFormProcess.Decay.zerothOrderOn_restrict_of_isScalarForcedWeakSolution {d : ℕ} {a : HCPolySupport.CoeffField d} {W V : Set (HCPolySupport.Vec d)} (hW : IsOpen W) (hV : IsOpen V) (hVW : V ⊆ W) {g : HCPolySupport.Vec d → ℝ} {u : HCPolySupport.H1Function W} (h : Form.IsScalarForcedWeakSolution a W g u) : Algsuperdiff.StochasticProcess.Common.Regularity.Ported.IsMatrixDivFormWeakSolutionZerothOrderOn a V (u.restrict hV hVW) g 0

The pointwise scalar equation restricts from an open set to an open subset, in the zeroth-order carrier consumed by the Schauder chain.

theorem DivergenceFormProcess.Decay.memScalarLInfOn_of_ae_abs_le {d : ℕ} {W : Set (HCPolySupport.Vec d)} {g : HCPolySupport.Vec d → ℝ} {G : ℝ} (hmeas : MeasureTheory.AEStronglyMeasurable g (MeasureTheory.volume.restrict W)) (hbound : ∀ᵐ (x : HCPolySupport.Vec d) ∂MeasureTheory.volume.restrict W, |g x| ≤ G) : Algsuperdiff.StochasticProcess.Common.Regularity.Ported.MemScalarLInfOn W g

An essential bound gives membership in the L^infinity carrier.

theorem DivergenceFormProcess.Decay.scalarLInfSizeOn_le_of_ae_abs_le {d : ℕ} {W : Set (HCPolySupport.Vec d)} {g : HCPolySupport.Vec d → ℝ} {G : ℝ} (hG : 0 ≤ G) (hbound : ∀ᵐ (x : HCPolySupport.Vec d) ∂MeasureTheory.volume.restrict W, |g x| ≤ G) : Algsuperdiff.StochasticProcess.Common.Regularity.Ported.scalarLInfSizeOn W g ≤ G

An essential bound bounds the L^infinity size.

theorem DivergenceFormProcess.Decay.exists_representative_abs_center_le {d : ℕ} [NeZero d] {a : HCPolySupport.CoeffField d} {Om : Set (HCPolySupport.Vec d)} (hOm : IsOpen Om) {u : HCPolySupport.H1Function Om} {g : HCPolySupport.Vec d → ℝ} {G E delta alpha : ℝ} (hd : 2 ≤ d) (halpha : alpha ∈ Set.Ico (1 / 2) 1) (hdelta0 : 0 ≤ delta) (hdelta : delta ≤ Algsuperdiff.StochasticProcess.Common.Regularity.Ported.smallContrastThreshold d alpha) (hameas : Measurable a) (ha : Algsuperdiff.StochasticProcess.Common.Regularity.Ported.CoefficientIdentityDistanceLE Om a delta) (hsol : Form.IsScalarForcedWeakSolution a Om g u) {x₀ : HCPolySupport.Vec d} {r : ℝ} (hr : 0 < r) (hball : HCPolySupport.euclideanBall x₀ r ⊆ Om) (hG : 0 ≤ G) (hgb : ∀ᵐ (x : HCPolySupport.Vec d) ∂HCPolySupport.volumeMeasureOn (HCPolySupport.euclideanBall x₀ r), |g x| ≤ G) (hE : Algsuperdiff.StochasticProcess.Common.Regularity.Ported.vectorLpSizeOn (HCPolySupport.euclideanBall x₀ r) 2 u.grad ≤ E) : ∃ (v : HCPolySupport.Vec d → ℝ), ContinuousOn v (HCPolySupport.euclideanBall x₀ (r / 2)) ∧ v =ᵐ[MeasureTheory.volume.restrict (HCPolySupport.euclideanBall x₀ r)] u.toFun ∧ ∀ (rho : ℝ), 0 < rho → rho ≤ r / 2 → |v x₀| ≤ √(∫ (y : HCPolySupport.Vec d) in HCPolySupport.euclideanBall x₀ rho, u.toFun y ^ 2) / √((MeasureTheory.volume (Algsuperdiff.StochasticProcess.Common.Regularity.Ported.smallContrastUnitBall d)).toReal * rho ^ d) + Algsuperdiff.StochasticProcess.Common.Regularity.Ported.smallContrastZerothSchauderConstant d * (r ^ (1 - alpha - ↑d / 2) * E + r ^ (2 - alpha) * G) * rho ^ alpha

Interior pointwise bound at the centre of a ball, under small contrast. The value of the continuous representative at the centre is bounded by the L² average on every concentric sub-ball of radius at most r / 2, plus the Schauder Hölder modulus at that radius.