ExhaustionTailInput #
Ported from scottnarmstrong/Superdiffusion at 7f20476385d4af418f110303085ad0740c9eba46. Module imports, support namespace and local option directives adapted for Lean Pool.
The stream-field variable exhaustion-tail input #
The amplified pointwise analytic tail is transported to the exhaustion metric and packaged with the shift-dependent uniform profile. Above the cubic-log cutoff this is the localized stream-field estimate; below it the normalized potential-mass bound supplies the unit estimate.
theorem
Algsuperdiff.Section5.Field.stream_liveTail_le_uniform
{d : ℕ}
[NeZero d]
(M : Section3.ABKModel d)
(omega : FullSample d M.gamma)
(R : MarkovProcess.PositiveC0ContractiveResolvent (HCPolySupport.Vec d))
(hid : (streamWholeSpaceAnalyticData M omega).KernelResolventIdentifiesAnalyticMinimal R)
(mu : ↑MarkovProcess.Semigroup.PositiveShift)
(hmu : 1 ≤ ↑mu)
(x : HCPolySupport.Vec d)
(r : ℝ)
(hr : 0 < r)
:
ENNReal.ofReal ↑mu * (R.kernelSemigroup.resolventPotential (↑mu) x) (Metric.ball x (streamExhaustionAmp x r))ᶜ ≤ ENNReal.ofReal (streamUniformExhaustionProfile M omega (↑mu) (√↑mu * r))
noncomputable def
Algsuperdiff.Section5.Field.streamVariableExhaustionTailInput
{d : ℕ}
[NeZero d]
(M : Section3.ABKModel d)
(omega : FullSample d M.gamma)
(R : MarkovProcess.PositiveC0ContractiveResolvent (HCPolySupport.Vec d))
(hid : (streamWholeSpaceAnalyticData M omega).KernelResolventIdentifiesAnalyticMinimal R)
(hcons : R.kernelSemigroup.IsConservative)
:
The stream-field profile and reciprocal-norm exhaustion provide the
shift-dependent one-point resolvent-tail input with time exponent 3/2.
Equations
- One or more equations did not get rendered due to their size.