theorem
proved
term proof
constant_vorticity_implies_rigid_rotation
show as:
view Lean formalization →
formal statement (Lean)
169theorem constant_vorticity_implies_rigid_rotation (ω₀ : ℝ) :
170 ∃ (u : ℝ × ℝ → ℝ × ℝ), ∀ (x : ℝ × ℝ),
171 u x = (ω₀ / 2 * (-x.2), ω₀ / 2 * x.1) := by
proof body
Term-mode proof.
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. -/