Axis Parabolic Boundary

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

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

The parabolic boundary Σ of lem:aniso:axis: the initial slice and the lateral half-circle.

Equations

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