Fix 1962 A2

This was disprovable because the zero function was excluded from the
solution set. The fix is to replace `a > 0` with `a ≥ 0` in the
solution. Other changes are just style.

There is incidentally a sharper version of this question which requires
establishing which solutions correspond to functions with finite /
infinite domain. However this is not actually asked.

lean4/src/putnam_1962_a2.lean

@@ -1,16 +1,15 @@
 import Mathlib
 open BigOperators
 
-open MeasureTheory
+open MeasureTheory Set
 
 abbrev putnam_1962_a2_solution : Set (ℝ → ℝ) := sorry
--- {f : ℝ → ℝ | ∃ a c : ℝ, a > 0 ∧ f = fun x => a / (1 - c * x)^2}
+-- {f : ℝ → ℝ | ∃ a c : ℝ, a ≥ 0 ∧ f = fun x ↦ a / (1 - c * x) ^ 2}
 theorem putnam_1962_a2
-(hf : ℝ → (ℝ → ℝ) → Prop)
-(hf_def : hf = fun (e : ℝ) (f : ℝ → ℝ) => ∀ x ∈ Set.Ioo 0 e, (⨍ v in Set.Icc 0 x, f v) = Real.sqrt ((f 0) * (f x)))
-(hfinf : (ℝ → ℝ) → Prop)
-(hfinf_def : hfinf = fun (f : ℝ → ℝ) => ∀ x > 0, (⨍ v in Set.Icc 0 x, f v) = Real.sqrt ((f 0) * (f x)))
-: (∀ f : ℝ → ℝ, (hfinf f → ∃ g ∈ putnam_1962_a2_solution, ∀ x ≥ 0, g x = f x) ∧
-∀ e > 0, hf e f → ∃ g ∈ putnam_1962_a2_solution, ∀ x ∈ Set.Ico 0 e, g x = f x) ∧
-∀ f ∈ putnam_1962_a2_solution, hfinf f ∨ (∃ e > 0, hf e f) :=
-sorry
+    (P : Set ℝ → (ℝ → ℝ) → Prop)
+    (P_def : ∀ s f, P s f ↔ ∀ x ∈ s, ⨍ t in Ico 0 x, f t = √(f 0 * f x)) :
+    (∀ f,
+      (P (Ioi 0) f → ∃ g ∈ putnam_1962_a2_solution, EqOn f g (Ici 0)) ∧
+      (∀ e > 0, P (Ioo 0 e) f → ∃ g ∈ putnam_1962_a2_solution, EqOn f g (Ico 0 e))) ∧
+    ∀ f ∈ putnam_1962_a2_solution, P (Ioi 0) f ∨ (∃ e > 0, P (Ioo 0 e) f) :=
+  sorry