Documentation

LeanPool.AnomalousDiffusion.AVenhance.Infra.Cutoff.CardinalIntegral

Exact quadratic mass of the cardinal small cutoff.

source
theorem AVenhance.Infra.Cutoff.CardinalIntegral.cardinalZeta_sq_left {t : ℝ} (ht₂ : t ≤ -zetaCoreRadius) :
cardinalZeta t ^ 2 = cardinalStep ((t + zetaOuterRadius) / zetaWidth) ^ 2
source
theorem AVenhance.Infra.Cutoff.CardinalIntegral.cardinalZeta_sq_right {t : ℝ} (ht₁ : zetaCoreRadius ≤ t) :
cardinalZeta t ^ 2 = cardinalStep ((zetaOuterRadius - t) / zetaWidth) ^ 2
source
noncomputable def AVenhance.Infra.Cutoff.CardinalIntegral.stepSquare (x : ℝ) :
ℝ

Square of the cardinal transition profile.

Equations
Instances For
    source
    noncomputable def AVenhance.Infra.Cutoff.CardinalIntegral.stepComplementSquare (x : ℝ) :
    ℝ

    Square of the complementary cardinal transition profile.

    Equations
    Instances For
      source
      theorem AVenhance.Infra.Cutoff.CardinalIntegral.stepSquare_integrable :
      IntervalIntegrable stepSquare MeasureTheory.volume 0 1
      source
      theorem AVenhance.Infra.Cutoff.CardinalIntegral.stepComplementSquare_integrable :
      IntervalIntegrable stepComplementSquare MeasureTheory.volume 0 1
      source
      theorem AVenhance.Infra.Cutoff.CardinalIntegral.stepProduct_integrable :
      IntervalIntegrable (fun (x : ℝ) => cardinalStep x * (1 - cardinalStep x)) MeasureTheory.volume 0 1
      source
      theorem AVenhance.Infra.Cutoff.CardinalIntegral.step_square_integral_eq_one_half_sub_mass :
      ∫ (x : ℝ) in 0..1, cardinalStep x ^ 2 = 1 / 2 - cardinalMass
      source
      theorem AVenhance.Infra.Cutoff.CardinalIntegral.square_profile_left_change :
      ∫ (t : ℝ) in -zetaOuterRadius..-zetaCoreRadius, cardinalStep ((t + zetaOuterRadius) / zetaWidth) ^ 2 = zetaWidth * ∫ (x : ℝ) in 0..1, cardinalStep x ^ 2
      source
      theorem AVenhance.Infra.Cutoff.CardinalIntegral.square_profile_right_change :
      ∫ (t : ℝ) in zetaCoreRadius..zetaOuterRadius, cardinalStep ((zetaOuterRadius - t) / zetaWidth) ^ 2 = zetaWidth * ∫ (x : ℝ) in 0..1, cardinalStep x ^ 2
      source
      theorem AVenhance.Infra.Cutoff.cardinalZeta_sq_integral :
      ∫ (t : ℝ), cardinalZeta t ^ 2 = 9 / 10