constant_vorticity_implies_rigid_rotation

formal source

 166    It is the final step in Stage 5 of the NS paper: once we know the
 167    blowup profile has constant vorticity direction and magnitude,
 168    it must be a rigid rotation, which is excluded by the energy constraint. -/
 169theorem constant_vorticity_implies_rigid_rotation (ω₀ : ℝ) :
 170    ∃ (u : ℝ × ℝ → ℝ × ℝ), ∀ (x : ℝ × ℝ),
 171      u x = (ω₀ / 2 * (-x.2), ω₀ / 2 * x.1) := by
 172  exact ⟨fun x => (ω₀ / 2 * (-x.2), ω₀ / 2 * x.1), fun x => rfl⟩
 173
 174/-- Rigid rotations have infinite energy (‖u‖² = ∫ ω₀²|x|²/4 dx = ∞).
 175    This contradicts the finite-energy assumption on NS solutions.
 176
 177    **Proof sketch** (standard measure theory):
 178    In `ℝ × ℝ` with the sup metric, `B(0, R) = (-R, R)²`. By Fubini:
 179    `∫_{(-R,R)²} (ω₀/2)² (x² + y²) = (ω₀/2)² · 8R⁴/3`,
 180    which grows as R⁴ and exceeds any bound. The formal computation
 181    requires `MeasureTheory.integral_prod` + `intervalIntegral.integral_pow`.
 182
 183    Recorded as a named proposition; the physical consequence (no finite-energy
 184    rigid rotation) is used as a structural hypothesis in the NS blowup
 185    exclusion argument. -/
 186def rigid_rotation_infinite_energy (ω₀ : ℝ) (_ : ω₀ ≠ 0) : Prop :=
 187  ¬ ∃ E : ℝ, ∀ R > 0, ∫ x in Metric.ball (0 : ℝ × ℝ) R,
 188    (ω₀ / 2)^2 * (x.1^2 + x.2^2) ≤ E
 189
 190private theorem rigid_rotation_energy_lower_bound {ω₀ R : ℝ} (hω₀ : ω₀ ≠ 0) (hR : 0 < R) :
 191    ((ω₀ / 2) ^ 2) * R ^ 4 / 64 ≤
 192      ∫ x in Metric.ball (0 : ℝ × ℝ) R, ((ω₀ / 2) ^ 2) * (x.1 ^ 2 + x.2 ^ 2) := by
 193  let c : ℝ := (ω₀ / 2) ^ 2
 194  let rect : Set (ℝ × ℝ) := Set.Icc (R / 2) (3 * R / 4) ×ˢ Set.Icc 0 (R / 4)
 195  let f : ℝ × ℝ → ℝ := fun x => c * (x.1 ^ 2 + x.2 ^ 2)
 196  have hc_nonneg : 0 ≤ c := by
 197    dsimp [c]
 198    positivity
 199  have hrect_subset_ball : rect ⊆ Metric.ball (0 : ℝ × ℝ) R := by