The normal Carleman phase for short-time vanishing

At exponent three quarters the normal part of the weight in lem:bu-small-time increases in height and decreases in time.

noncomputable def ESS.buShortF (y s : ℝ) : ℝ

The normal part of the half-space Carleman phase at exponent three quarters.

Equations

• ESS.buShortF y s = (1 - s) * y ^ (3 / 2) * s ^ (-(3 / 4))

theorem ESS.buShortF_pos {y s : ℝ} (hy : 0 < y) (hs : 0 < s) (hs1 : s < 1) : 0 < buShortF y s

The normal phase is positive at positive height and time below one.

theorem ESS.buShortF_mono_height {y₁ y₂ s : ℝ} (hy₁ : 0 ≤ y₁) (hyle : y₁ ≤ y₂) (hs : 0 < s) (hs1 : s ≤ 1) : buShortF y₁ s ≤ buShortF y₂ s

At fixed time the normal phase increases with height.

theorem ESS.buShortF_antitone_time {y s₀ s₁ : ℝ} (hy : 0 ≤ y) (hs₀ : 0 < s₀) (hsle : s₀ ≤ s₁) (hs₁ : s₁ ≤ 1) : buShortF y s₁ ≤ buShortF y s₀

At fixed height the normal phase decreases with time.