ExponentialPointwise

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

Pointwise exponential decay under small contrast

Combining the interior pointwise estimate with the radius balance turns an exponentially small local L² size into an exponentially small pointwise value, at the reduced rate kappa * alpha / (alpha + d / 2). The balance is taken over the radii the interior estimate allows, up to r / 2, so the statement holds at every scale r and the constant carries the explicit powers of r.

The small-contrast hypothesis comes from the interior Schauder estimate that supplies the Hölder modulus. For a general elliptic field the same conclusion would need a De Giorgi--Nash--Moser local boundedness estimate, which the layer does not carry.

Main results

• DivergenceFormProcess.Decay.exists_representative_abs_center_le_exp

theorem DivergenceFormProcess.Decay.unitBallVolume_pos {d : ℕ} : 0 < (MeasureTheory.volume (Algsuperdiff.StochasticProcess.Common.Regularity.Ported.smallContrastUnitBall d)).toReal

The unit ball carries positive volume.

theorem DivergenceFormProcess.Decay.exists_representative_abs_center_le_exp {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) {kappa s D : ℝ} (hkappa : 0 ≤ kappa) (hs : 0 ≤ s) (hD : 0 ≤ D) (hL2 : ∀ (rho : ℝ), 0 < rho → rho ≤ r / 2 → ∫ (y : HCPolySupport.Vec d) in HCPolySupport.euclideanBall x₀ rho, u.toFun y ^ 2 ≤ D ^ 2 * Real.exp (-(2 * (kappa * s)))) : ∃ (v : HCPolySupport.Vec d → ℝ), ContinuousOn v (HCPolySupport.euclideanBall x₀ (r / 2)) ∧ v =ᵐ[MeasureTheory.volume.restrict (HCPolySupport.euclideanBall x₀ r)] u.toFun ∧ |v x₀| ≤ (D / √(MeasureTheory.volume (Algsuperdiff.StochasticProcess.Common.Regularity.Ported.smallContrastUnitBall d)).toReal / √((r / 2) ^ d) + Algsuperdiff.StochasticProcess.Common.Regularity.Ported.smallContrastZerothSchauderConstant d * (r ^ (1 - alpha - ↑d / 2) * E + r ^ (2 - alpha) * G) * (r / 2) ^ alpha) * Real.exp (-(kappa * alpha / (alpha + ↑d / 2) * s))

Pointwise exponential decay of the continuous representative at the centre of a ball, from an exponentially small local L² size.