LocalizedTailProfile

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

The stream-field localized resolvent-tail profile

The logarithmic local constants in the two scale ranges give a pointwise log-subexponential profile. This module keeps the algebraic prefactor explicit and proves its finite cubic layer-cake budget.

noncomputable def Algsuperdiff.Section5.Field.streamPointLogWeight {d : ℕ} (x : HCPolySupport.Vec d) : ℝ

The point-dependent logarithmic weight.

Equations

• Algsuperdiff.Section5.Field.streamPointLogWeight x = Algsuperdiff.Section5.Field.streamLogWeight (1 + HCPolySupport.euclideanNorm x)

noncomputable def Algsuperdiff.Section5.Field.streamLocalizedUpperBase {d : ℕ} (M : Section3.ABKModel d) (omega : FullSample d M.gamma) (x : HCPolySupport.Vec d) : ℝ

The radius-independent coefficient in the logarithmic upper bound for the localized weighted estimate.

Equations

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

theorem Algsuperdiff.Section5.Field.streamLocalizedUpperBase_pos {d : ℕ} (M : Section3.ABKModel d) (omega : FullSample d M.gamma) (x : HCPolySupport.Vec d) : 0 < streamLocalizedUpperBase M omega x

theorem Algsuperdiff.Section5.Field.localizedAgmonUpper_stream_le {d : ℕ} (M : Section3.ABKModel d) (omega : FullSample d M.gamma) (x : HCPolySupport.Vec d) {mu r s : ℝ} (hmu : 1 ≤ mu) (hr : 0 ≤ r) (hrs : r ≤ s) : DivergenceFormProcess.Decay.localizedAgmonUpper M.nu mu (streamFieldSmallLocalConst M omega x r) (streamFieldLargeDivLocalConst M omega x r) ≤ streamLocalizedUpperBase M omega x * streamLogWeight (1 + s)

The effective upper constant at radius r = s / sqrt mu is at most its point-dependent base times 1 + log (1+s), uniformly for mu ≥ 1.

noncomputable def Algsuperdiff.Section5.Field.streamTailInnerFloor {d : ℕ} (M : Section3.ABKModel d) (omega : FullSample d M.gamma) (x : HCPolySupport.Vec d) : ℝ

A positive lower floor for the dimensionless frozen radius when the outer dimensionless scale is beyond one and the mass is at least one.

Equations

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

theorem Algsuperdiff.Section5.Field.streamTailInnerFloor_pos {d : ℕ} (M : Section3.ABKModel d) (omega : FullSample d M.gamma) (x : HCPolySupport.Vec d) : 0 < streamTailInnerFloor M omega x

noncomputable def Algsuperdiff.Section5.Field.streamTailDecayRate {d : ℕ} (M : Section3.ABKModel d) (omega : FullSample d M.gamma) (x : HCPolySupport.Vec d) : ℝ

The pointwise log-subexponential decay rate.

Equations

• Algsuperdiff.Section5.Field.streamTailDecayRate M omega x = DivergenceFormProcess.Decay.agmonTailRate d M.nu (Algsuperdiff.Section5.Field.streamLocalizedUpperBase M omega x) (1 / 2)

noncomputable def Algsuperdiff.Section5.Field.streamTailAlgebraicAmplitude {d : ℕ} (M : Section3.ABKModel d) (omega : FullSample d M.gamma) (x : HCPolySupport.Vec d) : ℝ

The explicit algebraic amplitude. Its two summands respectively control the averaged/gradient terms and the bounded-forcing term of the frozen tail.

Equations

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

noncomputable def Algsuperdiff.Section5.Field.streamLocalizedTailProfile {d : ℕ} (M : Section3.ABKModel d) (omega : FullSample d M.gamma) (x : HCPolySupport.Vec d) : ℝ → ℝ

The explicit profile for item 3 of PACKET_M2_28b.

Equations

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

theorem Algsuperdiff.Section5.Field.streamTailAlgebraicAmplitude_nonneg {d : ℕ} (M : Section3.ABKModel d) (omega : FullSample d M.gamma) (x : HCPolySupport.Vec d) : 0 ≤ streamTailAlgebraicAmplitude M omega x

theorem Algsuperdiff.Section5.Field.streamLocalizedSplitData_tail_le_profile {d : ℕ} [NeZero d] (M : Section3.ABKModel d) (omega : FullSample d M.gamma) (mu : ↑MarkovProcess.Semigroup.PositiveShift) (x : HCPolySupport.Vec d) (hmu : 1 ≤ ↑mu) {s : ℝ} (hs : 1 < s) : (streamLocalizedSplitData M omega).tail mu x (s / √↑mu) ≤ streamLocalizedTailProfile M omega x s

The exact localized two-scale tail is bounded by the explicit log-subexponential profile, uniformly in every mass mu ≥ 1.

theorem Algsuperdiff.Section5.Field.mul_toReal_streamAnalyticMinimalResolvent_le_profile {d : ℕ} [NeZero d] (M : Section3.ABKModel d) (omega : FullSample d M.gamma) (mu : ↑MarkovProcess.Semigroup.PositiveShift) (hmu : 1 ≤ ↑mu) {f : HCPolySupport.Vec d → ℝ} (hf : Measurable f) (hf0 : ∀ (x : HCPolySupport.Vec d), 0 ≤ f x) (hf1 : ∀ (x : HCPolySupport.Vec d), |f x| ≤ 1) {x : HCPolySupport.Vec d} {r : ℝ} (hr : 0 < r) (hs : 1 < √↑mu * r) (hzero : ∀ y ∈ HCPolySupport.euclideanBall x r, f y = 0) : ↑mu * ((streamWholeSpaceAnalyticData M omega).analyticMinimalResolvent mu f hf hf1 x).toReal ≤ streamLocalizedTailProfile M omega x (√↑mu * r)

The analytic minimal resolvent inherits the explicit pointwise log-subexponential profile. The estimate is uniform over the exhaustion cubes used to define the minimal resolvent.