Blowup Cutoff Time

Cutoff bounds used to localize the rescaled endpoint sequence.

noncomputable def ESS.blowupTimeCutoff (a b t : ℝ) : ℝ

A smooth time cutoff equal to one on [a,b], supported strictly below zero, with a fixed rising transition and a movable falling transition.

Equations

• ESS.blowupTimeCutoff a b t = CKN.smoothTransitionProfile (t - (a - 1)) * CKN.smoothTransitionProfile ((b / 2 - t) / (-b / 2))

theorem ESS.blowupTimeCutoff_smooth (a b : ℝ) : ContDiff ℝ (↑⊤) (blowupTimeCutoff a b)

The time cutoff is smooth when the upper plateau endpoint is negative.

theorem ESS.blowupTimeCutoff_bounds (a b t : ℝ) : 0 ≤ blowupTimeCutoff a b t ∧ blowupTimeCutoff a b t ≤ 1

The cutoff takes values in [0,1].

theorem ESS.blowupTimeCutoff_eq_one {a b t : ℝ} (hb : b < 0) (hat : a ≤ t) (htb : t ≤ b) : blowupTimeCutoff a b t = 1

The cutoff equals one throughout its intended time interval.

theorem ESS.blowupTimeCutoff_zero_left {a b t : ℝ} (ht : t ≤ a - 1) : blowupTimeCutoff a b t = 0

The cutoff vanishes to the left of its fixed rising transition.

theorem ESS.blowupTimeCutoff_zero_right {a b t : ℝ} (hb : b < 0) (ht : b / 2 ≤ t) : blowupTimeCutoff a b t = 0

The cutoff vanishes beyond the upper transition.

theorem ESS.blowupTimeCutoff_hasCompactSupport (a b : ℝ) (hb : b < 0) : HasCompactSupport (blowupTimeCutoff a b)

The cutoff has compact support inside the source past interval.

theorem ESS.blowupTimeCutoff_tsupport_subset (a b : ℝ) (hb : b < 0) : tsupport (blowupTimeCutoff a b) ⊆ Set.Icc (a - 1) (b / 2)

The closed support of the cutoff stays a positive distance from time zero.

theorem ESS.blowupTimeCutoff_tsupport_subset_open (a b : ℝ) (hb : b < 0) : tsupport (blowupTimeCutoff a b) ⊆ Set.Ioo (a - 2) 0

The support is strictly inside any past interval beginning one unit before the rising transition.

theorem ESS.blowupTimeCutoff_deriv_le_eight (a b t : ℝ) (hb : b < 0) : deriv (blowupTimeCutoff a b) t ≤ 8

The positive time derivative of the cutoff is bounded independently of the upper transition width.