Time Cutoff

Part of the Caffarelli–Kohn–Nirenberg partial regularity proof.

noncomputable def CKN.backwardTimeCutoff (t h s : ℝ) : ℝ

A smooth backward cutoff with its transition confined to a time interval.

Equations

• CKN.backwardTimeCutoff t h s = 1 - CKN.smoothTransitionProfile ((s - (t - h / 2)) / (h / 2))

theorem CKN.backwardTimeCutoff_smooth {t h : ℝ} : ContDiff ℝ (↑⊤) (backwardTimeCutoff t h)

theorem CKN.backwardTimeCutoff_nonneg {t h s : ℝ} : 0 ≤ backwardTimeCutoff t h s

theorem CKN.backwardTimeCutoff_le_one {t h s : ℝ} : backwardTimeCutoff t h s ≤ 1

theorem CKN.backwardTimeCutoff_eq_one_of_le {t h s : ℝ} (hh : 0 < h) (hs : s ≤ t - h) : backwardTimeCutoff t h s = 1

theorem CKN.backwardTimeCutoff_eq_zero_of_ge {t h s : ℝ} (hh : 0 < h) (hs : t ≤ s) : backwardTimeCutoff t h s = 0

theorem CKN.backwardTimeCutoff_deriv_nonpos {t h s : ℝ} (hh : 0 < h) : deriv (backwardTimeCutoff t h) s ≤ 0

theorem CKN.backwardTimeCutoff_abs_deriv_le {t h s : ℝ} (hh : 0 < h) : |deriv (backwardTimeCutoff t h) s| ≤ 16 / h

theorem CKN.backwardTimeCutoff_integral_deriv {t h : ℝ} (hh : 0 < h) : ∫ (s : ℝ) in t - h..t, deriv (backwardTimeCutoff t h) s = -1

theorem CKN.backwardTimeCutoff_kernel_support {t h : ℝ} (hh : 0 < h) : (Function.support fun (s : ℝ) => -deriv (backwardTimeCutoff t h) s) ⊆ Set.Icc (t - h) t

theorem CKN.backwardTimeCutoff_kernel_integral {t h : ℝ} (hh : 0 < h) : ∫ (s : ℝ), -deriv (backwardTimeCutoff t h) s = 1