Axis Closed Domain

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

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

The closed half-disc {r ≥ 0, r² + z² ≤ R²} with the times [t₁, s].

Equations

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