Fix 2009 B4

This was disprovable because the integral was using the two-dimensional
measure from the plane in the integral on the one-dimensional set that
is the circle (and thus was always zero). We could fix this by supplying
the one-dimensional Hausdorff measure but this is too heavy-weight
given that we can just parameterise and use the interval integral.

A second error was the inclusion of the typeclasses `[AddCommGroup V]
[Module ℝ V]`. The subset already has this algebraic structure and by
supplying these there is ambiguity of which structure applies, as well
as the fact that these are arbitrary typeclasses with no relation to the
ambient structure on `MvPolynomial (Fin 2) ℝ`.

lean4/src/putnam_2009_b4.lean

@@ -1,16 +1,17 @@
 import Mathlib
 
-open Topology MvPolynomial Filter Set Metric
+open intervalIntegral MvPolynomial Real
 
 abbrev putnam_2009_b4_solution : ℕ := sorry
 -- 2020050
 /--
 Say that a polynomial with real coefficients in two variables, $x,y$, is \emph{balanced} if the average value of the polynomial on each circle centered at the origin is $0$. The balanced polynomials of degree at most $2009$ form a vector space $V$ over $\mathbb{R}$. Find the dimension of $V$.
 -/
 theorem putnam_2009_b4
-(balanced : MvPolynomial (Fin 2) ℝ → Prop)
-(hbalanced : balanced = fun P ↦ ∀ r > 0, (∫ x in Metric.sphere (0 : EuclideanSpace ℝ (Fin 2)) r, MvPolynomial.eval x P) / (2 * Real.pi * r) = 0)
-(V : Set (MvPolynomial (Fin 2) ℝ)) [AddCommGroup V] [Module ℝ V]
-(hV : ∀ P : MvPolynomial (Fin 2) ℝ, P ∈ V ↔ balanced P ∧ P.totalDegree ≤ 2009)
-: (Module.rank V = putnam_2009_b4_solution) :=
-sorry
+    (IsBalanced : MvPolynomial (Fin 2) ℝ → Prop)
+    (IsBalanced_def : ∀ P, IsBalanced P ↔ ∀ r > 0,
+      (∫ t in (0 : ℝ)..(2 * π), eval ![r * cos t, r * sin t] P) / (2 * π * r) = 0)
+    (V : Submodule ℝ (MvPolynomial (Fin 2) ℝ))
+    (V_def : ∀ P, P ∈ V ↔ IsBalanced P ∧ P.totalDegree ≤ 2009) :
+    Module.rank ℝ V = putnam_2009_b4_solution :=
+  sorry