Cardinal Mass

Support for the Armstrong–Vicol anomalous-diffusion formalization.

noncomputable def AVenhance.Infra.Cutoff.cardinalMass : ℝ

The quadratic mass of the cardinal smooth step on the unit interval.

Equations

• AVenhance.Infra.Cutoff.cardinalMass = ∫ (x : ℝ) in 0..1, AVenhance.Infra.Cutoff.cardinalStep x * (1 - AVenhance.Infra.Cutoff.cardinalStep x)

theorem AVenhance.Infra.Cutoff.cardinalMass_lower : 9 / 50 ≤ cardinalMass

theorem AVenhance.Infra.Cutoff.cardinalMass_pos : 0 < cardinalMass