Zulip Chat Archive

Stream: new members

Topic: prime sum of two squares one sentence proof


view this post on Zulip Moritz Firsching (Jan 18 2021 at 20:51):

I can now fill in all the sorry in the above and also finished proving the following statements that will come handy later:

lemma z_at_least_one_fix (p:) (k: )
(hp : p.prime)
(h₁ : 0 < (1:))
(hk: 0 < k)
(h4: 1 * 1 + 4 * 1* k = p):
zagier_involution p hp (⟨(1, 1, k), h₁, h₁, hk, h4 : S p) =  ⟨(1, 1, k), h₁, h₁, hk, h4 := sorry


lemma z_at_most_one_fix (p: ) (x y z k: )
(hp: p.prime)
(hx: 0 < x)
(hy: 0 < y)
(hz: 0 < z)
(h4: x * x + 4 * y * z = p)
(h₁ : 0 < (1:))
(hk: 0 < k)
(h4fix: 1 * 1 + 4 * 1 * k = p)
(hfix: zagier_involution p hp (⟨(x, y, z), hx, hy, hz, h4 : S p) =
(⟨(x, y, z), hx, hy, hz, h4 : S p)):
(⟨(x, y, z), hx, hy, hz, h4 : S p) = (⟨(1, 1, k), h₁ , h₁, hk, h4fix : S p) := sorry


lemma z_involution (p:) (k x y z: )
(hp : p.prime)
(hx : 0 < x)
(hy : 0 < y)
(hz : 0 < z)
(h4: x * x + 4 * y * z = p)
: zagier_involution p hp (zagier_involution p hp ⟨(x, y, z), hx, hy, hz, h4⟩)  =
  ⟨(x, y, z), hx, hy, hz, h4
   := sorry

All the proofs are still very messy, but no at least there's no sorry left.

Next I plan to check out how finite sets in lean work and try to prove something similar to

-- The cardinatlies of a finite set S and its fixpoint set under an involution have equal parity.
lemma fix_equal_parity {α : Type*} {S: set α}
 (hf: finite S  )(f: α   α )
 (hff: finite {x  S | f x = x})
(hs:  x: α, S x  (S (f x)  f (f x) = x )):
odd (finite.to_finset hf).card 
odd (finite.to_finset (hff: finite {x  S | f x = x})).card := sorry

Is this a good path?

view this post on Zulip Bryan Gin-ge Chen (Jan 18 2021 at 20:54):

(I guess this is a continuation of this thread.)

view this post on Zulip Moritz Firsching (Jan 18 2021 at 21:08):

Bryan Gin-ge Chen said:

(I guess this is a continuation of this thread.)

Yes, I renamed it and now it should all be in one thread (hopefully..)


Last updated: May 12 2021 at 23:13 UTC