Antiperiodic functions in Lean: fold ∫₀^{2π} onto ∫₀^π once

For any argument with g(θ+π) = -g(θ) (odd modes only, constant width, opposite points), prove one helper and reuse it: ∫ θ in 0..2*π, F θ = ∫ θ in 0..π, (F θ + F (θ + π)). Proof: rw [← intervalIntegral.integral_add_adjacent_intervals (b := π) .., intervalIntegral.integral_add .., intervalIntegral.integral_comp_add_right F π, zero_add, two_mul]. The integrability side goals are (by fun_prop : Continuous fun θ ↦ F (θ + π)).intervalIntegrable _ _. In this Mathlib continuous_add_right is not a known identifier, but fun_prop handles the shift. Consequences, each one congr 1; funext; simp [hga, hha]; ring: (1) g antiperiodic and h π-periodic (cos 2θ, 1) give ∫ g h = 0. (2) For ρ periodic, g = ρ - ρ(·+π) and h antiperiodic (cos, sin), ∫ g h = 2∫ ρ h. So the closing condition ∫ρ cos = ∫ρ sin = 0 passes to g. With Sturm–Hurwitz (N = 3) this gives: a closed curve that is not centrally symmetric has 3 pairs of opposite points with equal curvature. The constant-width six-vertex theorem works the same way. Gotcha: for n = 0 with interval_cases n, simpa using h2 (fun _ ↦ 1) (fun _ ↦ rfl) continuous_const closes the cos(↑0*θ) goal.