Lengths

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

noncomputable def CIV.radialLength (t : ℝ) : ℝ

The radial length ℓ_r(t) = (−t)^{1/2} of eq:aniso:lengths.

Equations

• CIV.radialLength t = (-t) ^ (1 / 2)

noncomputable def CIV.axialLength (h t : ℝ) : ℝ

The axial length ℓ_z(t) = (−t)^{1/2 − h} of eq:aniso:lengths.

Equations

• CIV.axialLength h t = (-t) ^ (1 / 2 - h)

noncomputable def CIV.lengthRatio (h t : ℝ) : ℝ

The ratio δ = ℓ_r/ℓ_z = (−t)^h of eq:aniso:zoom:lengths.

Equations

• CIV.lengthRatio h t = (-t) ^ h

theorem CIV.radialLength_rpow_two_mul {t : ℝ} (ht : t < 0) (h : ℝ) : radialLength t ^ (2 * h) = lengthRatio h t

theorem CIV.radialLength_rpow_one_sub {t : ℝ} (ht : t < 0) (h : ℝ) : radialLength t ^ (1 - 2 * h) = axialLength h t

theorem CIV.radialLength_eq_mul {t : ℝ} (ht : t < 0) (h : ℝ) : radialLength t = lengthRatio h t * axialLength h t

theorem CIV.radialLength_sq {t : ℝ} (ht : t < 0) : radialLength t ^ 2 = -t

theorem CIV.tendsto_radialLength : Filter.Tendsto radialLength (nhdsWithin 0 (Set.Iio 0)) (nhds 0)

theorem CIV.tendsto_lengthRatio {h : ℝ} (hh : 0 < h) : Filter.Tendsto (lengthRatio h) (nhdsWithin 0 (Set.Iio 0)) (nhds 0)

theorem CIV.tendsto_axialLength {h : ℝ} (hh : h < 1 / 2) : Filter.Tendsto (axialLength h) (nhdsWithin 0 (Set.Iio 0)) (nhds 0)

theorem CIV.tendsto_neg_rpow_of_pos {a : ℝ} (ha : 0 < a) : Filter.Tendsto (fun (t : ℝ) => (-t) ^ a) (nhdsWithin 0 (Set.Iio 0)) (nhds 0)