Axis Domain

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

def CIV.axisDomain (R t₁ s : ℝ) : Set ((ℝ × ℝ) × ℝ)

The half-disc {r > 0, r² + z² < R²} with the times (t₁, s]: the set D of lem:aniso:axis.

Equations

• CIV.axisDomain R t₁ s = {p : (ℝ × ℝ) × ℝ | 0 < p.1.1 ∧ p.1.1 ^ 2 + p.1.2 ^ 2 < R ^ 2 ∧ t₁ < p.2 ∧ p.2 ≤ s}