Documentation

LeanPool.AnomalousDiffusion.AVenhance.Infra.Section4.Amnr.StreamMaterialSum

Material jets of the actual locally finite stream increment.

theorem AVenhance.Infra.Section4.amnr_zeta_local_finite {β : ℝ} (I : Ingredients β) (m : ℕ) (t : ℝ) :
∃ (s : Finset ℤ), s.card ≤ 3 ∧ ∀ (u : ℝ), |u - t| < tau β I.Λ m / 8 → ∀ k ∉ s, I.zetaMK m k u = 0

Fine cutoffs have three possible indices on a fixed open time neighborhood. This controls all differentiated stream sums.