Documentation

LeanPool.AnomalousDiffusion.AVenhance.Infra.Cutoff.CardinalStep

A flatter smooth step used to tune the quadratic mass of the time partition.

noncomputable def AVenhance.Infra.Cutoff.cardinalArg (x : ℝ) :

An odd polynomial reparametrization of the unit interval.

Equations

AVenhance.Infra.Cutoff.cardinalArg x = 1 / 2 + 2 ^ 10 * (x - 1 / 2) ^ 11

Instances For

noncomputable def AVenhance.Infra.Cutoff.cardinalStep (x : ℝ) :

A smooth transition with a long central region.

Equations

AVenhance.Infra.Cutoff.cardinalStep x = AVenhance.Infra.Cutoff.step (AVenhance.Infra.Cutoff.cardinalArg x)

Instances For

theorem AVenhance.Infra.Cutoff.cardinalStep_contDiff :

ContDiff ℝ (↑⊤) cardinalStep

theorem AVenhance.Infra.Cutoff.cardinalArg_one_sub (x : ℝ) :

cardinalArg (1 - x) = 1 - cardinalArg x

theorem AVenhance.Infra.Cutoff.cardinalArg_le_zero {x : ℝ} (hx : x ≤ 0) :

cardinalArg x ≤ 0

theorem AVenhance.Infra.Cutoff.cardinalArg_one_le {x : ℝ} (hx : 1 ≤ x) :

1 ≤ cardinalArg x

theorem AVenhance.Infra.Cutoff.cardinalStep_zero_of_nonpos {x : ℝ} (hx : x ≤ 0) :

cardinalStep x = 0

theorem AVenhance.Infra.Cutoff.cardinalStep_one_of_one_le {x : ℝ} (hx : 1 ≤ x) :

cardinalStep x = 1

theorem AVenhance.Infra.Cutoff.cardinalStep_one_sub (x : ℝ) :

cardinalStep (1 - x) = 1 - cardinalStep x

theorem AVenhance.Infra.Cutoff.cardinalArg_mem_middle {x : ℝ} (hlo : 1 / 8 ≤ x) (hhi : x ≤ 7 / 8) :

15 / 32 ≤ cardinalArg x ∧ cardinalArg x ≤ 17 / 32

theorem AVenhance.Infra.Cutoff.CardinalStep.step_ge_two_fifths_middle {x : ℝ} (hlo : 15 / 32 ≤ x) (hhi : x ≤ 17 / 32) :

2 / 5 ≤ step x

theorem AVenhance.Infra.Cutoff.cardinalStep_mem_middle {x : ℝ} (hlo : 1 / 8 ≤ x) (hhi : x ≤ 7 / 8) :

2 / 5 ≤ cardinalStep x ∧ cardinalStep x ≤ 3 / 5

theorem AVenhance.Infra.Cutoff.cardinalStep_sq_complement_lower {x : ℝ} (hlo : 1 / 8 ≤ x) (hhi : x ≤ 7 / 8) :

6 / 25 ≤ cardinalStep x * (1 - cardinalStep x)