Skip to content
New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

Sign up for GitHub

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Use ⟪x, y⟫_ℝ instead of Matrix.dotProduct #233

Merged
merged 2 commits into from
Oct 22, 2024
Merged

Use ⟪x, y⟫_ℝ instead of Matrix.dotProduct #233

Show file tree
Hide file tree
Changes from 1 commit
Commits
Show all changes
2 commits
Select commit Hold shift + click to select a range
27491bc
Use `⟪x, y⟫_ℝ` instead of `Matrix.dotProduct`
eric-wieser Oct 21, 2024
19d66f1
Merge branch 'main' into dotProduct
eric-wieser Oct 21, 2024
File filter

Filter by extension

Filter by extension
Conversations
Failed to load comments.
Loading
Jump to
Jump to file
Failed to load files.
Loading
Diff view
Diff view
3 changes: 2 additions & 1 deletion lean4/src/putnam_1998_a6.lean
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -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
Expand All @@ -13,6 +14,6 @@ theorem putnam_1998_a6
(hint : ∀ i : Fin 2, ∃ a b c : ℤ, A i = a ∧ B i = b ∧ C i = c)
(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 := fun P Q R ↦ dist Q P = dist Q R ∧ Matrix.dotProduct (P - Q) (R - Q) = 0)
(threesquare : EuclideanSpace ℝ (Fin 2) → EuclideanSpace ℝ (Fin 2) → EuclideanSpace ℝ (Fin 2) → Prop := fun P Q R ↦ dist Q P = dist Q R ∧ ⟪P - Q, R - Q⟫_ℝ = 0)
Copy link
Collaborator

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

Could you clarify why using Matrix.dotProduct is error free? Also, looks like this is also an optParam, must have missed it earlier. Could you modify that?

Copy link
Contributor Author

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

Nice catch, this is indeed an optParam!

Copy link
Contributor Author

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

#236 finds two other stray optParams

Copy link
Contributor Author

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

Could you clarify why using Matrix.dotProduct is error free?

I've expanded the PR description.

: (threesquare A B C ∨ threesquare B C A ∨ threesquare C A B) :=
sorry
7 changes: 4 additions & 3 deletions lean4/src/putnam_2002_a2.lean
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -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
Loading