From 4b5b2f5245c422f54b5894bc4df62fb2373052cc Mon Sep 17 00:00:00 2001
From: George Tsoukalas <george.tsoukalas@utexas.edu>
Date: Wed, 24 Jul 2024 16:09:49 +0000
Subject: [PATCH] Fixed (lean) volume on 3D triangle.

---
 lean4/src/putnam_2013_a5.lean | 6 +++---
 1 file changed, 3 insertions(+), 3 deletions(-)

diff --git a/lean4/src/putnam_2013_a5.lean b/lean4/src/putnam_2013_a5.lean
index 8b481331..e4f83fdb 100644
--- a/lean4/src/putnam_2013_a5.lean
+++ b/lean4/src/putnam_2013_a5.lean
@@ -1,7 +1,7 @@
 import Mathlib
 open BigOperators
 
-open Function Set
+open Function Set MeasureTheory
 
 -- Note: uses (Fin m → Fin m → Fin m → ℝ) instead of ensuring inputs are strictly increasing
 theorem putnam_2013_a5
@@ -11,8 +11,8 @@ theorem putnam_2013_a5
 (areadef2 : (Fin m → Fin m → Fin m → ℝ) → Prop)
 (areadef3 : (Fin m → Fin m → Fin m → ℝ) → Prop)
 (mge3 : m ≥ 3)
-(harea2 : ∀ a b c : Fin 2 → ℝ, area2 a b c = (MeasureTheory.volume (convexHull ℝ {a, b, c})).toReal)
-(harea3 : ∀ a b c : Fin 3 → ℝ, area3 a b c = (MeasureTheory.volume (convexHull ℝ {a, b, c})).toReal)
+(harea2 : ∀ a b c : Fin 2 → ℝ, area2 a b c = (volume (convexHull ℝ {a, b, c})).toReal)
+(harea3 : ∀ a b c : Fin 3 → ℝ, area3 a b c = (μH[2] (convexHull ℝ {a, b, c})).toReal)
 (hareadef2 : ∀ a : Fin m → Fin m → Fin m → ℝ, 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 : Fin m → Fin m → Fin m → ℝ, 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)
 : ∀ a : Fin m → Fin m → Fin m → ℝ, areadef2 a → areadef3 a :=