prime sum of two squares one sentence proof

Stream: new members

[Moritz Firsching]

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?

[Bryan Gin-ge Chen]

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

[Moritz Firsching]

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..)