152theorem tf_pinch_at_zero_node (J : ℝ → ℝ) (_hJ_convex : ConvexOn ℝ (Set.Ioi 0) J) 153 (_hJ_zero : J 1 = 0) (hJ_pos : ∀ x, x ∈ Set.Ioi 0 → x ≠ 1 → J x > 0) : 154 ∀ x, x ∈ Set.Ioi 0 → J x = 0 → x = 1 := by
proof body
Term-mode proof.
155 intro x hx hJx 156 by_contra h 157 exact absurd hJx (ne_of_gt (hJ_pos x hx h)) 158 159/-! ## Rigid Rotation Identification -/ 160 161/-- A 2D velocity field with constant vorticity is a rigid rotation. 162 If ω(x) = ω₀ (constant) and u is divergence-free, then 163 u(x) = (ω₀/2) × (x - x₀) for some center x₀. 164 165 This is the content of the 2D Biot-Savart law for constant vorticity. 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. -/
used by (1)
From the project-wide theorem graph. These declarations reference this one in their body.