Classic theorems without their usual tools: every challenge is settled

Claim 115

Status

verified

Claimed

7

Measured

7

Label

no improvement

Signed commit

25abb822d7319ebd2381f3c4c9e9aa2cff537916

Verification runs

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.bertrand":"import Mathlib.NumberTheory.Primorial\nimport Mathlib.Data.Nat.Choose.Central\nimport Mathlib.Data.Nat.Choose.Factorization\n\nopen Nat\n\ntheorem bert_mid_le (k : ℕ) :\n    (∏ i ∈ Finset.Ico (k+1+1) (2*k+1+1), if i.Prime then i else 1) ≤ 4 ^ k := by\n  rw [← Finset.prod_filter]\n  have hd : (∏ p ∈ Finset.filter Nat.Prime (Finset.Ico (k+1+1) (2*k+1+1)), p) ∣\n      choose (k+1+k) (k+1) := by\n    apply Finset.prod_primes_dvd\n    · intro a ha; exact (Finset.mem_filter.1 ha).2.prime\n    · intro a ha\n      obtain ⟨h1, h2⟩ := Finset.mem_filter.1 ha\n      rw [Finset.mem_Ico] at h1\n      exact h2.dvd_choose_add (by omega) (by omega) (by omega)\n  have hc : choose (k+1+k) (k+1) = choose (2*k+1) k := by\n    rw [show k+1+k = 2*k+1 by omega]\n    exact Nat.choose_symm_of_eq_add (by omega)\n  rw [hc] at hd\n  exact (Nat.le_of_dvd (Nat.choose_pos (by omega)) hd).trans (Nat.choose_middle_le_pow k)\n\ntheorem bert_Q_le (n : ℕ) :\n    (∏ i ∈ Finset.range (n+1), if i.Prime then i else 1) ≤ 4 ^ n := by\n  induction n using Nat.strong_induction_on with\n  | _ n ih =>\n  rcases Nat.even_or_odd' n with ⟨k, rfl | rfl⟩\n  · rcases Nat.lt_or_ge k 2 with hk | hk\n    · interval_cases k <;> decide\n    · obtain ⟨j, hj⟩ : ∃ j, 2 * k = j + 1 := ⟨2 * k - 1, by omega⟩\n      rw [hj, Finset.prod_range_succ, if_neg, Nat.mul_one]\n      · exact (ih j (by omega)).trans (Nat.pow_le_pow_right (by omega) (by omega))\n      · rw [← hj]; intro hp\n        rcases hp.eq_one_or_self_of_dvd 2 (Nat.dvd_mul_right 2 k) with h | h <;> omega\n  · rcases Nat.lt_or_ge k 1 with hk | hk\n    · interval_cases k; decide\n    · rw [← Finset.prod_range_mul_prod_Ico _ (show k+1+1 ≤ 2*k+1+1 by omega)]\n      calc _ ≤ 4 ^ (k+1) * 4 ^ k := Nat.mul_le_mul (ih (k+1) (by omega)) (bert_mid_le k)\n        _ = 4 ^ (2*k+1) := by rw [← Nat.pow_add]; congr 1; omega\n\ntheorem bert_primorial_le (n : ℕ) :\n    ∏ p ∈ Finset.filter Nat.Prime (Finset.range (n+1)), p ≤ 4 ^ n := by\n  rw [Finset.prod_filter]; exact bert_Q_le n\n\ntheorem bert_factorization_small (n : ℕ) (n_large : 2 < n)\n    (no_prime : ¬∃ p : ℕ, p.Prime ∧ n < p ∧ p ≤ 2 * n) :\n    centralBinom n = ∏ p ∈ Finset.range (2 * n / 3 + 1), p ^ (centralBinom n).factorization p := by\n  refine (Eq.trans ?_ n.prod_pow_factorization_centralBinom).symm\n  apply Finset.prod_subset\n  · exact Finset.range_subset_range.2 (Nat.add_le_add_right (Nat.div_le_self _ _) _)\n  intro x hx h2x\n  rw [Finset.mem_range, Nat.lt_succ_iff] at hx h2x\n  have h3 : 2 * n < 3 * x := by omega\n  by_cases hp : x.Prime\n  · have : x ≤ n := by\n      by_contra h\n      exact no_prime ⟨x, hp, by omega, hx⟩\n    rw [factorization_centralBinom_of_two_mul_self_lt_three_mul n_large this h3, Nat.pow_zero]\n  · rw [Nat.factorization_eq_zero_of_not_prime _ hp, Nat.pow_zero]\n\ntheorem bert_centralBinom_le (n : ℕ) (n_large : 2 < n)\n    (no_prime : ¬∃ p : ℕ, Nat.Prime p ∧ n < p ∧ p ≤ 2 * n) :\n    centralBinom n ≤ (2 * n) ^ sqrt (2 * n) * 4 ^ (2 * n / 3) := by\n  have n_pos : 0 < n := (Nat.zero_le _).trans_lt n_large\n  have n2_pos : 1 ≤ 2 * n := by omega\n  let S := {p ∈ Finset.range (2 * n / 3 + 1) | Nat.Prime p}\n  let f x := x ^ n.centralBinom.factorization x\n  have : ∏ x ∈ S, f x = ∏ x ∈ Finset.range (2 * n / 3 + 1), f x := by\n    refine Finset.prod_filter_of_ne fun p _ h => ?_\n    contrapose! h; dsimp only [f]\n    rw [Nat.factorization_eq_zero_of_not_prime n.centralBinom h, _root_.pow_zero]\n  rw [bert_factorization_small n n_large no_prime, ← this, ←\n    Finset.prod_filter_mul_prod_filter_not S fun p => p ^ 2 ≤ 2 * n]\n  apply Nat.mul_le_mul\n  · refine (Finset.prod_le_prod' fun p _ => (?_ : f p ≤ 2 * n)).trans ?_\n    · exact pow_factorization_choose_le (by omega)\n    have : (Finset.Icc 1 (sqrt (2 * n))).card = sqrt (2 * n) := by\n      rw [Nat.card_Icc, Nat.add_sub_cancel]\n    rw [Finset.prod_const]\n    refine pow_right_mono₀ n2_pos ((Finset.card_le_card fun x hx => ?_).trans this.le)\n    obtain ⟨h1, h2⟩ := Finset.mem_filter.1 hx\n    exact Finset.mem_Icc.mpr ⟨(Finset.mem_filter.1 h1).2.one_lt.le, Nat.le_sqrt'.mpr h2⟩\n  · refine le_trans ?_ (bert_primorial_le (2 * n / 3))\n    refine (Finset.prod_le_prod' fun p hp => (?_ : f p ≤ p)).trans ?_\n    · obtain ⟨h1, h2⟩ := Finset.mem_filter.1 hp\n      refine (pow_right_mono₀ (Finset.mem_filter.1 h1).2.one_lt.le ?_).trans (pow_one p).le\n      exact Nat.factorization_choose_le_one (not_le.1 h2)\n    refine Finse
… (truncated; the full value is in this page's JSON)