Add more random unfinished stuff

Changes

2 changed files (+112/-0)

• ac.lean (new)
  • @@ -0,0 +1,31 @@
    + -- https://b-mehta.github.io/formalising-mathematics-notes/Part_1/the_axiom_of_choice.html + + import Mathlib + -- import Mathlib.Analysis.Complex.Polynomial -- import proof of fundamental theorem of algebra + + open Polynomial -- so I can use notation ℂ[X] for polynomial rings + -- and so I can write `X` and not `polynomial.X` + + suppress_compilation -- because everything is noncomputable + + def f : ℂ[X] := X^5 + X + 37 -- a random polynomial + + lemma f_degree : degree f = 5 := by + unfold f + compute_degree -- polynomial degree computing tactic + norm_num + trivial + + theorem f_has_a_root : ∃ (z : ℂ), f.IsRoot z := by + apply Complex.exists_root -- the fundamental theorem of algebra + -- ⊢ 0 < degree f + rw [f_degree] + -- ⊢ 0 < 5 + norm_num + + -- let z be a root of f (getting data from a theorem) + def z : ℂ := Classical.choose f_has_a_root + + -- proof that z is a root of f (the "API" for `Classical.choose`) + theorem z_is_a_root_of_f : f.IsRoot z := by + exact Classical.choose_spec f_has_a_root
• sum.lean (new)
  • @@ -0,0 +1,81 @@
    + import Mathlib + open Finset BigOperators + + -- OK let's do some warm-up + example (b : ℝ) (h : b ≥ 2) : 1 / ((b - 1) * b) = 1 / (b - 1) - 1 / b := by + have h₁ : b - 1 ≠ 0 := by linarith + field_simp + + -- More easy stuff + example (n : ℕ) : (∑ k ∈ Finset.range n, (2 * k + 1)) = n ^ 2 := by + induction n with + | zero => trivial + | succ n ih => + -- have blah (k : ℕ) : 2 * k + 1 = 2 * (k + 1) - 1 := by sorry + -- rw [blah] + rw [sum_range_succ, ih] + ring + + -- example (n : ℕ) : (∑ k ∈ Finset.range n, (2 * k + 1)) = (∑ k ∈ Finset.range n, (2 * k + 1)) := by + + def converges_to (s : ℕ → ℝ) (a : ℝ) := + ∀ ε > 0, ∃ N, ∀ n ≥ N, |s n - a| < ε + + -- Important: b should be in ℝ so that it's real div not nat div + -- This was so excruciating wow + lemma geom_sum (b : ℝ) (N : ℕ) (h₁ : N ≥ 2) (h₂ : b ≥ 2) : ∑ a ∈ Ico 2 N, 1 / (b ^ a) = 1 / (b - 1) - 1 / b - 1 / (b ^ (N - 1) * (b - 1)) := + calc + ∑ a ∈ Ico 2 N, 1 / (b ^ a) = ∑ a ∈ Ico 2 N, (1 / b) ^ a := by simp + _ = ((1 / b) ^ 2 - (1 / b) ^ N) / (1 - (1 / b)) := by + rw [geom_sum_Ico'] + by_contra h + simp at h + linarith + exact h₁ + _ = 1 / (b - 1) - 1 / b - b / (b ^ N * (b - 1)) := by + have h₃ : b - 1 ≠ 0 := by linarith + field_simp + ring + _ = 1 / (b - 1) - 1 / b - 1 / (b ^ (N - 1) * (b - 1)) := by + have h₃ : b ≠ 0 := by linarith + have h₄ : b ^ N * (b - 1) = b * (b ^ (N - 1) * (b - 1)) := by + rw [← mul_assoc, ← pow_succ' b (N - 1), Nat.sub_one_add_one] + linarith + simp [h₄, div_mul_cancel_left₀ h₃] + + lemma double_sum : converges_to (fun N : ℕ => ∑ a ∈ Ico 2 N, ∑ b ∈ Ico 2 N, 1 / (b ^ a)) 1 := by + intro ε εpos + use max (Nat.floor (1 / ε)) 2 + intro n nlarge + simp + have h₁ : n ≥ 2 := by + exact le_of_max_le_right nlarge + have h₂ (b : ℕ) (N : ℕ) (h₁ : N ≥ 2) (h₂ : b ∈ Ico 2 N) : ∑ a ∈ Ico 2 N, (1 : ℝ) / (b ^ a) = (1 : ℝ) / (b - 1) - (1 : ℝ) / b - (1 : ℝ) / (b ^ (N - 1) * (b - 1)) := by + have h₃ : (b : ℝ) ≥ 2 := by + have h₄ : b ≥ 2 := List.left_le_of_mem_range' h₂ + exact Nat.ofNat_le_cast.mpr h₄ + exact geom_sum ↑b N h₁ h₃ + have h₃ : ∑ a ∈ Ico 2 n, ∑ b ∈ Ico 2 n, (1 : ℝ) / (b ^ a) = 1 - (1 : ℝ) / (n - 1) - ∑ b ∈ Ico 2 n, (1 : ℝ) / (b ^ (n - 1) * (b - 1)) := by + calc + ∑ a ∈ Ico 2 n, ∑ b ∈ Ico 2 n, (1 : ℝ) / (b ^ a) = ∑ b ∈ Ico 2 n, ∑ a ∈ Ico 2 n, (1 : ℝ) / (b ^ a) := sum_comm + _ = ∑ b ∈ Ico 2 n, (1 / (b - 1) - 1 / b - 1 / (b ^ (n - 1) * (b - 1))) := by + rw [h₂ _ n h₁] + + + _ = 1 - (1 : ℝ) / (n - 1) - ∑ b ∈ Ico 2 n, (1 : ℝ) / (b ^ (n - 1) * (b - 1)) := by + induction n with + | zero => trivial + | succ n ih => + cases h₁ + field_simp + rename_i h₃ + push_cast + push_cast at ih + rw [sum_Ico_succ_top, ih _ h₃] + + + -- rw [h₂] + + + -- then telescope the sums and bound the other sum + -- qed