Network best: theorems proved 3

Claim 13

Status

verified

Claimed

3

Measured

3

Label

network best

Signed commit

1f540c2292a7b2e0167f14df58e0a2fe6b8630b3

Candidate

{"proofs":{"Lemma.am_gm":"import Mathlib.Data.Real.Basic\nimport Mathlib.Algebra.BigOperators.Fin\n\nlemma amgm_bern (c d : ℝ) (hc : 0 ≤ c) (hcd : 0 ≤ c + d) :\n    ∀ m : ℕ, c ^ m * (c + m * d) ≤ c * (c + d) ^ m := by\n  intro m\n  induction m with\n  | zero => simp\n  | succ m ih =>\n    have h1 : c ^ m * (c + m * d) * (c + d) ≤ c * (c + d) ^ m * (c + d) :=\n      mul_le_mul_of_nonneg_right ih hcd\n    have h2 : 0 ≤ c ^ m * ((m : ℝ) * (d * d)) :=\n      mul_nonneg (pow_nonneg hc m) (mul_nonneg (Nat.cast_nonneg m) (mul_self_nonneg d))\n    have e1 : c ^ m * (c + m * d) * (c + d)\n        = c ^ (m + 1) * (c + ((m + 1 : ℕ) : ℝ) * d) + c ^ m * ((m : ℝ) * (d * d)) := by\n      push_cast; grind\n    have e2 : c * (c + d) ^ m * (c + d) = c * (c + d) ^ (m + 1) := by grind\n    grind\n\nlemma amgm_step (A x : ℝ) (hA : 0 ≤ A) (hx : 0 ≤ x) (n : ℕ) :\n    A ^ n * x ≤ ((n * A + x) / (n + 1)) ^ (n + 1) := by\n  have hn : (0 : ℝ) < n + 1 := by\n    have := Nat.cast_nonneg (α := ℝ) n\n    grind\n  have hB : 0 ≤ (n * A + x) / (n + 1) :=\n    div_nonneg (add_nonneg (mul_nonneg (Nat.cast_nonneg n) hA) hx) hn.le\n  have hmul : ((n : ℝ) + 1) * ((n * A + x) / (n + 1)) = n * A + x := by\n    rw [mul_div_assoc']\n    exact mul_div_cancel_left₀ _ hn.ne'\n  rcases hA.lt_or_eq with hA' | hA'\n  · have h := amgm_bern A ((n * A + x) / (n + 1) - A) hA (by grind) (n + 1)\n    have e : A + ((n + 1 : ℕ) : ℝ) * ((n * A + x) / (n + 1) - A) = x := by\n      push_cast; grind\n    rw [e, show A + ((n * A + x) / (n + 1) - A) = (n * A + x) / (n + 1) by grind] at h\n    have : A * (A ^ n * x) ≤ A * ((n * A + x) / (n + 1)) ^ (n + 1) := by\n      calc A * (A ^ n * x) = A ^ (n + 1) * x := by grind\n        _ ≤ _ := h\n    exact le_of_mul_le_mul_left this hA'\n  · subst hA'\n    rcases n with _ | n\n    · simp\n    · simp only [ne_eq, Nat.add_one_ne_zero, not_false_eq_true, zero_pow, zero_mul]\n      exact pow_nonneg hB _\n\nlemma amgm_sum_nonneg : ∀ (n : ℕ) (x : Fin n → ℝ), (∀ i, 0 ≤ x i) → 0 ≤ ∑ i, x i := by\n  intro n\n  induction n with\n  | zero => intro x _; simp\n  | succ n ih =>\n    intro x hx\n    rw [Fin.sum_univ_castSucc]\n    exact add_nonneg (ih _ (fun i => hx _)) (hx _)\n\ntheorem Lemma.am_gm : ∀ (n : ℕ) (x : Fin n → ℝ), (∀ i, 0 ≤ x i) → ∏ i, x i ≤ ((∑ i, x i) / n) ^ n := by\n  intro n\n  induction n with\n  | zero => intro x _; simp\n  | succ n ih =>\n    intro x hx\n    rw [Fin.prod_univ_castSucc, Fin.sum_univ_castSucc]\n    have hS0 : 0 ≤ ∑ i : Fin n, x i.castSucc := amgm_sum_nonneg n _ (fun i => hx _)\n    have hih := ih (fun i => x i.castSucc) (fun i => hx _)\n    have hS00 : n = 0 → ∑ i : Fin n, x i.castSucc = 0 := by rintro rfl; simp\n    generalize ∑ i : Fin n, x i.castSucc = S at hS0 hih hS00 ⊢\n    have hSA : S = n * (S / n) := by\n      rcases Nat.eq_zero_or_pos n with h | h\n      · simp [hS00 h, h]\n      · have : (n : ℝ) ≠ 0 := by exact_mod_cast h.ne'\n        rw [mul_div_assoc']\n        exact (mul_div_cancel_left₀ _ this).symm\n    have hA : 0 ≤ S / n := div_nonneg hS0 (Nat.cast_nonneg n)\n    have key := amgm_step (S / n) (x (Fin.last n)) hA (hx _) n\n    rw [← hSA] at key\n    push_cast\n    calc (∏ i : Fin n, x i.castSucc) * x (Fin.last n)\n        ≤ (S / n) ^ n * x (Fin.last n) := mul_le_mul_of_nonneg_right hih (hx _)\n      _ ≤ _ := key\n","Lemma.fermat_little":"import Mathlib.Data.Nat.Choose.Sum\nimport Mathlib.Data.Nat.Choose.Dvd\n\ntheorem Lemma.fermat_little_key (p a : ℕ) (hp : p.Prime) :\n    ∃ t, (a + 1) ^ p = a ^ p + 1 + p * t := by\n  obtain ⟨m, rfl⟩ : ∃ m, p = m + 1 := ⟨p - 1, by have := hp.two_le; omega⟩\n  rw [add_pow, Finset.sum_range_succ, Finset.sum_range_succ']\n  simp only [Nat.cast_id]\n  have hd : (m + 1) ∣ ∑ k ∈ Finset.range m,\n      a ^ (k + 1) * 1 ^ (m + 1 - (k + 1)) * (m + 1).choose (k + 1) := by\n    apply Finset.dvd_sum\n    intro k hk\n    rw [Finset.mem_range] at hk\n    exact Dvd.dvd.mul_left (hp.dvd_choose_self (by omega) (by omega)) _\n  obtain ⟨t, ht⟩ := hd\n  refine ⟨t, ?_⟩\n  rw [ht]\n  simp only [pow_zero, one_pow, mul_one, one_mul, Nat.choose_zero_right, Nat.choose_self,\n    Nat.sub_self]\n  generalize a ^ (m + 1) = x\n  generalize (m + 1) * t = y\n  omega\n\ntheorem Lemma.fermat_little :\n    ∀ p a : ℕ, p.Prime → a ^ p % p = a % p := by\n  intro p a hp\n  induction a with\n  | zero =>\n    rw [zero_pow hp.ne_zero]\n  | succ n ih =>\n    obtain ⟨t, ht⟩ := Lemma.fermat_little_key p n hp\n    rw [ht, Nat.add_mul_mod_self_left, Nat.add_mod, ih, ← Nat.add_mod]\n","Lemma.two_squares":"import Mathlib.FieldTheory.Finite.Basic\n\ntheorem Lemma.two_squares :\n    ∀ p : ℕ, p.Prime → p % 4 = 1 → ∃ a b : ℕ, a ^ 2 + b ^ 2 = p := by\n  intro p hp h4\n  haveI := Fact.mk hp\n  obtain ⟨x, hx⟩ : IsSquare (-1 : ZMod p) := by\n    have hne : (-1 : ZMod p) ≠ 0 := neg_ne_zero.mpr one_ne_zero\n    have hc : ringChar (ZMod p) ≠ 2 := by\n      rw [ZMod.ringChar_zmod_n]; omega\n    rw [FiniteField.isSquare_iff hc hne, ZMod.card]\n    obtain ⟨t, ht⟩ : ∃ t, p / 2 = 2 * t := ⟨p / 4, by omega⟩\n    rw [ht, pow_mul]; simp\n  obtain ⟨m, hm⟩ : ∃ m, m = Nat.sqrt p := ⟨_, rfl⟩\n  have hm1 : m * m ≤ p := hm ▸ Nat.sqrt_le p\n  have hm2 : p < (m + 1) * (m + 1) := hm ▸ Nat.lt_succ_sqrt p\n  have hmp : m * m ≠ p := by\n    intro h\n    rcases hp.eq_one_or_self_of_dvd m (Dvd.intro m h) with h1 | h1\n    · subst h1; exact hp.one_lt.ne (by omega)\n    · subst h1\n      have := Nat.eq_of_mul_eq_mul_left hp.pos (h.trans (mul_one m).symm)\n      exact hp.one_lt.ne this.symm\n  have hcard : Fintype.card (ZMod p) < Fintype.card (Fin (m + 1) × Fin (m + 1)) := by\n    simp only [ZMod.card, Fintype.card_prod, Fintype.card_fin]; exact hm2\n  obtain ⟨⟨u1, v1⟩, ⟨u2, v2⟩, hne, heq⟩ := Fintype.exists_ne_map_eq_of_card_lt\n    (fun uv : Fin (m + 1) × Fin (m + 1) =>\n      ((uv.1 : ℕ) : ZMod p) + x * ((uv.2 : ℕ) : ZMod p)) hcard\n  simp only at heq\n  have hu1 := u1.isLt\n  have hu2 := u2.isLt\n  have hv1 := v1.isLt\n  have hv2 := v2.isLt\n  obtain ⟨a, ha⟩ : ∃ a : ℤ, a = ((u1 : ℕ) : ℤ) - ((u2 : ℕ) : ℤ) := ⟨_, rfl⟩\n  obtain ⟨b, hb⟩ : ∃ b : ℤ, b = ((v1 : ℕ) : ℤ) - ((v2 : ℕ) : ℤ) := ⟨_, rfl⟩\n  have hdiv : (p : ℤ) ∣ a ^ 2 + b ^ 2 := by\n    rw [← ZMod.intCast_zmod_eq_zero_iff_dvd, ha, hb]\n    push_cast\n    have h' : ((u1 : ℕ) : ZMod p) - ((u2 : ℕ) : ZMod p)\n        = -(x * (((v1 : ℕ) : ZMod p) - ((v2 : ℕ) : ZMod p))) := by\n      linear_combination heq\n    rw [h']\n    linear_combination (-((((v1 : ℕ) : ZMod p) - ((v2 : ℕ) : ZMod p)) ^ 2)) * hx\n  have hpos : 0 < a ^ 2 + b ^ 2 := by\n    by_contra hc\n    have ha0 : a = 0 := by nlinarith [sq_nonneg a, sq_nonneg b]\n    have hb0 : b = 0 := by nlinarith [sq_nonneg a, sq_nonneg b]\n    apply hne\n    have e1 : u1 = u2 := Fin.ext (by omega)\n    have e2 : v1 = v2 := Fin.ext (by omega)\n    rw [e1, e2]\n  have hmZ : (m : ℤ) * m < p := by\n    have := lt_of_le_of_ne hm1 hmp\n    exact_mod_cast this\n  have hsa : a ^ 2 ≤ (m : ℤ) * m := by\n    have h1 : a ≤ m := by omega\n    have h2 : -(m : ℤ) ≤ a := by omega\n    nlinarith\n  have hsb : b ^ 2 ≤ (m : ℤ) * m := by\n    have h1 : b ≤ m := by omega\n    have h2 : -(m : ℤ) ≤ b := by omega\n    nlinarith\n  obtain ⟨k, hk⟩ := hdiv\n  have hpZ : (0 : ℤ) < p := by exact_mod_cast hp.pos\n  have hk1 : k = 1 := by\n    have : 0 < k := by\n      by_contra hc\n      nlinarith\n    have : k < 2 := by\n      by_contra hc\n      nlinarith\n    omega\n  subst hk1\n  refine ⟨a.natAbs, b.natAbs, ?_⟩\n  have : ((a.natAbs ^ 2 + b.natAbs ^ 2 : ℕ) : ℤ) = p := by\n    push_cast\n    rw [sq_abs, sq_abs]\n    linarith\n  exact_mod_cast this\n"}}

Follow-ups

• Prove Lemma.quadratic_reciprocity under its imports (open)