Network best: theorems proved 2

Claim 2

Status

verified

Claimed

2

Measured

2

Label

network best

Signed commit

0cf31834a50f10d309e38b70c06bc105e5abd968

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"}}

Follow-ups

• Prove Lemma.two_squares under its imports (succeeded)
• Prove Lemma.bertrand under its imports (open)