Merge pull request #233 from eric-wieser/dotProduct

Use `⟪x, y⟫_ℝ` instead of `Matrix.dotProduct`
trishullab · Oct 22, 2024 · 380dfe6 · 380dfe6
2 parents 06dc7cb + 19d66f1
commit 380dfe6
Show file tree

Hide file tree

Showing 2 changed files with 6 additions and 4 deletions.
diff --git a/lean4/src/putnam_1998_a6.lean b/lean4/src/putnam_1998_a6.lean
@@ -2,6 +2,7 @@ import Mathlib
 open BigOperators
 
 open Set Function Metric
+open scoped InnerProductSpace
 
 /--
 Let $A, B, C$ denote distinct points with integer coordinates in $\mathbb R^2$. Prove that if
@@ -14,6 +15,6 @@ theorem putnam_1998_a6
 (htriangle : A ≠ B ∧ A ≠ C ∧ B ≠ C)
 (harea : (dist A B + dist B C) ^ 2 < 8 * (MeasureTheory.volume (convexHull ℝ {A, B, C})).toReal + 1)
 (threesquare : (EuclideanSpace ℝ (Fin 2)) → (EuclideanSpace ℝ (Fin 2)) → (EuclideanSpace ℝ (Fin 2)) → Prop)
-(threesquare_def : threesquare = fun P Q R ↦ dist Q P = dist Q R ∧ Matrix.dotProduct (P - Q) (R - Q) = 0)
+(threesquare_def : threesquare = fun P Q R ↦ dist Q P = dist Q R ∧ ⟪P - Q, R - Q⟫_ℝ = 0)
 : (threesquare A B C ∨ threesquare B C A ∨ threesquare C A B) :=
 sorry
diff --git a/lean4/src/putnam_2002_a2.lean b/lean4/src/putnam_2002_a2.lean
@@ -2,14 +2,15 @@ import Mathlib
 open BigOperators
 
 open Nat Metric
+open scoped InnerProductSpace
 
 /--
 Given any five points on a sphere, show that some four of them must lie on a closed hemisphere.
 -/
 theorem putnam_2002_a2
 (unit_sphere : Set (EuclideanSpace ℝ (Fin 3)))
 (hsphere : unit_sphere = sphere 0 1)
-(hemi : (EuclideanSpace ℝ (Fin 3)) → Set (EuclideanSpace ℝ (Fin 3)))
-(hhemi : hemi = fun V ↦ {P : EuclideanSpace ℝ (Fin 3) | Matrix.dotProduct P V ≥ 0})
-: (∀ (S : Set (EuclideanSpace ℝ (Fin 3))), S ⊆ unit_sphere ∧ S.encard = 5 → ∃ V : (EuclideanSpace ℝ (Fin 3)), V ≠ 0 ∧ (S ∩ hemi V).encard ≥ 4) :=
+(hemi : EuclideanSpace ℝ (Fin 3) → Set (EuclideanSpace ℝ (Fin 3)))
+(hhemi : hemi = fun V ↦ {P : EuclideanSpace ℝ (Fin 3) | ⟪P, V⟫_ℝ ≥ 0})
+: (∀ (S : Set (EuclideanSpace ℝ (Fin 3))), S ⊆ unit_sphere ∧ S.encard = 5 → ∃ V : EuclideanSpace ℝ (Fin 3), V ≠ 0 ∧ (S ∩ hemi V).encard ≥ 4) :=
 sorry