Negative phase on the cutoff transition region

The normal and time transitions in lem:bu-small-time lie in a region where the shifted Carleman phase is uniformly negative.

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

The upper edge of the normal cutoff transition.

Equations

• ESS.buShortYPlus scale = 3 / scale + 3 / 2

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

The reference height above the normal cutoff transition.

Equations

• ESS.buShortYZero scale = 3 / scale + 2

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

The positive phase shift used in the short-time Carleman argument.

Equations

• ESS.buShortB scale = 2 * ESS.buShortF (ESS.buShortYZero scale) (1 / 2)

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

A positive gap below both transition phase levels.

Equations

• ESS.buShortD scale = min (-2 * (ESS.buShortF (ESS.buShortYPlus scale) (1 / 2) - ESS.buShortB scale)) (4 * ESS.buShortB scale / 3)

theorem ESS.buShortYPlus_lt_YZero (scale : ℝ) : buShortYPlus scale < buShortYZero scale

The reference height lies strictly above the cutoff transition.

theorem ESS.buShortB_pos {scale : ℝ} (hscale : 0 < scale) : 0 < buShortB scale

The phase shift is positive at every positive spatial scale.

theorem ESS.buShortD_pos {scale : ℝ} (hscale : 0 < scale) : 0 < buShortD scale

The cutoff transition has a strictly negative phase gap.

theorem ESS.buShort_spatial_transition_phase_le {scale y s : ℝ} (hy : 0 ≤ y) (hyle : y ≤ buShortYPlus scale) (hs : 1 / 2 ≤ s) (hs1 : s ≤ 1) : buShortF y s - buShortB scale ≤ -buShortD scale / 2

The spatial cutoff transition lies at least half the phase gap below zero.

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

A positive shifted phase occurs above the completed normal cutoff.

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

Above the negative transition gap, the normal cutoff is complete.