Documentation

LeanPool.AnomalousDiffusion.AVenhance.Infra.Cutoff.CardinalZeta

The smooth, compactly supported part of the small time partition.

source
noncomputable def AVenhance.Infra.Cutoff.zetaWidth :
ℝ

Width of the transition zone, chosen from the cardinal step's quadratic mass.

Equations
Instances For
    source
    noncomputable def AVenhance.Infra.Cutoff.zetaCoreRadius :
    ℝ

    Radius of the region on which the small cutoff is identically one.

    Equations
    Instances For
      source
      noncomputable def AVenhance.Infra.Cutoff.zetaOuterRadius :
      ℝ

      Outer radius of the small cutoff's support.

      Equations
      Instances For
        source
        theorem AVenhance.Infra.Cutoff.zetaWidth_pos :
        0 < zetaWidth
        source
        theorem AVenhance.Infra.Cutoff.zetaWidth_le_one_third :
        zetaWidth ≤ 1 / 3
        source
        theorem AVenhance.Infra.Cutoff.zetaWidth_lt_one :
        zetaWidth < 1
        source
        theorem AVenhance.Infra.Cutoff.zetaCoreRadius_pos :
        0 < zetaCoreRadius
        source
        theorem AVenhance.Infra.Cutoff.zetaCoreRadius_add_width :
        zetaCoreRadius + zetaWidth = 1 - zetaCoreRadius
        source
        theorem AVenhance.Infra.Cutoff.zetaOuterRadius_sub_coreRadius :
        zetaOuterRadius - zetaCoreRadius = zetaWidth
        source
        theorem AVenhance.Infra.Cutoff.zetaSupportRadius_le :
        zetaCoreRadius + zetaWidth ≤ 2 / 3
        source
        theorem AVenhance.Infra.Cutoff.zetaOuterRadius_le_one :
        zetaOuterRadius ≤ 1
        source
        noncomputable def AVenhance.Infra.Cutoff.cardinalZeta (t : ℝ) :
        ℝ

        The small time cutoff. Its transition profile is the flatter cardinal smooth step.

        Equations
        • One or more equations did not get rendered due to their size.
        Instances For
          source
          theorem AVenhance.Infra.Cutoff.cardinalZeta_contDiff :
          ContDiff ℝ (↑⊤) cardinalZeta
          source
          theorem AVenhance.Infra.Cutoff.cardinalZeta_nonneg (t : ℝ) :
          0 ≤ cardinalZeta t
          source
          theorem AVenhance.Infra.Cutoff.cardinalZeta_le_one (t : ℝ) :
          cardinalZeta t ≤ 1
          source
          theorem AVenhance.Infra.Cutoff.cardinalZeta_eq_one {t : ℝ} (ht₁ : -zetaCoreRadius ≤ t) (ht₂ : t ≤ zetaCoreRadius) :
          cardinalZeta t = 1
          source
          theorem AVenhance.Infra.Cutoff.cardinalZeta_eq_zero_of_le {t : ℝ} (ht : t ≤ -zetaOuterRadius) :
          cardinalZeta t = 0
          source
          theorem AVenhance.Infra.Cutoff.cardinalZeta_eq_zero_of_ge {t : ℝ} (ht : zetaOuterRadius ≤ t) :
          cardinalZeta t = 0
          source
          theorem AVenhance.Infra.Cutoff.cardinalZeta_even (t : ℝ) :
          cardinalZeta (-t) = cardinalZeta t
          source
          theorem AVenhance.Infra.Cutoff.cardinalZeta_le_indIcc (t : ℝ) :
          cardinalZeta t ≤ indIcc (-(2 / 3)) (2 / 3) t
          source
          theorem AVenhance.Infra.Cutoff.cardinalZeta_compact :
          HasCompactSupport cardinalZeta
          source
          theorem AVenhance.Infra.Cutoff.cardinalZeta_deriv_bound (N : ℕ) :
          ∃ (C : ℝ), 1 ≤ C ∧ ∀ j ≤ N, ∀ (t : ℝ), |iteratedDeriv j cardinalZeta t| ≤ C
          source
          theorem AVenhance.Infra.Cutoff.cardinalZeta_eq_cellCutoff (t : ℝ) :
          cardinalZeta t = cellCutoff cardinalStep 1 (zetaWidth / 2) t
          source
          theorem AVenhance.Infra.Cutoff.cardinalZeta_partition (t : ℝ) :
          ∑' (k : ℤ), cardinalZeta (t - ↑k) = 1