Kato Regularization

Supporting results for the Constantin–Ignatova–Vicol axisymmetric regularity theorem.

noncomputable def CIV.katoSmooth (kap : ℝ) (g : ℝ → ℝ) (x : ℝ) : ℝ

The smooth positive part: katoSmooth kap g x is a smooth approximation of max (g x) 0 that equals (g x + |g x|)/2 when kap = 0.

Equations

• CIV.katoSmooth kap g x = (g x + √(g x ^ 2 + kap ^ 2)) / 2 - kap / 2

theorem CIV.max_eq_add_abs_div_two (a : ℝ) : max a 0 = (a + |a|) / 2

The identity max a 0 = (a + |a|) / 2.

theorem CIV.radicand_pos (kap : ℝ) (g : ℝ → ℝ) (x : ℝ) (hkap : kap ≠ 0) : 0 < g x ^ 2 + kap ^ 2

The radicand g x ^ 2 + kap ^ 2 is strictly positive when kap ≠ 0.

theorem CIV.radicand_ne_zero (kap : ℝ) (g : ℝ → ℝ) (x : ℝ) (hkap : 0 < kap) : g x ^ 2 + kap ^ 2 ≠ 0

The radicand g x ^ 2 + kap ^ 2 is nonzero when kap > 0.

theorem CIV.katoSmooth_le_posPart (kap : ℝ) (hkap : 0 < kap) (g : ℝ → ℝ) (x : ℝ) : katoSmooth kap g x ≤ max (g x) 0

theorem CIV.posPart_sub_katoSmooth_le (kap : ℝ) (g : ℝ → ℝ) (x : ℝ) : max (g x) 0 - katoSmooth kap g x ≤ kap / 2

theorem CIV.contDiff_katoSmooth {n : WithTop ℕ∞} (kap : ℝ) (hkap : 0 < kap) {g : ℝ → ℝ} (hg : ContDiff ℝ n g) : ContDiff ℝ n (katoSmooth kap g)

theorem CIV.tendsto_katoSmooth (g : ℝ → ℝ) (x : ℝ) : Filter.Tendsto (fun (kap : ℝ) => katoSmooth kap g x) (nhdsWithin 0 (Set.Ioi 0)) (nhds (max (g x) 0))