SourceExponent #
Ported from scottnarmstrong/Superdiffusion at 7f20476385d4af418f110303085ad0740c9eba46. Module imports, support namespace and local option directives adapted for Lean Pool.
Arithmetic of the source exponent #
The energy test uses the embedding L^p(B_1) ⊆ L²(B_r). It is valid in
the manuscript's regime d ≥ 2; this file makes that otherwise implicit
dimension restriction and the identity d / p = 1 - alpha explicit.
theorem
Algsuperdiff.StochasticProcess.Common.Regularity.Ported.two_le_schauderSourceExponent
{d : ℕ}
{alpha : ℝ}
(hd : 2 ≤ d)
(halpha0 : 0 ≤ alpha)
(halpha1 : alpha < 1)
:
In the intended PDE dimensions, the printed exponent is at least two, so
the L^p datum can be used in the quadratic energy test.
theorem
Algsuperdiff.StochasticProcess.Common.Regularity.Ported.dimension_div_schauderSourceExponent
{d : ℕ}
{alpha : ℝ}
(hd : 1 ≤ d)
(halpha : alpha < 1)
:
The scale exponent in the forcing row is exactly 1-alpha.