Normal and phase cutoffs for short-time vanishing

The cutoff in lem:bu-small-time turns on above the normal transition and on the positive shifted phase region.

noncomputable def ESS.buShortYMinus (scale : ℝ) : ℝ

The lower edge of the normal cutoff transition.

Equations

• ESS.buShortYMinus scale = 3 / scale + 1

noncomputable def ESS.buShortNormalCutoff (scale y : ℝ) : ℝ

The smooth normal cutoff.

Equations

• ESS.buShortNormalCutoff scale y = CKN.smoothTransitionProfile ((y - ESS.buShortYMinus scale) / (ESS.buShortYPlus scale - ESS.buShortYMinus scale))

noncomputable def ESS.buShortPhaseCutoff (u : ℝ) : ℝ

The smooth shifted-phase cutoff.

Equations

• ESS.buShortPhaseCutoff u = CKN.smoothTransitionProfile (12 * u + 9)

noncomputable def ESS.buShortCutoff (scale y s : ℝ) : ℝ

The product of the normal and shifted-phase cutoffs.

Equations

• ESS.buShortCutoff scale y s = ESS.buShortNormalCutoff scale y * ESS.buShortPhaseCutoff ((ESS.buShortF y s - ESS.buShortB scale) / ESS.buShortB scale)

theorem ESS.buShortYPlus_sub_YMinus (scale : ℝ) : buShortYPlus scale - buShortYMinus scale = 1 / 2

The normal transition interval has width one half.

theorem ESS.buShortNormalCutoff_eq_zero {scale y : ℝ} (hy : y ≤ buShortYMinus scale) : buShortNormalCutoff scale y = 0

The normal cutoff vanishes below its lower transition height.

theorem ESS.buShortNormalCutoff_eq_one {scale y : ℝ} (hy : buShortYPlus scale ≤ y) : buShortNormalCutoff scale y = 1

The normal cutoff equals one above its upper transition height.

theorem ESS.buShortPhaseCutoff_eq_zero {u : ℝ} (hu : u ≤ -(3 / 4)) : buShortPhaseCutoff u = 0

The phase cutoff vanishes below the lower transition level.

theorem ESS.buShortPhaseCutoff_eq_one {u : ℝ} (hu : -(2 / 3) ≤ u) : buShortPhaseCutoff u = 1

The phase cutoff equals one above the upper transition level.

theorem ESS.buShortCutoff_eq_zero_of_low_phase {scale y s : ℝ} (hphase : (buShortF y s - buShortB scale) / buShortB scale ≤ -(3 / 4)) : buShortCutoff scale y s = 0

The product cutoff vanishes below the lower shifted-phase level.

theorem ESS.buShortCutoff_eq_one_above_gap {scale y s : ℝ} (hscale : 0 < scale) (hy : 0 ≤ y) (hs : 1 / 2 ≤ s) (hs1 : s ≤ 1) (hphase : -buShortD scale / 2 < buShortF y s - buShortB scale) : buShortCutoff scale y s = 1

The cutoff is one throughout the region above its negative phase transition gap.