From f5290ac9972e0c5cf48c6d2ef0c0a08a3c460fba Mon Sep 17 00:00:00 2001 From: Oliver Nash Date: Thu, 24 Oct 2024 16:02:43 +0000 Subject: [PATCH] Fix 1963 A3 (again) MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit This was disprovable because `y` could fail to be differentiable at `1`. E.g., one could define `y` such that: `y x = ∫ t in (1 : ℝ)..x, putnam_1963_a3_solution f n x t` for `x ≥ 1` and `y x = 0` for `x < 1`. This will satisfy the RHS of the iff in the goal but not the left. I see two obvious ways to resolve the issue: 1. Demand that `y` is C^n on `[1, ∞)` 2. Require that `y x = ∫ t in (1 : ℝ)..x, putnam_1963_a3_solution f n x t` holds on a neighbourhood of `[1, ∞)` The informal statement is very vague so I have somewhat arbitrarily opted for the first of these resolutions. This was previously "fixed" in 7a9215271b97b0d3a87f747c3828fea29e0d9ef7 but unfortunately an error remained. --- lean4/src/putnam_1963_a3.lean | 5 +++-- 1 file changed, 3 insertions(+), 2 deletions(-) diff --git a/lean4/src/putnam_1963_a3.lean b/lean4/src/putnam_1963_a3.lean index 07471de0..a16ea888 100644 --- a/lean4/src/putnam_1963_a3.lean +++ b/lean4/src/putnam_1963_a3.lean @@ -13,7 +13,8 @@ theorem putnam_1963_a3 (n : ℕ) (hn : 0 < n) (f y : ℝ → ℝ) - (hf : ContinuousOn f (Ici 1)) : - ContDiffOn ℝ n y (Ici 1) ∧ (∀ i < n, deriv^[i] y 1 = 0) ∧ (Ici 1).EqOn (P n y) f ↔ + (hf : ContinuousOn f (Ici 1)) + (hy : ContDiffOn ℝ n y (Ici 1)) : + (∀ i < n, deriv^[i] y 1 = 0) ∧ (Ici 1).EqOn (P n y) f ↔ ∀ x ≥ 1, y x = ∫ t in (1 : ℝ)..x, putnam_1963_a3_solution f n x t := sorry