From a65cf48fb109bbf6b9112404a2a307180c5a3def Mon Sep 17 00:00:00 2001 From: Ivan Smirnov Date: Tue, 25 Aug 2026 19:25:05 +0200 Subject: [PATCH] putnam_2013_a5: use EuclideanSpace so area3 measures Euclidean area MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit On `Fin 3 → ℝ` Mathlib's instance norm is the sup norm, so the `μH[2]` in `harea3` is the Hausdorff area of the l-infinity metric, whose ratio to Euclidean area varies with the plane's orientation — while `harea2`'s `volume` on `Fin 2 → ℝ` is genuine Lebesgue area, so the two sides of the theorem measure different geometries. This commit changes only the ambient types to `EuclideanSpace ℝ (Fin n)`; `harea2`, `harea3` and the conclusion are unchanged. `μH[2]` is unnormalized, so on a 2-plane in `EuclideanSpace ℝ (Fin 3)` it equals (4/π) × Euclidean area — but that is one constant for every plane, and area-definiteness (`∑ aᵢⱼₖ · area ≥ 0` over all configurations) is invariant under uniform positive rescaling of the area functional, so the corrected statement is equivalent to the original problem. --- lean4/src/putnam_2013_a5.lean | 8 ++++---- 1 file changed, 4 insertions(+), 4 deletions(-) diff --git a/lean4/src/putnam_2013_a5.lean b/lean4/src/putnam_2013_a5.lean index c430f9d..23b0125 100644 --- a/lean4/src/putnam_2013_a5.lean +++ b/lean4/src/putnam_2013_a5.lean @@ -8,14 +8,14 @@ For $m \geq 3$, a list of $\binom{m}{3}$ real numbers $a_{ijk}$ ($1 \leq i< j< k -/ theorem putnam_2013_a5 (m : ℕ) -(area2 : (Fin 2 → ℝ) → (Fin 2 → ℝ) → (Fin 2 → ℝ) → ℝ) -(area3 : (Fin 3 → ℝ) → (Fin 3 → ℝ) → (Fin 3 → ℝ) → ℝ) +(area2 : EuclideanSpace ℝ (Fin 2) → EuclideanSpace ℝ (Fin 2) → EuclideanSpace ℝ (Fin 2) → ℝ) +(area3 : EuclideanSpace ℝ (Fin 3) → EuclideanSpace ℝ (Fin 3) → EuclideanSpace ℝ (Fin 3) → ℝ) (areadef2 : (Fin m → Fin m → Fin m → ℝ) → Prop) (areadef3 : (Fin m → Fin m → Fin m → ℝ) → Prop) (mge3 : m ≥ 3) (harea2 : ∀ a b c, area2 a b c = (volume (convexHull ℝ {a, b, c})).toReal) (harea3 : ∀ a b c, area3 a b c = (μH[2] (convexHull ℝ {a, b, c})).toReal) -(hareadef2 : ∀ a, areadef2 a ↔ ∀ A : Fin m → (Fin 2 → ℝ), (∑ i : Fin m, ∑ j : Fin m, ∑ k : Fin m, if (i < j ∧ j < k) then (a i j k * area2 (A i) (A j) (A k)) else 0) ≥ 0) -(hareadef3 : ∀ a, areadef3 a ↔ ∀ A : Fin m → (Fin 3 → ℝ), (∑ i : Fin m, ∑ j : Fin m, ∑ k : Fin m, if (i < j ∧ j < k) then (a i j k * area3 (A i) (A j) (A k)) else 0) ≥ 0) +(hareadef2 : ∀ a, areadef2 a ↔ ∀ A : Fin m → EuclideanSpace ℝ (Fin 2), (∑ i : Fin m, ∑ j : Fin m, ∑ k : Fin m, if (i < j ∧ j < k) then (a i j k * area2 (A i) (A j) (A k)) else 0) ≥ 0) +(hareadef3 : ∀ a, areadef3 a ↔ ∀ A : Fin m → EuclideanSpace ℝ (Fin 3), (∑ i : Fin m, ∑ j : Fin m, ∑ k : Fin m, if (i < j ∧ j < k) then (a i j k * area3 (A i) (A j) (A k)) else 0) ≥ 0) : ∀ a, areadef2 a → areadef3 a := sorry