diff --git a/FormalBook/Ch20/CauchyAMGM.lean b/FormalBook/Ch20/CauchyAMGM.lean index 2cf8e09..983e97c 100644 --- a/FormalBook/Ch20/CauchyAMGM.lean +++ b/FormalBook/Ch20/CauchyAMGM.lean @@ -92,7 +92,7 @@ lemma cauchy_amgm_backward_iter (d n : ℕ) (hn : 0 < n) (h : CauchyAMGM (n + d) | zero => exact h | succ d ihd => apply ihd - exact cauchy_amgm_backward (n + d) (by omega) (by convert h using 1) + exact cauchy_amgm_backward (n + d) (by omega) (by rw [add_assoc]; exact h) /-- **Cauchy's AM-GM inequality**: for n ≥ 1 and nonneg reals, ∏aᵢ ≤ (∑aᵢ/n)ⁿ. Proved by forward doubling P(2)→P(4)→...→P(2^k), then backward P(2^k)→...→P(n). -/ diff --git a/FormalBook/Ch20/ErdosGallai.lean b/FormalBook/Ch20/ErdosGallai.lean index 36417b6..2d6deb2 100644 --- a/FormalBook/Ch20/ErdosGallai.lean +++ b/FormalBook/Ch20/ErdosGallai.lean @@ -26,9 +26,11 @@ theorem hm_le_gm (a b : ℝ) (ha : 0 < a) (hb : 0 < b) : rw [div_le_iff₀ hab] have hsqa := Real.mul_self_sqrt ha.le have hsqb := Real.mul_self_sqrt hb.le - have hsqab : Real.sqrt (a * b) * Real.sqrt (a * b) = a * b := Real.mul_self_sqrt (mul_nonneg ha.le hb.le) + have hsqab : Real.sqrt (a * b) * Real.sqrt (a * b) = a * b := + Real.mul_self_sqrt (mul_nonneg ha.le hb.le) have hsqab' : Real.sqrt a * Real.sqrt b = Real.sqrt (a * b) := (Real.sqrt_mul ha.le b).symm - nlinarith [sq_nonneg (Real.sqrt a - Real.sqrt b), Real.sqrt_nonneg a, Real.sqrt_nonneg b, Real.sqrt_nonneg (a * b)] + nlinarith [sq_nonneg (Real.sqrt a - Real.sqrt b), Real.sqrt_nonneg a, Real.sqrt_nonneg b, + Real.sqrt_nonneg (a * b)] /-- Product identity: ∏ᵢ (αᵢ - 1) · ∏ᵢ (αᵢ + 1) = ∏ᵢ (αᵢ² - 1). -/ @@ -43,15 +45,18 @@ theorem prod_sub_one_mul_prod_add_one {n : ℕ} (α : Fin n → ℝ) : /-- f'(1) for our polynomial, up to sign: f'(1) = -2 · ∏ᵢ(αᵢ - 1) · ∏ⱼ(βⱼ + 1). -/ +@[nolint defsWithUnderscore] noncomputable def erdos_gallai_deriv_at_one {m n : ℕ} (α : Fin m → ℝ) (β : Fin n → ℝ) : ℝ := -2 * (∏ i, (α i - 1)) * (∏ j, (β j + 1)) /-- f'(-1) for our polynomial: f'(-1) = 2 · ∏ᵢ(αᵢ + 1) · ∏ⱼ(βⱼ - 1). -/ +@[nolint defsWithUnderscore] noncomputable def erdos_gallai_deriv_at_neg_one {m n : ℕ} (α : Fin m → ℝ) (β : Fin n → ℝ) : ℝ := 2 * (∏ i, (α i + 1)) * (∏ j, (β j - 1)) /-- C² = ∏ᵢ(αᵢ² - 1) · ∏ⱼ(βⱼ² - 1). -/ +@[nolint defsWithUnderscore] noncomputable def erdos_gallai_C_sq {m n : ℕ} (α : Fin m → ℝ) (β : Fin n → ℝ) : ℝ := (∏ i, (α i ^ 2 - 1)) * (∏ j, (β j ^ 2 - 1)) @@ -69,6 +74,7 @@ theorem erdos_gallai_deriv_product {m n : ℕ} (α : Fin m → ℝ) (β : Fin n When f'(1) < 0 and f'(-1) > 0 (normal case), this equals 2·|f'(1)|·|f'(-1)| / (|f'(1)| + |f'(-1)|), the harmonic mean. -/ +@[nolint defsWithUnderscore] noncomputable def erdos_gallai_T {m n : ℕ} (α : Fin m → ℝ) (β : Fin n → ℝ) : ℝ := -2 * (erdos_gallai_deriv_at_one α β) * (erdos_gallai_deriv_at_neg_one α β) / (erdos_gallai_deriv_at_one α β - erdos_gallai_deriv_at_neg_one α β) @@ -78,10 +84,12 @@ noncomputable def erdos_gallai_T {m n : ℕ} (α : Fin m → ℝ) (β : Fin n open MeasureTheory intervalIntegral /-- f(x) = (1 - x²) · ∏ᵢ (αᵢ - x) · ∏ⱼ (βⱼ + x). -/ +@[nolint defsWithUnderscore] noncomputable def erdos_gallai_f {m n : ℕ} (α : Fin m → ℝ) (β : Fin n → ℝ) (x : ℝ) : ℝ := (1 - x ^ 2) * (∏ i, (α i - x)) * (∏ j, (β j + x)) /-- The area A = ∫₋₁¹ f(x) dx. -/ +@[nolint defsWithUnderscore] noncomputable def erdos_gallai_area {m n : ℕ} (α : Fin m → ℝ) (β : Fin n → ℝ) : ℝ := ∫ x in (-1 : ℝ)..1, erdos_gallai_f α β x @@ -92,9 +100,9 @@ theorem erdos_gallai_f_continuous {m n : ℕ} (α : Fin m → ℝ) (β : Fin n apply Continuous.mul · apply Continuous.mul · exact continuous_const.sub (continuous_pow 2) - · exact continuous_finset_prod _ fun i _ => + · exact continuous_finsetProd _ fun i _ => continuous_const.sub continuous_id - · exact continuous_finset_prod _ fun j _ => + · exact continuous_finsetProd _ fun j _ => continuous_const.add continuous_id /-- f is interval-integrable on [-1, 1]. -/ @@ -199,10 +207,10 @@ theorem integral_one_sub_sq : ∫ x in (-1:ℝ)..1, (1 - x ^ 2) = 4 / 3 := by intro x _ have h1 := hasDerivAt_id (𝕜 := ℝ) x have h3 : HasDerivAt (fun x => x ^ 3 / 3) (x ^ 2) x := by - have := (hasDerivAt_pow 3 x).div_const (3 : ℝ) - convert this using 1 - push_cast; ring - convert h1.sub h3 using 1 + have h := (hasDerivAt_pow 3 x).div_const (3 : ℝ) + have h_eq : ((3 : ℕ) : ℝ) * x ^ (3 - 1) / 3 = x ^ 2 := by ring + rwa [h_eq] at h + convert h1.sub h3 using 1 <;> rfl have hint : IntervalIntegrable (fun x => (1:ℝ) - x ^ 2) volume (-1) 1 := (continuous_const.sub (continuous_pow 2)).intervalIntegrable _ _ rw [integral_eq_sub_of_hasDerivAt hderiv hint] diff --git a/FormalBook/Ch28/BrouwerCovering.lean b/FormalBook/Ch28/BrouwerCovering.lean index 45a8208..4930e1b 100644 --- a/FormalBook/Ch28/BrouwerCovering.lean +++ b/FormalBook/Ch28/BrouwerCovering.lean @@ -27,7 +27,7 @@ private def acCov : IsCoveringMap (QuotientAddGroup.mk : ℝ → AddCircle (1 : private theorem acLoop_lift_eq : (⟨fun t => (t : ℝ), continuous_subtype_val⟩ : C(I, ℝ)) = acCov.liftPath acLoop.toContinuousMap 0 rfl := by - rw [IsCoveringMap.eq_liftPath_iff'] + rw [acCov.eq_liftPath_iff' rfl] exact ⟨by ext; simp [acLoop], by simp⟩ private theorem not_sc_addCircle : ¬ SimplyConnectedSpace (AddCircle (1 : ℝ)) := by @@ -39,7 +39,7 @@ private theorem not_sc_addCircle : ¬ SimplyConnectedSpace (AddCircle (1 : ℝ)) have h2 : (acCov.liftPath (Path.refl acBase).toContinuousMap 0 rfl) 1 = (0 : ℝ) := by have : (ContinuousMap.const I (0 : ℝ)) = acCov.liftPath (Path.refl acBase).toContinuousMap 0 rfl := by - rw [IsCoveringMap.eq_liftPath_iff'] + rw [acCov.eq_liftPath_iff' rfl] exact ⟨by ext; simp only [ContinuousMap.const_zero, ContinuousMap.coe_zero, Function.comp_apply, Pi.zero_apply, QuotientAddGroup.mk_zero, Path.coe_toContinuousMap, Path.refl_apply], by simp only [ContinuousMap.const_zero, ContinuousMap.zero_apply]⟩ diff --git a/FormalBook/Ch28/SpernerBrouwer.lean b/FormalBook/Ch28/SpernerBrouwer.lean index cfb016d..aed6553 100644 --- a/FormalBook/Ch28/SpernerBrouwer.lean +++ b/FormalBook/Ch28/SpernerBrouwer.lean @@ -139,7 +139,7 @@ private theorem stdSimplex2_eq : stdSimplex2 = stdSimplex ℝ (Fin 3) := by /-- The standard 2-simplex is compact. -/ private theorem stdSimplex2_isCompact : IsCompact stdSimplex2 := by - rw [stdSimplex2_eq]; exact isCompact_stdSimplex _ + rw [stdSimplex2_eq]; exact isCompact_stdSimplex ℝ (Fin 3) /-- The Sperner coloring is well-defined: if v ∈ Δ² and f(v) ≠ v with f(v) ∈ Δ², then some coordinate strictly decreases. -/ @@ -200,6 +200,7 @@ private instance subdivVertDecEq (k : ℕ) : DecidableEq (SubdivVert k) := inferInstanceAs (DecidableEq { abc : Fin 3 → ℕ // ∑ i, abc i = k }) /-- The coordinate map: send a subdivision vertex to its barycentric point in Δ². -/ +@[nolint unusedArguments] private noncomputable def subdivCoord (k : ℕ) (hk : 0 < k) (v : SubdivVert k) : Fin 3 → ℝ := fun i => (v.1 i : ℝ) / (k : ℝ) @@ -207,7 +208,7 @@ private theorem subdivCoord_mem (k : ℕ) (hk : 0 < k) (v : SubdivVert k) : subdivCoord k hk v ∈ stdSimplex2 := by constructor · intro i; apply div_nonneg (Nat.cast_nonneg _) (Nat.cast_nonneg _) - · simp only [subdivCoord, div_add_div_same, ← Finset.sum_div] + · simp only [subdivCoord, ← Finset.sum_div] rw [show (∑ i : Fin 3, (v.1 i : ℝ)) = (∑ i : Fin 3, v.1 i : ℕ) from by push_cast; rfl] rw [v.2]; field_simp @@ -430,6 +431,7 @@ private lemma odd_transitions (n : ℕ) (s : Fin (n + 1) → Bool) rw [h0, hlast] at h simpa using h +@[nolint unusedArguments] private theorem subdivSperner_odd_sum (f : (Fin 3 → ℝ) → (Fin 3 → ℝ)) (hfS : ∀ x ∈ stdSimplex2, f x ∈ stdSimplex2) (hne : ∀ x ∈ stdSimplex2, f x ≠ x) @@ -520,6 +522,7 @@ private theorem subdivSperner_odd_sum /-- From a rainbow triangle in the subdivision, extract three vertices with the desired geometric properties. -/ +@[nolint unusedArguments] private theorem rainbow_triangle_gives_vertices (f : (Fin 3 → ℝ) → (Fin 3 → ℝ)) (hfS : ∀ x ∈ stdSimplex2, f x ∈ stdSimplex2) (hne : ∀ x ∈ stdSimplex2, f x ≠ x) diff --git a/FormalBook/Chapter_01.lean b/FormalBook/Chapter_01.lean index ccced56..4cd7f19 100644 --- a/FormalBook/Chapter_01.lean +++ b/FormalBook/Chapter_01.lean @@ -12,6 +12,7 @@ import Mathlib.Algebra.Notation.Indicator import Mathlib.Topology.Algebra.InfiniteSum.Defs import Mathlib.NumberTheory.EulerProduct.Basic import Mathlib.NumberTheory.PrimesCongruentOne +import Mathlib.Analysis.SpecialFunctions.Pow.Real open Finset Nat open BigOperators @@ -195,22 +196,41 @@ noncomputable def invRealHom : ℕ →*₀ ℝ := grind } lemma S1_eq_smoothNumbers (x : ℝ) : S₁ x = Nat.smoothNumbers (⌊x⌋₊ + 1) := by - ext n; - constructor <;> intro hn <;> simp_all +decide [ S₁ ]; - · by_cases hn0 : n = 0 <;> simp_all +decide [ Nat.smoothNumbers ]; - · exact absurd ( hn ( Nat.find ( Nat.exists_infinite_primes ( ⌊x⌋₊ + 1 ) ) ) ( Nat.find_spec ( Nat.exists_infinite_primes ( ⌊x⌋₊ + 1 ) ) |>.2 ) ) ( by exact not_le_of_gt ( Nat.lt_of_floor_lt ( Nat.find_spec ( Nat.exists_infinite_primes ( ⌊x⌋₊ + 1 ) ) |>.1 ) ) ); - · exact fun p pp dp => Nat.lt_succ_of_le <| Nat.le_floor <| hn p pp dp; - · intro p pp dp; - -- Since $p$ is a prime factor of $n$ and $n$ is in the set of smooth numbers up to $\lfloor x \rfloor + 1$, it follows that $p \leq \lfloor x \rfloor$. - have hp_le_floor : p ≤ ⌊x⌋₊ := by - simp_all +decide [ Nat.smoothNumbers ]; - linarith [ hn.2 p pp dp hn.1 ]; - exact le_trans ( Nat.cast_le.mpr hp_le_floor ) ( Nat.floor_le ( show x ≥ 0 from le_of_not_gt fun h => by { rw [ Nat.floor_of_nonpos h.le ] at hp_le_floor; aesop } ) ) + ext n + simp only [S₁, Nat.smoothNumbers, Set.mem_setOf_eq] + constructor + · intro hn + have hn0 : n ≠ 0 := by + intro hn0 + obtain ⟨p, hp_le, hp_prime⟩ := Nat.exists_infinite_primes (⌊x⌋₊ + 1) + have hle := hn p hp_prime (hn0 ▸ dvd_zero p) + have : (p : ℝ) ≤ x := hle + have : p ≤ ⌊x⌋₊ := Nat.le_floor this + omega + refine ⟨hn0, ?_⟩ + intro p hp + have hp_prime : Nat.Prime p := Nat.prime_of_mem_primeFactorsList hp + have hp_dvd : p ∣ n := Nat.dvd_of_mem_primeFactorsList hp + have hle : (p : ℝ) ≤ x := hn p hp_prime hp_dvd + have : p ≤ ⌊x⌋₊ := Nat.le_floor hle + omega + · rintro ⟨hn0, hn⟩ p hp_prime hp_dvd + have hp_mem : p ∈ n.primeFactorsList := + (Nat.mem_primeFactorsList hn0).2 ⟨hp_prime, hp_dvd⟩ + have hlt : p < ⌊x⌋₊ + 1 := hn p hp_mem + have hp_le : p ≤ ⌊x⌋₊ := by omega + have hx0 : 0 ≤ x := by + by_contra hneg + have : ⌊x⌋₊ = 0 := Nat.floor_of_nonpos (by linarith) + have hp_pos := Nat.Prime.pos hp_prime + omega + exact le_trans (Nat.cast_le.mpr hp_le) (Nat.floor_le hx0) lemma norm_invRealHom_prime_lt_one (p : ℕ) (hp : Nat.Prime p) : ‖invRealHom p‖ < 1 := by - erw [ Real.norm_of_nonneg ]; - · exact inv_lt_one_of_one_lt₀ <| mod_cast hp.one_lt; + erw [Real.norm_of_nonneg] + · exact inv_lt_one_of_one_lt₀ <| mod_cast hp.one_lt · exact inv_nonneg.2 <| Nat.cast_nonneg _ + /-- The inverse function is a monoid homomorphism. -/ noncomputable def invRealMonoidHom : ℕ →* ℝ := { toFun := fun n => (n : ℝ)⁻¹ @@ -220,50 +240,57 @@ noncomputable def invRealMonoidHom : ℕ →* ℝ := simp [mul_comm] } lemma summable_invRealHom_smoothNumbers (N : ℕ) : Summable (fun (m : Nat.smoothNumbers N) ↦ ‖invRealHom m‖) := by - have := @EulerProduct.summable_and_hasSum_smoothNumbers_prod_primesBelow_geometric; - convert this ( show ∀ { p : ℕ }, Nat.Prime p → ‖( invRealMonoidHom : ℕ → ℝ ) p‖ < 1 from ?_ ) N |>.1; - intro p hp; erw [ Real.norm_of_nonneg ( inv_nonneg.2 <| Nat.cast_nonneg _ ) ] ; exact inv_lt_one_of_one_lt₀ <| mod_cast hp.one_lt; + have h : ∀ {p : ℕ}, Nat.Prime p → ‖invRealMonoidHom p‖ < 1 := by + intro p hp + have : invRealMonoidHom p = (p : ℝ)⁻¹ := rfl + rw [this, Real.norm_of_nonneg (inv_nonneg.2 (Nat.cast_nonneg _))] + exact inv_lt_one_of_one_lt₀ (mod_cast hp.one_lt) + have := (EulerProduct.summable_and_hasSum_smoothNumbers_prod_primesBelow_geometric (f := invRealMonoidHom) h N).1 + exact this theorem f_abs_summable (x : ℝ) (n : ℕ) (hxge : x ≥ ↑n) (hxlt : x < ↑n + 1) (f : ArithmeticFunction ℝ) (hf : f.toFun = (S₁ x).indicator fun y ↦ (↑y)⁻¹) : Summable fun x ↦ ‖f x‖ := by - -- By Lemma `summable_invRealHom_smoothNumbers`, we know that `Summable (fun m : Nat.smoothNumbers (n + 1) ↦ ‖invRealHom m‖)`. - have h_summable : Summable (fun m : Nat.smoothNumbers (n + 1) ↦ ‖invRealHom m‖) := by - convert summable_invRealHom_smoothNumbers ( n + 1 ) using 1; - have h_summable_f : Summable (fun m : ℕ ↦ ‖(f.toFun m)‖) := by - have h_eq : ∀ m : ℕ, ‖(f.toFun m)‖ = if m ∈ S₁ x then ‖(invRealHom m)‖ else 0 := by - unfold invRealHom; aesop; - have h_eq : ∀ m : ℕ, ‖(f.toFun m)‖ = if m ∈ Nat.smoothNumbers (n + 1) then ‖(invRealHom m)‖ else 0 := by - convert h_eq using 3; - rw [ S1_eq_smoothNumbers ]; - norm_num [ show ⌊x⌋₊ = n by exact Nat.floor_eq_iff ( by linarith ) |>.2 ⟨ by linarith, by linarith ⟩ ]; - refine' summable_of_sum_le _ _; - exact ∑' m : Nat.smoothNumbers ( n + 1 ), ‖invRealHom m‖; - · exact fun _ => norm_nonneg _; - · intro u; rw [ Finset.sum_congr rfl fun m hm => h_eq m ] ; simp +decide [ Finset.sum_ite ] ; - refine' le_trans _ ( Summable.sum_le_tsum _ _ h_summable ); - rotate_left; - exact Finset.subtype (fun x ↦ x ∈ (n + 1).smoothNumbers) u; - · exact fun _ _ => abs_nonneg _; - · refine' le_of_eq _; - refine' Finset.sum_bij ( fun x hx => ⟨ x, _ ⟩ ) _ _ _ _ <;> aesop; - convert h_summable_f using 1 + have h_floor : ⌊x⌋₊ = n := by + have h1 : (n : ℝ) ≤ x := hxge + have h2 : x < (n : ℝ) + 1 := hxlt + exact Nat.floor_eq_on_Ico n x ⟨h1, h2⟩ + have hS : S₁ x = Nat.smoothNumbers (n + 1) := by + rw [S1_eq_smoothNumbers, h_floor] + have h_summable : Summable (fun m : Nat.smoothNumbers (n + 1) ↦ ‖(m : ℝ)⁻¹‖) := + summable_invRealHom_smoothNumbers (n + 1) + have h_ind : Summable ((Nat.smoothNumbers (n + 1)).indicator (fun m : ℕ ↦ ‖(m : ℝ)⁻¹‖)) := + summable_subtype_iff_indicator.mp h_summable + have h_eq : (fun x ↦ ‖f x‖) = (Nat.smoothNumbers (n + 1)).indicator (fun m : ℕ ↦ ‖(m : ℝ)⁻¹‖) := by + rw [← hS] + ext m + have : f m = f.toFun m := rfl + rw [this, hf, Set.indicator_apply, Set.indicator_apply] + split_ifs with hm + · rfl + · simp + rw [h_eq] + exact h_ind lemma exists_image_primes_eq_primesBelow (n : ℕ) : - ∃ (s : Finset Primes), s.image (fun p ↦ ↑p) = n.primesBelow := by - use n.primesBelow.attach.image (fun p => ⟨p.val, Nat.prime_of_mem_primesBelow p.property⟩); - ext; aesop + ∃ (s : Finset Nat.Primes), s.image (fun p : Nat.Primes ↦ p.1) = n.primesBelow := by + unfold Nat.Primes + refine ⟨Finset.subtype Nat.Prime n.primesBelow, ?_⟩ + ext a + simp only [Finset.mem_image, Finset.mem_subtype, Nat.mem_primesBelow] + constructor + · rintro ⟨p, hp, rfl⟩ + exact hp + · intro ha + exact ⟨⟨a, ha.2⟩, ha, rfl⟩ lemma arithmetic_f (x: ℝ) (n: ℕ) (hxlt : x < n + 1) : ∃ f: ArithmeticFunction ℝ, f.toFun = (S₁ x).indicator (fun y ↦ (↑y)⁻¹) := by { exists ZeroHom.mk ((S₁ x).indicator (fun y: ℕ ↦ (y: ℝ)⁻¹)) (by { have: ¬ (0 ∈ S₁ x) := by { unfold S₁ - rewrite [Set.mem_setOf] intro h - contrapose! h have: ∃ p, Nat.Prime p ∧ p > x := by { - have := @Nat.exists_prime_gt_modEq_one 1 (n+1) (by bound) obtain ⟨p, hp⟩ := this obtain ⟨pprime, ⟨pgt, _⟩⟩ := hp @@ -275,13 +302,8 @@ lemma arithmetic_f (x: ℝ) (n: ℕ) (hxlt : x < n + 1) : ∃ f: ArithmeticFunct exists p } obtain ⟨p, ⟨pprime, pgt⟩⟩ := this - exists p - have: p ∣ 0 := by bound - constructor - . assumption - . constructor - . assumption - . linarith + have hle := h p pprime (dvd_zero p) + linarith } apply Set.indicator_of_notMem assumption @@ -296,13 +318,7 @@ theorem euler_product_rearrangement (x: ℝ) (n: ℕ) (hxge : x ≥ n) (hxlt : x obtain ⟨f, hf⟩ := hf have f_one_eq_one: f.toFun 1 = 1 := by { rewrite [hf]; clear hf - have: 1 ∈ S₁ x := by { - unfold S₁ - rewrite [Set.mem_setOf] - intro p Hp contra - contrapose! contra - exact not_dvd_one Hp - } + have: 1 ∈ S₁ x := fun p Hp contra => (Nat.Prime.not_dvd_one Hp contra).elim simp [this] } have f_mul: f.IsMultiplicative := by { @@ -328,102 +344,80 @@ theorem euler_product_rearrangement (x: ℝ) (n: ℕ) (hxge : x ≥ n) (hxlt : x clear this rewrite [← euler_rewrite] clear euler_rewrite - have hs: ∃ s: Finset Primes, s.image (fun i: Primes => i.val) = (⌊x⌋.natAbs+1).primesBelow := by convert exists_image_primes_eq_primesBelow ( Int.natAbs ⌊x⌋ + 1 ) using 1 + have hs : ∃ s : Finset Nat.Primes, s.image (fun i : Nat.Primes ↦ i.1) = (⌊x⌋.natAbs + 1).primesBelow := + exists_image_primes_eq_primesBelow (Int.natAbs ⌊x⌋ + 1) obtain ⟨s, hs⟩ := hs - have f_eq_one: ∀ p ∉ s, ∑' (e : ℕ), f (↑p ^ e) = 1 := by { + have f_eq_one: ∀ p ∉ s, ∑' (e : ℕ), f (↑p ^ e) = 1 := by intro p hp - have: ∑' e: ℕ, f.toFun (↑p^e) = 1 := by { - have pprime: Nat.Prime ↑p := by { - have: ↑p ∈ { p : ℕ | Nat.Prime p }:= by bound - rewrite [Set.mem_setOf] at this - assumption - } - have: ↑p ∉ (⌊x⌋.natAbs+1).primesBelow := by { - contrapose! hp - rewrite [← hs] at hp - rewrite [Function.Injective.mem_finset_image] at hp - assumption - exact (Set.injective_codRestrict Subtype.property).mp fun ⦃a₁ a₂⦄ a ↦ a - } - rewrite [Nat.mem_primesBelow] at this - simp at this - have pfloor: ↑ p ≥ (⌊x⌋.natAbs+1) := by { - contrapose! pprime - apply this at pprime; assumption - } - clear this - have: ∀ e, e ∉ ({0}: Finset ℕ) → f.toFun (↑p^e) = 0 := by { - intro e he - have enz: e ≠ 0 := by bound - clear he - have pnin: (p: ℕ)^e ∉ S₁ x := by { - unfold S₁ - rewrite [Set.mem_setOf] - intro h - specialize h ↑p - apply h at pprime - simp [enz] at pprime - have: p ≤ ⌊x⌋ := by exact Int.le_floor.mpr pprime - - have contra: p > ⌊x⌋ := by { - have contra: p > ⌊x⌋.natAbs := by bound - omega - } - linarith - } - rewrite [hf] - simp [pnin] - } - clear pfloor - rewrite [tsum_eq_sum this] - simp - bound - - } - bound - } - have tprod_rewrite := @tprod_eq_prod ℝ Primes _ _ (fun p => ∑' (e : ℕ), f (↑p ^ e)) (SummationFilter.unconditional Primes) _ (s) f_eq_one - simp at tprod_rewrite - rewrite [tprod_rewrite] - rewrite [← hs] - have: Set.InjOn (fun i: Primes => (i: Nat)) s := by { - -- Since primes are unique by their value, if two primes are equal, their values must be the same. So, if i and j are primes in s and i.val = j.val, then i must equal j. That makes sense because each prime has a unique value. So the function is injective. - intros i hi j hj hij; exact (by - -- Since primes are unique by their value, if two primes have the same value, they must be the same prime. So, if i.val = j.val, then i = j. That makes sense because each prime has a unique value. So the function is injective. - apply Subtype.ext; exact hij) - } - apply @Finset.prod_image ℕ Primes ℝ _ (fun p => ∑' (k : ℕ), (↑p ^ k)⁻¹) _ s (fun i: Primes => (i: Nat)) at this - conv => - right - rewrite [this] - clear this - apply Finset.prod_congr - rfl - intro y hy - apply congrArg tsum - ext i - have: f.toFun (↑y^i) = (↑↑y ^ i)⁻¹ := by { - rewrite [hf] - have: (y: ℕ)^i ∈ S₁ x := by { - intro p pp dp; have := Nat.Prime.dvd_of_dvd_pow pp dp; simp_all +decide [] ; - -- Since $p$ divides $y.val$ and $y \in s$, we have $p \leq y.val$. - have hp_le_y : p ≤ y.val := by - exact Nat.le_of_dvd y.2.pos this; - -- Since $y$ is a prime in the set $s$, and $s$ is defined as the image of the primes below $\lfloor x \rfloor + 1$, we have $y.val \leq \lfloor x \rfloor$. - have hy_le_floor : y.val ≤ ⌊x⌋₊ := by - -- Since $y$ is a prime in the set $s$, and $s$ is defined as the image of the primes below $\lfloor x \rfloor + 1$, we have $y \leq \lfloor x \rfloor$ by definition of `primesBelow`. - have hy_le_floor : y.val ∈ Nat.primesBelow (⌊x⌋₊ + 1) := by - convert hs ▸ Finset.mem_image_of_mem _ hy using 1; - erw [ show ⌊x⌋ = ⌊x⌋₊ by exact Eq.symm <| Int.toNat_of_nonneg <| Int.floor_nonneg.mpr <| by linarith ] ; norm_num [ Int.natAbs_eq_iff ] ; - exact Nat.le_of_lt_succ ( Nat.lt_of_succ_le ( Nat.succ_le_of_lt ( Nat.lt_of_mem_primesBelow hy_le_floor ) ) ); - exact le_trans ( Nat.cast_le.mpr ( hp_le_y.trans hy_le_floor ) ) ( Nat.floor_le ( show 0 ≤ x by linarith ) ) - } - - simp [this] - } - bound - - + have pprime : Nat.Prime (p : ℕ) := p.2 + have hp_not_below : (p : ℕ) ∉ (⌊x⌋.natAbs + 1).primesBelow := by + intro hmem + rw [← hs, Finset.mem_image] at hmem + obtain ⟨q, hq_s, hq_eq⟩ := hmem + have : q = p := Subtype.ext hq_eq + exact hp (this ▸ hq_s) + have pfloor : (p : ℕ) ≥ ⌊x⌋.natAbs + 1 := by + rw [Nat.mem_primesBelow] at hp_not_below + by_contra hlt + have : (p : ℕ) < ⌊x⌋.natAbs + 1 := by omega + exact hp_not_below ⟨this, pprime⟩ + have h_tsum_zero : ∀ e, e ∉ ({0}: Finset ℕ) → f.toFun (↑p^e) = 0 := by + intro e he + have enz : e ≠ 0 := by + intro he0; subst he0; exact he (Finset.mem_singleton_self 0) + have pnin : (p : ℕ)^e ∉ S₁ x := by + intro h + simp only [S₁, Set.mem_setOf_eq] at h + have h_dvd : (p : ℕ) ∣ (p : ℕ)^e := dvd_pow_self _ enz + have hle : (p : ℝ) ≤ x := h (p : ℕ) pprime h_dvd + have : (p : ℕ) ≤ ⌊x⌋ := Int.le_floor.mpr hle + have contra : (p : ℕ) > ⌊x⌋ := by + have : (p : ℕ) > ⌊x⌋.natAbs := by omega + omega + linarith + rw [hf] + simp [pnin] + have ht : ∑' e : ℕ, f.toFun (↑p ^ e) = ∑ e ∈ {0}, f.toFun (↑p ^ e) := + tsum_eq_sum (s := {0}) h_tsum_zero + simp only [Finset.sum_singleton, pow_zero, f_one_eq_one] at ht + exact ht + have tprod_rewrite := @tprod_eq_prod ℝ Nat.Primes _ _ (fun p : Nat.Primes => ∑' (e : ℕ), f (p.1 ^ e)) (SummationFilter.unconditional Nat.Primes) _ s f_eq_one + rw [tprod_rewrite] + have h_prod_img : (∏ p ∈ (⌊x⌋.natAbs + 1).primesBelow, ∑' k : ℕ, ((p : ℝ) ^ k)⁻¹) = + ∏ y ∈ s, ∑' k : ℕ, ((y.1 : ℝ) ^ k)⁻¹ := by + rw [← hs] + exact Finset.prod_image (s := s) (g := fun i : Nat.Primes ↦ i.1) (f := fun (p : ℕ) ↦ ∑' k : ℕ, ((p : ℝ) ^ k)⁻¹) (fun i _ j _ hij => Subtype.ext hij) + rw [h_prod_img] + refine Finset.prod_congr rfl fun y hy => ?_ + congr 1 + ext e + have hy_mem : y.1 ∈ (⌊x⌋.natAbs + 1).primesBelow := by + rw [← hs] + exact Finset.mem_image_of_mem (fun i : Nat.Primes ↦ i.1) hy + have hy_le : (y.1 : ℝ) ≤ x := by + rw [Nat.mem_primesBelow] at hy_mem + have hx0 : 0 ≤ x := by linarith + have : (y.1 : ℝ) ≤ ⌊x⌋₊ := by + have : y.1 < ⌊x⌋.natAbs + 1 := hy_mem.1 + have h1 : 0 ≤ ⌊x⌋ := Int.floor_nonneg.mpr hx0 + have h_floor : ⌊x⌋.natAbs = ⌊x⌋₊ := by + exact_mod_cast (Int.natAbs_of_nonneg h1).trans (Int.toNat_of_nonneg h1).symm + have : y.1 ≤ ⌊x⌋₊ := by omega + exact_mod_cast this + exact le_trans this (Nat.floor_le hx0) + have h_mem_S1 : (y.1 : ℕ) ^ e ∈ S₁ x := by + intro p hp_prime hp_dvd + have hp_eq : p = y.1 := by + have := hp_prime.dvd_of_dvd_pow hp_dvd + have hy_prime : y.1.Prime := y.2 + exact (Nat.dvd_prime hy_prime).mp this |>.resolve_left (Nat.Prime.ne_one hp_prime) + rw [hp_eq] + exact hy_le + have : f.toFun (y.1 ^ e) = ((y.1 : ℝ) ^ e)⁻¹ := by + have : f.toFun = (S₁ x).indicator (fun y ↦ (y : ℝ)⁻¹) := hf + rw [this, Set.indicator_of_mem h_mem_S1] + push_cast; rfl + exact this } theorem log_riemann_bound (x: ℝ) (n: ℕ) (hxge : x ≥ n) (hxlt : x < n + 1): Real.log x ≤ ∑ k ∈ Icc 1 n, (k : ℝ)⁻¹ := by { diff --git a/FormalBook/Chapter_02.lean b/FormalBook/Chapter_02.lean index 206da88..e3718ae 100644 --- a/FormalBook/Chapter_02.lean +++ b/FormalBook/Chapter_02.lean @@ -7,7 +7,8 @@ import Mathlib.Algebra.Lie.OfAssociative import Mathlib.Analysis.Convex.SpecificFunctions.Basic import Mathlib.Analysis.Convex.SpecificFunctions.Deriv import Mathlib.Data.Nat.Choose.Factorization -import Mathlib.Data.Real.StarOrdered +import Mathlib.Analysis.Real.Sqrt +import Mathlib.Tactic.ContinuousFunctionalCalculus import Mathlib.NumberTheory.Harmonic.Defs import Mathlib.NumberTheory.Primorial import Mathlib.Tactic.NormNum.Prime @@ -53,18 +54,17 @@ theorem real_main_inequality {x : ℝ} (n_large : (512 : ℝ) ≤ x) : mul_one_div, ← log_nonpos_iff (hf' x h5).le, ← hf x h5] have h : ConcaveOn ℝ (Set.Ioi 0.5) f := by apply ConcaveOn.sub - apply ConcaveOn.add - exact strictConcaveOn_log_Ioi.concaveOn.subset - (Set.Ioi_subset_Ioi (by norm_num)) (convex_Ioi 0.5) - convert ((strictConcaveOn_sqrt_mul_log_Ioi.concaveOn.comp_linearMap - ((2 : ℝ) • LinearMap.id))) using 1 - · ext x - norm_num1 - simp - field_simp - apply ConvexOn.smul - refine div_nonneg (log_nonneg (by norm_num1)) (by norm_num1) - exact convexOn_id (convex_Ioi (0.5 : ℝ)) + · apply ConcaveOn.add + · exact strictConcaveOn_log_Ioi.concaveOn.subset + (Set.Ioi_subset_Ioi (by norm_num)) (convex_Ioi 0.5) + · have h1 := (strictConcaveOn_sqrt_mul_log_Ioi.concaveOn.comp_linearMap ((2 : ℝ) • (LinearMap.id : ℝ →ₗ[ℝ] ℝ))) + have hsub : Set.Ioi (0.5 : ℝ) ⊆ ((2 : ℝ) • (LinearMap.id : ℝ →ₗ[ℝ] ℝ)) ⁻¹' Set.Ioi 1 := by + intro x hx + simp only [Set.mem_preimage, Set.mem_Ioi, LinearMap.smul_apply, LinearMap.id_apply, smul_eq_mul] + linarith [Set.mem_Ioi.mp hx] + exact h1.subset hsub (convex_Ioi 0.5) + · have hpos : 0 ≤ log 4 / 3 := div_nonneg (log_nonneg (by norm_num1)) (by norm_num1) + exact (convexOn_id (convex_Ioi (0.5 : ℝ))).smul hpos suffices ∃ x1 x2, 0.5 < x1 ∧ x1 < x2 ∧ x2 ≤ x ∧ 0 ≤ f x1 ∧ f x2 ≤ 0 by obtain ⟨x1, x2, h1, h2, h0, h3, h4⟩ := this exact (h.right_le_of_le_left'' h1 ((h1.trans h2).trans_le h0) h2 h0 (h4.trans h3)).trans h4 @@ -150,7 +150,7 @@ theorem centralBinom_le_of_no_bertrand_prime (n : ℕ) (n_big : 2 < n) refine' pow_le_pow_right₀ n2_pos ((Finset.card_le_card fun x hx ↦ _).trans this.le) obtain ⟨h1, h2⟩ := Finset.mem_filter.1 hx exact Finset.mem_Icc.mpr ⟨(Finset.mem_filter.1 h1).2.one_lt.le, h2⟩ - · refine' le_trans _ (primorial_le_4_pow (2 * n / 3)) + · refine' le_trans _ (primorial_le_four_pow (2 * n / 3)) refine' (Finset.prod_le_prod' fun p hp ↦ (_ : f p ≤ p)).trans _ · obtain ⟨h1, h2⟩ := Finset.mem_filter.1 hp refine' (pow_le_pow_right₀ (Finset.mem_filter.1 h1).2.one_lt.le _).trans (pow_one p).le @@ -214,8 +214,7 @@ theorem harmonic_number_bounds {n : ℕ} (hn : 1 < n) : Real.log n + 1 / n < harmonic n ∧ harmonic n < Real.log n + 1 := by constructor · induction hn <;> norm_num [harmonic] at * - · norm_num [Finset.sum_range_succ] - linarith [@Real.log_lt_sub_one_of_pos 2 zero_lt_two (OfNat.one_ne_ofNat 2).symm] + · linarith [@Real.log_lt_sub_one_of_pos 2 zero_lt_two (OfNat.one_ne_ofNat 2).symm] · rw [Finset.sum_range_succ] rename_i k hk ih rw [show (k : ℝ) + 1 = k * (1 + (k : ℝ) ⁻¹) by diff --git a/FormalBook/Chapter_04.lean b/FormalBook/Chapter_04.lean index 75afca2..0524a58 100644 --- a/FormalBook/Chapter_04.lean +++ b/FormalBook/Chapter_04.lean @@ -54,34 +54,21 @@ lemma lemma₁ {p : ℕ} [h : Fact p.Prime] : -- TODO: golf, and perhaps make it even close to book proof lemma lemma₂ (n m : ℕ) (hn : n = 4 * m + 3) : - ¬ ∃ a b, n = a ^2 + b ^2 := by - push_neg - intro a b - by_contra h - have : (n : ZMod 4) = a ^ 2 + b ^ 2 := by + ¬ ∃ a b, n = a ^ 2 + b ^ 2 := by + intro ⟨a, b, h⟩ + have : (n : ZMod 4) = a ^ 2 + b ^ 2 := by rw [h] simp only [Nat.cast_add, Nat.cast_pow] rw [hn] at this simp only [Nat.cast_add, Nat.cast_mul, Nat.cast_ofNat] at this rw [mul_eq_zero_of_left (by rfl) (m : ZMod 4), zero_add] at this - have hx : ∀ (x : ZMod 4), x ^2 ∈ ({0, 1} : Finset (ZMod 4)) := by - intro x - fin_cases x <;> simp - · exact Or.inl rfl - · exact Or.inr rfl - have ha := hx <| a - have hb := hx <| b - generalize hA: (a : ZMod 4) ^ 2 = A - generalize hB: (b : ZMod 4) ^ 2 = B - rw [hA, hB] at this - rw [hA] at ha - rw [hB] at hb - fin_cases A <;> fin_cases B <;> norm_num at this <;> tauto + have h_mod : ∀ (x y : ZMod 4), (3 : ZMod 4) ≠ x ^ 2 + y ^ 2 := by decide + exact h_mod a b this -- We follow a similar path taken by Jeremy Tan and Thomas Browning in -- mathlib4/Archive/ZagierTwoSquares.lean. -theorem theorem₁ {p : ℕ} [h : Fact p.Prime] (hp : p % 4 = 1) : ∃ a b : ℕ, a ^ 2 + b ^ 2 = p := by +theorem theorem₁ {p : ℕ} [h : Fact p.Prime] (hp : p % 4 = 1) : ∃ a b : ℕ, a ^ 2 + b ^ 2 = p := by sorry section Sets @@ -94,20 +81,21 @@ variable (k : ℕ) [hk : Fact (4 * k + 1).Prime] def S : Set (ℤ × ℤ × ℤ) := {((x, y, z) : ℤ × ℤ × ℤ) | 4 * x * y + z ^ 2 = 4 * k + 1 ∧ x > 0 ∧ y > 0} omit hk in -lemma S_lower_bound {x y z : ℤ} (h : ⟨x, y, z⟩ ∈ S k) : 0 < x ∧ 0 < y := ⟨h.2.1, h.2.2⟩ +lemma S_lower_bound {x y z : ℤ} (h : ⟨x, y, z⟩ ∈ S k) : 0 < x ∧ 0 < y := ⟨h.2.1, h.2.2⟩ omit hk in lemma S_upper_bound {x y z : ℤ} (h : ⟨x, y, z⟩ ∈ S k) : x ≤ k ∧ y ≤ k := by obtain ⟨_, _⟩ := S_lower_bound k h - simp [S, mem_setOf_eq] at h + simp [S] at h refine ⟨?_, ?_⟩ all_goals try nlinarith -- todo use Fin 2 instead of ({(0 : ℤ), 1}) /-- Embedding of the set `S k` into a finite product of finite sets for `Fintype` instance. -/ +@[nolint defsWithUnderscore] def embed_S : S k → Ioc (0 : ℤ) k ×ˢ Ioc (0 : ℤ) k ×ˢ ({(0 : ℤ), 1}) := - fun (⟨⟨x, y, z⟩, h⟩ : S k) ↦ by + fun (⟨⟨x, y, z⟩, h⟩ : S k) ↦ by have lb := S_lower_bound k h have ub := S_upper_bound k h exact ⟨⟨x, y, if 0 ≤ z then 1 else 0⟩, ⟨⟨lb.1, ub.1⟩, ⟨lb.2, ub.2⟩, by @@ -115,27 +103,23 @@ def embed_S : S k → Ioc (0 : ℤ) k ×ˢ Ioc (0 : ℤ) k ×ˢ ({(0 : ℤ), 1}) Int.lt_or_le z 0 ⟩⟩ omit hk in -lemma embed_S_injective : Function.Injective (embed_S k):= by - intro s1 s2 hS - simp [embed_S] at hS - ext - · exact hS.1 - · exact hS.2.1 - · have := hS.2.2 - have ⟨⟨x1, y1, z1⟩, ⟨h1, _, _⟩⟩ := s1 - have ⟨⟨x2, y2, z2⟩, ⟨h2, _, _⟩⟩ := s2 - have hz_eq_z: z1 ^ 2 = z2 ^ 2 := by - nlinarith - simp at this - by_cases hz1 : 0 ≤ z1 - · simp [hz1] at this - by_cases hz2 : 0 ≤ z2 - · nlinarith - · simp [hz2] at this - · by_cases hz2 : 0 ≤ z2 - · simp [hz2] at this - tauto - · nlinarith +lemma embed_S_injective : Function.Injective (embed_S k) := by + intro ⟨⟨x1, y1, z1⟩, h1⟩ ⟨⟨x2, y2, z2⟩, h2⟩ hS + have h_val := congr_arg Subtype.val hS + simp only [embed_S, Prod.mk.injEq] at h_val + obtain ⟨rfl, rfl, hz⟩ := h_val + have hz_sq : z1 ^ 2 = z2 ^ 2 := by + have h1_eq := h1.1 + have h2_eq := h2.1 + linarith + have hz_eq : z1 = z2 := by + split_ifs at hz with hz1 hz2 + · nlinarith + · linarith + · linarith + · nlinarith + subst hz_eq + rfl noncomputable instance : Fintype (S k) := by refine' Fintype.ofInjective (embed_S k) (embed_S_injective k) @@ -155,15 +139,20 @@ def linearInvo : Function.End (S k) := fun ⟨⟨x, y, z⟩, h⟩ => ⟨⟨y, x, simp only [S, Set.mem_setOf_eq] at h ⊢ exact ⟨by linarith [h], h.2.2, h.2.1⟩ ⟩ -theorem linearInvo_sq : linearInvo k ^2 = (1 : Function.End (S k)) := by +theorem linearInvo_sq : linearInvo k ^ 2 = (1 : Function.End (S k)) := by change linearInvo k ∘ linearInvo k = id - funext x - simp [linearInvo] + funext ⟨⟨x, y, z⟩, h⟩ + rw [show (linearInvo k ∘ linearInvo k) ⟨(x, y, z), h⟩ = + linearInvo k (linearInvo k ⟨(x, y, z), h⟩) from rfl] + apply Subtype.ext + dsimp [linearInvo] + ext <;> simp theorem linearInvo_no_fixedPoints : IsEmpty (fixedPoints (linearInvo k)) := by simp only [isEmpty_subtype, mem_fixedPoints, Subtype.forall, Prod.forall] intro x y z h hfixed - simp only [IsFixedPt, linearInvo, Subtype.mk.injEq, Prod.mk.injEq] at hfixed + have hfixed' : (linearInvo k ⟨⟨x, y, z⟩, h⟩).1.2.2 = z := by rw [hfixed] + have : -z = z := hfixed' have : z = 0 := by linarith obtain ⟨h, _, _⟩ := h simp only [this, ne_eq, OfNat.ofNat_ne_zero, not_false_eq_true, zero_pow, add_zero] at h @@ -171,7 +160,7 @@ theorem linearInvo_no_fixedPoints : IsEmpty (fixedPoints (linearInvo k)) := by simp [mul_assoc, Int.add_emod] at h /-- The subset of `S k` where `z` is positive. -/ -def T : Set (S k) := {⟨(_, _, z), _⟩ : S k | z > 0} +def T : Set (S k) := {⟨(_, _, z), _⟩ : S k | z > 0} noncomputable instance : Fintype <| T k := by exact Fintype.ofFinite ↑(T k) @@ -180,6 +169,7 @@ noncomputable instance : Fintype <| T k := by def U : Set (S k) := {⟨(x, y, z), _⟩ | (x - y) + z > 0} noncomputable instance : Fintype <| U k := Fintype.ofFinite ↑(U k) +noncomputable instance (s : Set (U k)) : Fintype s := Fintype.ofFinite s theorem sameCard : Fintype.card (U k) = Fintype.card (T k) := by sorry @@ -187,6 +177,7 @@ theorem sameCard : Fintype.card (U k) = Fintype.card (T k) := by /- 2. -/ /-- The function underlying the second involution. -/ +@[nolint defsWithUnderscore] def secondInvo_fun := fun ((x,y,z) : ℤ × ℤ × ℤ) ↦ (x - y + z, y, 2 * y - z) /-- The second involution that we study is an involution on the set U. -/ @@ -205,11 +196,16 @@ def secondInvo : Function.End (U k) := fun ⟨⟨⟨x, y, z⟩, hS⟩, h⟩ => /-- `secondInvo k` is indeed an involution. -/ theorem secondInvo_sq : secondInvo k ^ 2 = 1 := by change secondInvo k ∘ secondInvo k = id - funext ⟨⟨x, y, z⟩, h⟩ - rw [comp_apply] - simp only [secondInvo, secondInvo_fun, sub_sub_cancel, id_eq, Subtype.mk.injEq, Prod.mk.injEq, - and_true] - ring_nf + funext ⟨⟨⟨x, y, z⟩, hS⟩, h⟩ + rw [show (secondInvo k ∘ secondInvo k) ⟨⟨(x, y, z), hS⟩, h⟩ = + secondInvo k (secondInvo k ⟨⟨(x, y, z), hS⟩, h⟩) from rfl] + apply Subtype.ext + apply Subtype.ext + dsimp [secondInvo, secondInvo_fun] + ext + · ring + · rfl + · ring variable [hk : Fact (4 * k + 1).Prime] theorem k_pos : 0 < k := by @@ -241,48 +237,37 @@ theorem eq_of_mem_fixedPoints : fixedPoints (secondInvo k) = singletonFixedPoint /-- `secondInvo k` has exactly one fixed point. -/ theorem card_fixedPoints_eq_one : Fintype.card (fixedPoints (secondInvo k)) = 1 := by - simp only [eq_of_mem_fixedPoints, singletonFixedPoint] - rfl + have : fixedPoints (secondInvo k) = (singletonFixedPoint k : Set (U k)) := eq_of_mem_fixedPoints k + rw [this] + simp [singletonFixedPoint] theorem card_T_odd : Odd <| Fintype.card <| T k := by sorry /- 3. -/ /-- The third, trivial, involution `(x, y, z) ↦ (y, x, z)`. -/ -def trivialInvo : Function.End (T k) := fun ⟨⟨⟨x, y, z⟩, ⟨h, hx, hy⟩⟩, hz⟩ => ⟨⟨⟨y, x, z⟩, by - exact ⟨by rw [← h,Int.mul_assoc, Int.mul_comm y x, Int.mul_assoc], hy, hx⟩⟩, hz⟩ +def trivialInvo : Function.End (T k) := fun ⟨⟨⟨x, y, z⟩, hS⟩, hz⟩ => ⟨⟨⟨y, x, z⟩, by + obtain ⟨h, hx, hy⟩ := hS + exact ⟨by rw [← h, Int.mul_assoc, Int.mul_comm y x, Int.mul_assoc], hy, hx⟩⟩, hz⟩ omit hk in theorem trivialInvo_apply (x y z : ℤ) (hS : ⟨x, y, z⟩ ∈ S k) (hT : ⟨⟨x, y, z⟩ , hS⟩ ∈ T k) (hS' : ⟨y, x, z⟩ ∈ S k) (hT' : ⟨⟨y, x, z⟩ , hS'⟩ ∈ T k) : - trivialInvo k ⟨⟨⟨x, y, z⟩, hS⟩, hT⟩ = ⟨⟨⟨y,x,z⟩, hS'⟩, hT'⟩ := by - simp [trivialInvo] - aesop + trivialInvo k ⟨⟨⟨x, y, z⟩, hS⟩, hT⟩ = ⟨⟨⟨y,x,z⟩, hS'⟩, hT'⟩ := rfl omit hk in /-- If `trivialInvo k` has a fixed point, a representation of `4 * k + 1` as a sum of two squares can be extracted from it. -/ theorem sq_add_sq_of_nonempty_fixedPoints (hn : (fixedPoints (trivialInvo k)).Nonempty) : ∃ a b : ℤ, a ^ 2 + b ^ 2 = 4 * k + 1 := by - simp only [sq] obtain ⟨⟨⟨⟨x, y, z⟩, hS⟩, hT⟩, hf⟩ := hn - have hf := mem_fixedPoints_iff.mp hf - simp only [ Subtype.mk.injEq, Prod.mk.injEq, true_and] at hf - have : (trivialInvo k ⟨⟨(x, y, z), hS⟩, hT⟩).1.1 = (⟨⟨(x, y, z), hS⟩, hT⟩ : T k).1.1 := by + have hf' : (trivialInvo k ⟨⟨⟨x, y, z⟩, hS⟩, hT⟩).1.1.1 = (⟨⟨⟨x, y, z⟩, hS⟩, hT⟩ : T k).1.1.1 := by rw [hf] - simp at this - rw [trivialInvo_apply] at this - · simp at this - use (2 * y), z - rw [show 2 * y * (2 * y) = 4 * y * y by linarith, ← hS.1] - congr - · exact this.1 - · ring - --TODO: avoid repeating from the definition of trivialInvo here! - · exact ⟨by rw [← hS.1,Int.mul_assoc, Int.mul_comm y x, Int.mul_assoc], hS.2.2, hS.2.1⟩ - · exact hT - - + have h_eq : y = x := hf' + use 2 * y, z + have hS1 := hS.1 + subst h_eq + linear_combination hS1 theorem trivialInvo_fixedPoints : (fixedPoints (trivialInvo k)).Nonempty := by sorry @@ -290,12 +275,17 @@ end Involutions theorem theorem₂ {p : ℕ} [h : Fact p.Prime] (hp : p % 4 = 1) : ∃ a b : ℕ, a ^ 2 + b ^ 2 = p := by - rw [← div_add_mod p 4, hp] at h ⊢ - let k := p / 4 - have ⟨a, b, h⟩ := sq_add_sq_of_nonempty_fixedPoints k <| trivialInvo_fixedPoints k + have hk : Fact (4 * (p / 4) + 1).Prime := ⟨by + have : 4 * (p / 4) + 1 = p := by omega + rw [this] + exact h.out⟩ + have ⟨a, b, h_sq⟩ := sq_add_sq_of_nonempty_fixedPoints (p / 4) (trivialInvo_fixedPoints (p / 4)) refine ⟨a.natAbs, b.natAbs, ?_⟩ + have hp_eq : p = 4 * (p / 4) + 1 := by omega + rw [hp_eq] zify - simpa only [sq_abs] using h + simp only [sq_abs] + exact h_sq -- The windged square of area 4xy + z^2 = 73 that corresponds to (x,y,z) = (3,4,5) diff --git a/FormalBook/Chapter_05.lean b/FormalBook/Chapter_05.lean index 9bb89d2..262bb6a 100644 --- a/FormalBook/Chapter_05.lean +++ b/FormalBook/Chapter_05.lean @@ -39,6 +39,7 @@ namespace quadratic_reciprocity variable (p : ℕ) (h_p : p ≠ 2) [Fact (Nat.Prime p)] /-- The Legendre symbol `(a / p)`, where `p` is an odd prime. -/ +@[nolint defsWithUnderscore] def legendre_sym (a : ℤ) : ℤ := ite ( (a : ZMod p) = 0) 0 $ ite (∃ b : ZMod p, a = (b ^ (2 : ℤ) : ZMod p)) 1 (-1) diff --git a/FormalBook/Chapter_06.lean b/FormalBook/Chapter_06.lean index dfb0ab4..0d5c13b 100644 --- a/FormalBook/Chapter_06.lean +++ b/FormalBook/Chapter_06.lean @@ -6,7 +6,8 @@ Authors: Moritz Firsching, Nick Kuhn import Mathlib.Algebra.Lie.OfAssociative import Mathlib.Algebra.Order.Ring.Star import Mathlib.Data.Int.Star -import Mathlib.Data.Real.StarOrdered +import Mathlib.Analysis.Real.Sqrt +import Mathlib.Tactic.ContinuousFunctionalCalculus import Mathlib.RingTheory.LittleWedderburn import Mathlib.RingTheory.SimpleRing.Principal @@ -134,7 +135,9 @@ lemma div_of_qpoly_div (k n q : ℕ) (hq : 1 < q) (hk : 0 < k) (hn : 0 < n) exact Nat.eq_add_of_sub_eq hkm rfl exact Nat.strongRecOn n this -/-- The centralizer of an element `x` is isomorphic to the stabilizer of `x` under the conjugation action. -/ +/-- The centralizer of an element `x` is isomorphic to the stabilizer of `x` +under the conjugation action. -/ +@[nolint defsWithUnderscore] def ConjAct_stabilizer_centralizer_eq : ∀ x : Rˣ, Set.centralizer {x} ≃ MulAction.stabilizer (ConjAct Rˣ) x := by intro x @@ -151,22 +154,25 @@ def ConjAct_stabilizer_centralizer_eq : left_inv := congrFun rfl right_inv := congrFun rfl} --- Orbit stabilizer theorem, specialized to conjugacy classes lemma orbit_stabilizer [Fintype R] (A: ConjClasses Rˣ) [Fintype A.carrier] : Fintype.card Rˣ = (Fintype.card A.carrier) * - (@Fintype.card (Set.centralizer {ConjClasses.exists_rep A|>.choose}) ( - Fintype.ofFinite (Set.centralizer {ConjClasses.exists_rep A|>.choose}))) := by - letI := Fintype.ofFinite (Set.centralizer {ConjClasses.exists_rep A|>.choose}) - letI : Fintype ↑(MulAction.orbit (ConjAct Rˣ) (ConjClasses.exists_rep A|>.choose)) - := by refine Set.fintypeRange fun m => m • Exists.choose ?_ - letI : Fintype { x // x ∈ MulAction.stabilizer (ConjAct Rˣ) - (ConjClasses.exists_rep A|>.choose) } := Fintype.ofFinite _ - have := MulAction.card_orbit_mul_card_stabilizer_eq_card_group (ConjAct Rˣ) - (ConjClasses.exists_rep A|>.choose) - replace this := this.symm - rw [Fintype.card_congr <| ConjAct_stabilizer_centralizer_eq (ConjClasses.exists_rep A|>.choose)] - convert this - rw [ConjAct.orbit_eq_carrier_conjClasses, (ConjClasses.exists_rep A|>.choose_spec)] + (Fintype.card (Set.centralizer {ConjClasses.exists_rep A|>.choose})) := by + classical + let a := ConjClasses.exists_rep A|>.choose + have ha : ConjClasses.mk a = A := ConjClasses.exists_rep A|>.choose_spec + have horbit : MulAction.orbit (ConjAct Rˣ) a = A.carrier := by + rw [ConjAct.orbit_eq_carrier_conjClasses, ha] + have e_orbit : (MulAction.orbit (ConjAct Rˣ) a : Set Rˣ) ≃ (A.carrier : Set Rˣ) := + Equiv.setCongr horbit + have e_stab : (MulAction.stabilizer (ConjAct Rˣ) a : Set (ConjAct Rˣ)) ≃ + (Set.centralizer {a} : Set Rˣ) := + (ConjAct_stabilizer_centralizer_eq a).symm + have h1 := MulAction.card_orbit_mul_card_stabilizer_eq_card_group (ConjAct Rˣ) a + have h2 : Fintype.card Rˣ = Fintype.card (ConjAct Rˣ) := + (Fintype.card_congr ConjAct.toConjAct.toEquiv).symm + rw [h2, ← h1, Fintype.card_congr e_orbit] + congr 1 + exact Fintype.card_congr e_stab section wedderburn @@ -263,9 +269,12 @@ theorem wedderburn (h: Fintype R): IsField R := by have := @eval_dvd ℤ _ _ _ q h_noneval simp only [eval_mul, eval_sub, eval_pow, eval_X, eval_one, IsUnit.mul_iff] at this rw [← hq] at * - convert this - · simp [hq_pow_pos <| n_k A] - · simp [hq_pow_pos n] + have h_cast_nk : (((q ^ (n_k A) - 1 : ℕ) : ℤ)) = (q : ℤ) ^ (n_k A) - 1 := + Nat.cast_sub (hq_pow_pos (n_k A)) + have h_cast_n : (((q ^ n - 1 : ℕ) : ℤ)) = (q : ℤ) ^ n - 1 := + Nat.cast_sub (hq_pow_pos n) + rw [h_cast_nk, h_cast_n] + exact this simp only [eval_sub, eval_pow, eval_X, eval_one] at h₁_dvd have h1' : (((q:ℤ) ^ n - (1 : ℕ)) : ℤ) = ((q - (1 :ℕ) : ℕ):ℤ) + ∑ A : S', (q ^ n - 1) / (q ^ (n_k A) - 1) := by diff --git a/FormalBook/Chapter_07.lean b/FormalBook/Chapter_07.lean index d801d65..e4186dd 100644 --- a/FormalBook/Chapter_07.lean +++ b/FormalBook/Chapter_07.lean @@ -6,6 +6,7 @@ Authors: Moritz Firsching import Mathlib.Tactic import Mathlib.Data.Matrix.Basic import Mathlib.LinearAlgebra.Matrix.Hermitian +import Mathlib.LinearAlgebra.UnitaryGroup /-! # The spectral theorem and Hadamard's determinant problem diff --git a/FormalBook/Chapter_08.lean b/FormalBook/Chapter_08.lean index 7a01bcb..4499691 100644 --- a/FormalBook/Chapter_08.lean +++ b/FormalBook/Chapter_08.lean @@ -92,6 +92,7 @@ Let `n : ℕ`, `n ≥ 1` be fixed, and consider `f_aux n x = x ^ n * (1 - x) ^ n -/ /-- The auxiliary function `xⁿ * (1 - x)ⁿ / n!` used in the irrationality proofs. -/ +@[nolint defsWithUnderscore] noncomputable def f_aux (n : ℕ) (x : ℝ) := x ^ n * (1 - x) ^ n / n.factorial lemma lem_aux_i (n : ℕ) (x : ℝ) : ∃ c : ℕ → ℤ, f_aux n x = ∑ i ∈ Icc n (2 * n), (c i) * x ^ i := by @@ -105,8 +106,9 @@ lemma lem_aux_ii (n : ℕ) (x : ℝ) (h_1 : 0 < x) (h_2 : x < 0) : WARNING: There might be a better way to state this, not sure what the best API for derivatives of smooth (polynomial) functions is -/ -lemma lem_aux_iii (n : ℕ) (k : ℕ): iteratedDeriv k (f_aux n) 0 ∈ Set.range (fun (q : ℚ) ↦ (q : ℝ)) ∧ - iteratedDeriv k (f_aux n) 1 ∈ Set.range (fun (q : ℚ) ↦ (q : ℝ)) := by +lemma lem_aux_iii (n : ℕ) (k : ℕ): + iteratedDeriv k (f_aux n) 0 ∈ Set.range (fun (q : ℚ) ↦ (q : ℝ)) ∧ + iteratedDeriv k (f_aux n) 1 ∈ Set.range (fun (q : ℚ) ↦ (q : ℝ)) := by sorry diff --git a/FormalBook/Chapter_09.lean b/FormalBook/Chapter_09.lean index ee04254..b39771c 100644 --- a/FormalBook/Chapter_09.lean +++ b/FormalBook/Chapter_09.lean @@ -186,7 +186,11 @@ theorem euler_series : ∑' n : ℕ, ((n : ℝ) ^ 2)⁻¹ = π ^ 2 / 6 := by · intro uv huv beta_reduce congr 1 - norm_num [f', Matrix.det_fin_two, J] + dsimp [f'] + rw [LinearMap.det_conj (Matrix.toLin' J) (LinearEquiv.finTwoArrow ℝ ℝ)] + rw [LinearMap.det_toLin', Matrix.det_fin_two] + dsimp [J] + norm_num · exact measurableSet_S · intro uv huv refine (hasFDerivWithinAt_of_mem_nhds ?_).mpr ?_ @@ -195,8 +199,26 @@ theorem euler_series : ∑' n : ℕ, ((n : ℝ) ^ 2)⁻¹ = π ^ 2 / 6 := by · rw [hasFDerivAt_iff_isLittleO_nhds_zero] suffices ∀ h, f (uv + h) - f uv - (f' uv) h = 0 by simp [this] intro h - simp [f, f', J, Matrix.mulVec] - split_ands <;> ring + have h1 : (Matrix.toLin' J ![h.1, h.2]) 0 = h.1 - h.2 := by + rw [Matrix.toLin'_apply] + simp [J, Matrix.mulVec] + ring + have h2 : (Matrix.toLin' J ![h.1, h.2]) 1 = h.1 + h.2 := by + rw [Matrix.toLin'_apply] + simp [J, Matrix.mulVec] + apply Prod.ext + · simp only [f, f', LinearMap.coe_toContinuousLinearMap', LinearMap.comp_apply, + LinearEquiv.coe_coe, LinearEquiv.finTwoArrow_apply, + LinearEquiv.finTwoArrow_symm_apply, + Prod.fst_sub, Prod.fst_zero, Prod.fst_add, Prod.snd_add] + rw [h1] + ring + · simp only [f, f', LinearMap.coe_toContinuousLinearMap', LinearMap.comp_apply, + LinearEquiv.coe_coe, LinearEquiv.finTwoArrow_apply, + LinearEquiv.finTwoArrow_symm_apply, + Prod.snd_sub, Prod.snd_zero, Prod.snd_add, Prod.fst_add] + rw [h2] + ring · exact bijective_f.injective.injOn clear! f finv J f' -- Pull the ofReal upwards to prepare going back to regular ℝ valued interval based integrals. @@ -352,7 +374,7 @@ theorem euler_series : ∑' n : ℕ, ((n : ℝ) ^ 2)⁻¹ = π ^ 2 / 6 := by all_goals · refine setLIntegral_congr_fun measurableSet_Ioo fun u hu => ?_ congr 1 - rw [integral_inv_sq_add_sq] + rw [intervalIntegral.integral_inv_sq_add_sq] swap · rw [sqrt_ne_zero] <;> nlinarith only [hu.1, hu.2] simp_rw [sub_eq_add_neg, ←arctan_neg] @@ -454,8 +476,8 @@ theorem euler_series : ∑' n : ℕ, ((n : ℝ) ^ 2)⁻¹ = π ^ 2 / 6 := by · exact h3 · exact h1 show deriv (fun u => ((arctan ∘ fun u => _ / ((sqrt ∘ fun u => _) u)) ^ 2) u) u = _ - erw [deriv_fun_pow, deriv_comp, deriv_fun_div, deriv_comp, deriv_fun_sub] - erw [deriv_sqrt, deriv_fun_pow] + erw [deriv_pow, deriv_comp, deriv_fun_div, deriv_comp, deriv_fun_sub] + erw [deriv_sqrt, deriv_pow] erw [Real.deriv_arctan, deriv_id'', deriv_const] · simp field_simp @@ -516,8 +538,8 @@ theorem euler_series : ∑' n : ℕ, ((n : ℝ) ^ 2)⁻¹ = π ^ 2 / 6 := by · exact h1 show deriv (fun u => -2 * ((arctan ∘ fun u => _ / ((sqrt ∘ fun u => _) u)) ^ 2) u) u = _ erw [deriv_const_mul] - erw [deriv_fun_pow, deriv_comp, deriv_fun_div, deriv_comp, deriv_fun_sub] - erw [deriv_sqrt, deriv_sub, deriv_fun_pow] + erw [deriv_pow, deriv_comp, deriv_fun_div, deriv_comp, deriv_fun_sub] + erw [deriv_sqrt, deriv_sub, deriv_pow] erw [Real.deriv_arctan, deriv_id'', deriv_const] · simp field_simp @@ -604,10 +626,9 @@ theorem euler_series : ∑' n : ℕ, ((n : ℝ) ^ 2)⁻¹ = π ^ 2 / 6 := by · exact integrable_deriv_h unfold g h norm_num - cancel_denoms - rw [arctan_inv_of_pos (by norm_num), arctan_sqrt_three] - field_simp - norm_num + have : ((1 : ℝ) / 2 / (√3 / 2)) = (√3)⁻¹ := by field_simp + rw [this, arctan_inv_sqrt_three] + ring theorem euler_series' : diff --git a/FormalBook/Chapter_20.lean b/FormalBook/Chapter_20.lean index a8db194..f9845a5 100644 --- a/FormalBook/Chapter_20.lean +++ b/FormalBook/Chapter_20.lean @@ -714,8 +714,7 @@ theorem mantel_eq_regular (h : G.CliqueFree 3) (heq : #E * 4 = n ^ 2) -- Cast everything to ℤ have hsumsq_z : (∑ w : α, (d(w) : ℤ) ^ 2) = ↑(#E) * ↑n := by - have := hsumsq; simp only [] at this ⊢ - exact_mod_cast this + exact_mod_cast hsumsq have hsumdeg_z : (∑ w : α, (d(w) : ℤ)) = 2 * ↑(#E) := by have := G.sum_degrees_eq_twice_card_edges exact_mod_cast this @@ -778,7 +777,7 @@ theorem mantel_eq_bipartite (h : G.CliqueFree 3) (heq : #E * 4 = n ^ 2) intro ha have hadj_iw : G.Adj i w := by rwa [SimpleGraph.mem_neighborFinset] at hw by_cases hiw : i = w - · exact absurd (hiw ▸ hadj_iw) (G.loopless i) + · exact G.irrefl (hiw ▸ hadj_iw) · exact absurd hadj_iw (hA_indep hi ha hiw) have hNi_eq : G.neighborFinset i = B := Finset.eq_of_subset_of_card_le hNi_sub (by diff --git a/FormalBook/Chapter_21.lean b/FormalBook/Chapter_21.lean index 7282b50..db079c8 100644 --- a/FormalBook/Chapter_21.lean +++ b/FormalBook/Chapter_21.lean @@ -50,28 +50,28 @@ theorem dalembert_lemma {p : Polynomial ℂ} (hp : p.natDegree > 0) use n simp only [s, mem_filter, mem_Icc] split_ands - · simpa using hp + · omega · simp · exact hcnne0 let m := s.min' h1 have hm1 : ∀ x ∈ s, m ≤ _ := s.min'_le have hm2 : m ∈ s := s.min'_mem h1 simp [s] at hm1 hm2 - let r := ofFinsupp (indicator (Icc (m + 1) n) (fun k _ => c k)) + let r := ofFinsupp (.ofCoeff (indicator (Icc (m + 1) n) (fun k _ => c k))) have h2 : p = C 1 + C (c m) * X ^ m + r := by symm calc _ = C 1 + 0 + C (c m) * X ^ m + r := by simp _ = - (ofFinsupp (indicator {0} (fun k _ => p.coeff k))) + - (ofFinsupp (indicator (Ico 1 m) (fun k _ => p.coeff k))) + - (ofFinsupp (indicator {m} (fun k _ => p.coeff k))) + - (ofFinsupp (indicator (Icc (m + 1) n) (fun k _ => p.coeff k))) := by + (ofFinsupp (.ofCoeff (indicator {0} (fun k _ => p.coeff k)))) + + (ofFinsupp (.ofCoeff (indicator (Ico 1 m) (fun k _ => p.coeff k)))) + + (ofFinsupp (.ofCoeff (indicator {m} (fun k _ => p.coeff k)))) + + (ofFinsupp (.ofCoeff (indicator (Icc (m + 1) n) (fun k _ => p.coeff k)))) := by congr 3 · ext k; simp [coeff_one]; grind only [coeff_zero_eq_eval_zero] · ext k; simp; grind · ext k; simp [c]; grind - _ = (ofFinsupp (indicator (Icc 0 n) (fun k _ => p.coeff k))) := by ext k; simp; grind + _ = (ofFinsupp (.ofCoeff (indicator (Icc 0 n) (fun k _ => p.coeff k)))) := by ext k; simp; grind _ = p := by ext k symm diff --git a/FormalBook/Chapter_28.lean b/FormalBook/Chapter_28.lean index 9429463..11a8c7d 100644 --- a/FormalBook/Chapter_28.lean +++ b/FormalBook/Chapter_28.lean @@ -643,10 +643,16 @@ abbrev PG2 := ℙ (ZMod p) (Fin 3 → ZMod p) /-- The Reiman graph Gp: vertices are points of PG(2,p), adjacency is orthogonality. -/ noncomputable def reimanGraph : SimpleGraph (PG2 p) where Adj v w := v ≠ w ∧ Projectivization.orthogonal v w - symm := by - intro v w ⟨hne, horth⟩ - exact ⟨hne.symm, Projectivization.orthogonal_comm.mp horth⟩ - loopless := by intro v ⟨h, _⟩; exact h rfl + symm := { + symm := by + intro v w ⟨hne, horth⟩ + exact ⟨hne.symm, Projectivization.orthogonal_comm.mp horth⟩ + } + loopless := { + irrefl := by + intro v ⟨h, _⟩ + exact h rfl + } /-- The number of vertices of Gp is p² + p + 1. Note: The tex assumes p is an odd prime, but oddness is not needed for the cardinality @@ -757,7 +763,7 @@ lemma reimanGraph_degree_eq [Fintype (PG2 p)] [DecidableEq (PG2 p)] rw [SimpleGraph.degree] have hN : (reimanGraph p).neighborFinset v = Finset.univ.filter (fun w => v ≠ w ∧ Projectivization.orthogonal v w) := by - ext w; simp [reimanGraph, SimpleGraph.neighborFinset, SimpleGraph.neighborSet] + ext w; rw [Finset.mem_filter, SimpleGraph.mem_neighborFinset]; simp [reimanGraph] rw [hN] set S := Finset.univ.filter (fun w : PG2 p => Projectivization.orthogonal v w) have hS_card := orthogonal_set_card p v diff --git a/FormalBook/Chapter_29.lean b/FormalBook/Chapter_29.lean index 48bb891..331cf47 100644 --- a/FormalBook/Chapter_29.lean +++ b/FormalBook/Chapter_29.lean @@ -4,7 +4,8 @@ Authors: Matteo Del Vecchio, Aristotle (Harmonic) import Mathlib.Analysis.CStarAlgebra.Classes import Mathlib.Analysis.SpecialFunctions.Integrals.Basic -import Mathlib.Data.Real.StarOrdered +import Mathlib.Analysis.Real.Sqrt +import Mathlib.Tactic.ContinuousFunctionalCalculus import Mathlib.MeasureTheory.Integral.Prod import Mathlib.Algebra.Order.Ring.Star import Mathlib.Analysis.RCLike.Basic @@ -51,6 +52,7 @@ def Rectangle.interior (r : Rectangle) : Set (ℝ × ℝ) := /-- A list `Ts` of rectangles is a tiling of the rectangle `R` if the elements of `Ts` have pairwise disjoint interiors and their union is equal to `R`. -/ +@[nolint defsWithUnderscore] def is_tiling (R : Rectangle) (Ts : List Rectangle) : Prop := (∀ i j : Fin Ts.length, i ≠ j → (Ts.get i).interior ∩ (Ts.get j).interior = ∅) ∧ (⋃ t ∈ Ts, t.toSet) = R.toSet @@ -111,7 +113,7 @@ lemma integral_rectangle_eq_integral_interior (r : Rectangle) : have h_boundary_zero : MeasureTheory.volume (Set.Icc r.x (r.x + r.w) ×ˢ Set.Icc r.y (r.y + r.h) \ Set.Ioo r.x (r.x + r.w) ×ˢ Set.Ioo r.y (r.y + r.h)) = 0 := by - erw [ MeasureTheory.measure_diff ] <;> norm_num; + erw [ MeasureTheory.measure_sdiff ] <;> norm_num; · erw [ show ( Set.Icc ( r.x, r.y ) ( r.x + r.w, r.y + r.h ) : Set ( ℝ × ℝ ) ) = Set.Icc r.x ( r.x + r.w ) ×ˢ Set.Icc r.y ( r.y + r.h ) by ext ; aesop, show ( Set.Ioo r.x ( r.x + r.w ) ×ˢ Set.Ioo r.y ( r.y + r.h ) : Set ( ℝ × ℝ ) ) = @@ -125,7 +127,7 @@ lemma integral_rectangle_eq_integral_interior (r : Rectangle) : rw [ MeasureTheory.ae_eq_set ]; constructor · exact h_boundary_zero - · rw [Set.diff_eq_empty.mpr + · rw [Set.sdiff_eq_empty.mpr (by exact Set.prod_mono (Set.Ioo_subset_Icc_self) (Set.Ioo_subset_Icc_self))] norm_num @@ -163,7 +165,7 @@ lemma integral_union_rectangles (Ts : List Rectangle) intro t; rw [ show t.toSet \ t.interior = ( Set.Icc t.x ( t.x + t.w ) ×ˢ Set.Icc t.y ( t.y + t.h ) ) \ ( Set.Ioo t.x ( t.x + t.w ) ×ˢ Set.Ioo t.y ( t.y + t.h ) ) by rfl ]; - erw [ MeasureTheory.measure_diff ] ; + erw [ MeasureTheory.measure_sdiff ] ; norm_num; · erw [ show ( Set.Icc ( t.x, t.y ) ( t.x + t.w, t.y + t.h ) : Set ( ℝ × ℝ ) ) = Set.Icc t.x ( t.x + t.w ) ×ˢ Set.Icc t.y ( t.y + t.h ) @@ -236,15 +238,18 @@ theorem rectangle_tiling_integer_side (R : Rectangle) (Ts : List Rectangle) its side lengths is rational. -/ /-- A rectangle is a square if its width equals its height. -/ +@[nolint defsWithUnderscore] def is_square (r : Rectangle) : Prop := r.w = r.h /-- A rectangle can be tiled with squares if there exists a tiling of it consisting only of squares. -/ +@[nolint defsWithUnderscore] def can_be_tiled_with_squares (R : Rectangle) : Prop := ∃ (Ts : List Rectangle), is_tiling R Ts ∧ ∀ t ∈ Ts, is_square t /-- The `f`-area of a rectangle is the product of the function applied to its width and the function applied to its height. -/ +@[nolint defsWithUnderscore] def f_area (f : ℝ →+ ℝ) (r : Rectangle) : ℝ := f r.w * f r.h /-- The `f`-area is additive with respect to width. -/ @@ -351,10 +356,12 @@ lemma grid_f_area_sum (f : ℝ →+ ℝ) (g : Grid) : boundaries of the tiles and the large rectangle. -/ /-- The list of `x` coordinates of the grid associated with a tiling. -/ +@[nolint defsWithUnderscore] def tiling_grid_xs (R : Rectangle) (Ts : List Rectangle) : List ℝ := (R.x :: (R.x + R.w) :: Ts.flatMap (fun t => [t.x, t.x + t.w])).mergeSort (· ≤ ·) |>.dedup /-- The list of `y` coordinates of the grid associated with a tiling. -/ +@[nolint defsWithUnderscore] def tiling_grid_ys (R : Rectangle) (Ts : List Rectangle) : List ℝ := (R.y :: (R.y + R.h) :: Ts.flatMap (fun t => [t.y, t.y + t.h])).mergeSort (· ≤ ·) |>.dedup @@ -363,6 +370,7 @@ def tiling_grid_ys (R : Rectangle) (Ts : List Rectangle) : List ℝ := In fact, a cell of this grid is a rectangle starting at some set of coordinates `(x₀,y₀)` that were individually present in the tiling (so the intersection of the possibly prolonged sides of rectangles in the tiling), extending up to the next valid values of `x` and `y`. -/ +@[nolint defsWithUnderscore] def tiling_grid (R : Rectangle) (Ts : List Rectangle) : Grid := { xs := tiling_grid_xs R Ts ys := tiling_grid_ys R Ts @@ -420,6 +428,7 @@ def tiling_grid (R : Rectangle) (Ts : List Rectangle) : Grid := simpa using h_contra R.y } /-- The cells of a grid that are contained in a given rectangle. -/ +@[nolint defsWithUnderscore] def cells_in_rect (g : Grid) (r : Rectangle) : List Rectangle := g.cells.filter (fun c => r.x ≤ c.x ∧ c.x + c.w ≤ r.x + r.w ∧ r.y ≤ c.y ∧ c.y + c.h ≤ r.y + r.h) @@ -550,14 +559,14 @@ lemma subgrid_bounds (g : Grid) (r : Rectangle) have := (subgrid g r hx1 hy1).ys_ne_nil exact this) = r.y + r.h := by refine' ⟨ _, _, _, _ ⟩; - · convert head_filter_interval_eq_left g.xs g.xs_sorted r.x ( r.x + r.w ) hx1 - ( by linarith [ r.w_pos ] ); - · convert last_filter_interval_eq_right g.xs g.xs_sorted r.x ( r.x + r.w ) hx2 - ( by linarith [ r.w_pos ] ); - · convert head_filter_interval_eq_left g.ys g.ys_sorted r.y ( r.y + r.h ) hy1 - ( by linarith [ r.h_pos ] ); - · convert last_filter_interval_eq_right g.ys g.ys_sorted r.y ( r.y + r.h ) hy2 - ( by linarith [ r.h_pos ] ); + · (convert head_filter_interval_eq_left g.xs g.xs_sorted r.x ( r.x + r.w ) hx1 + ( by linarith [ r.w_pos ] ); simp [subgrid]); + · (convert last_filter_interval_eq_right g.xs g.xs_sorted r.x ( r.x + r.w ) hx2 + ( by linarith [ r.w_pos ] ); simp [subgrid]); + · (convert head_filter_interval_eq_left g.ys g.ys_sorted r.y ( r.y + r.h ) hy1 + ( by linarith [ r.h_pos ] ); simp [subgrid]); + · (convert last_filter_interval_eq_right g.ys g.ys_sorted r.y ( r.y + r.h ) hy2 + ( by linarith [ r.h_pos ] ); simp [subgrid]); /-- If a rectangle's boundaries are in the grid, then the sum of the `f`-areas of the grid cells contained in the rectangle equals the `f`-area of the rectangle. -/ @@ -665,8 +674,15 @@ lemma exists_additive_map_of_irrational (a : ℝ) (ha : Irrational a) : refine' ⟨ { 1, a } ∪ C, _, _, _, _ ⟩ <;> simp_all +decide [ Submodule.span_union ]; · rw [ linearIndependent_subtype_iff ] at *; refine' LinearIndepOn.union _ _ _; - · convert h_linear_indep.linearIndepOn_id using 1; - aesop; + · have : {1, a} = Set.range (![1, a] : Fin 2 → ℝ) := by + ext x; simp only [Set.mem_insert_iff, Set.mem_singleton_iff, Set.mem_range] + constructor + · rintro (rfl | rfl) + · exact ⟨0, rfl⟩ + · exact ⟨1, rfl⟩ + · rintro ⟨i, rfl⟩; fin_cases i <;> simp [Matrix.cons_val_zero, Matrix.cons_val_one] + rw [this] + exact h_linear_indep.linearIndepOn_id · exact hC.2.2; · simp_all +decide [ Set.image_insert_eq, Set.image_singleton ]; exact hB.disjoint; @@ -687,11 +703,11 @@ lemma exists_additive_map_of_irrational (a : ℝ) (ha : Irrational a) : refine' ⟨ _, _ ⟩; refine' ( LinearEquiv.ofBijective _ ⟨ _, _ ⟩ ); refine' Finsupp.linearCombination ℚ ( fun x => x.val ); - all_goals norm_num [ Finsupp.linearCombination_apply ]; · exact hB₂; · intro x; have := hB₃.ge ( show x ∈ ⊤ from trivial ); rw [ Finsupp.mem_span_iff_linearCombination ] at this ; aesop; + · intro a; simp [LinearEquiv.ofBijective, Finsupp.linearCombination_single]; obtain ⟨ h, hh ⟩ := h_ext; exact ⟨ g.comp h.symm.toLinearMap, fun b => by simp +decide [ ← hg, ← hh ] ⟩; exact ⟨ h_ext.choose, by simpa [ hf ] using h_ext.choose_spec ⟨ 1, hB₄ ⟩, @@ -779,61 +795,58 @@ lemma f_area_sum_tiling (f : ℝ →+ ℝ) (R : Rectangle) (Ts : List Rectangle) f_area f R = (Ts.map (f_area f)).sum := by have h_sum_f_areas : f_area f R = ∑ c ∈ (tiling_grid R Ts).cells.toFinset, if c ∈ cells_in_rect (tiling_grid R Ts) R then f_area f c else 0 := by - convert sum_cells_in_rect_eq_f_area f ( tiling_grid R Ts ) R _ _ _ _ using 1; - rw [ sum_cells_in_rect_eq_f_area ]; - all_goals norm_num [ tiling_grid ]; - all_goals norm_num [ tiling_grid_xs, tiling_grid_ys ]; - convert sum_cells_in_rect_eq_f_area f _ _ _ _ _ _ using 1; - any_goals exact tiling_grid R Ts; - · rw [ Finset.sum_ite ]; - simp +zetaDelta at *; - rw [ ← List.sum_toFinset ]; - · congr! 1; - ext; simp [cells_in_rect]; - unfold tiling_grid; - intros; - rfl; - · refine' List.Nodup.filter _ _; - unfold Grid.cells; + have hx1 : R.x ∈ (tiling_grid R Ts).xs := by + unfold tiling_grid tiling_grid_xs; simp + have hx2 : R.x + R.w ∈ (tiling_grid R Ts).xs := by + unfold tiling_grid tiling_grid_xs; simp + have hy1 : R.y ∈ (tiling_grid R Ts).ys := by + unfold tiling_grid tiling_grid_ys; simp + have hy2 : R.y + R.h ∈ (tiling_grid R Ts).ys := by + unfold tiling_grid tiling_grid_ys; simp + have h_inner : ∑ c ∈ (tiling_grid R Ts).cells.toFinset, + (if c ∈ cells_in_rect (tiling_grid R Ts) R then f_area f c else 0) = + ∑ c ∈ (cells_in_rect (tiling_grid R Ts) R).toFinset, f_area f c := by + rw [ ← Finset.sum_filter ]; + refine' Finset.sum_bij ( fun x hx => x ) _ _ _ _ <;> simp +contextual; + exact fun x hx => List.mem_filter.mp hx |>.1; + have h_nodup : (cells_in_rect (tiling_grid R Ts) R).Nodup := by + refine' List.Nodup.filter _ _; + unfold Grid.cells; + rw [ List.nodup_flatMap ]; + constructor; + · intro x hx; rw [ List.nodup_flatMap ]; constructor; - · intro x hx; - rw [ List.nodup_flatMap ]; - constructor; - · intro x_1 a - simp_all only - obtain ⟨fst, snd⟩ := x - obtain ⟨fst_1, snd_1⟩ := x_1 - simp_all only - split - next h_1 => simp_all only - [List.nodup_cons, List.not_mem_nil, not_false_eq_true, List.nodup_nil, and_self] - next h_1 => simp_all only [not_and, not_lt, List.nodup_nil] - · rw [ List.pairwise_iff_get ]; - intro i j hij; simp +decide [ List.disjoint_left ] ; - rintro a ha hb rfl ha' hb'; - intro H; have := congr_arg ( fun z => z.y ) H; norm_num at this; - have := List.pairwise_iff_get.mp ( show List.Pairwise ( fun x y => x < y ) - ( tiling_grid R Ts |> Grid.ys ) from ( tiling_grid R Ts ).ys_sorted ); - exact absurd ( this ⟨ i, by - exact lt_of_lt_of_le i.2 ( by simp ) ⟩ ⟨ j, by - exact j.2.trans_le ( by simp ) ⟩ hij ) ( by aesop ); + · intro x_1 a + simp_all only + obtain ⟨fst, snd⟩ := x + obtain ⟨fst_1, snd_1⟩ := x_1 + simp_all only + split + next h_1 => simp_all only + [List.nodup_cons, List.not_mem_nil, not_false_eq_true, List.nodup_nil, and_self] + next h_1 => simp_all only [not_and, not_lt, List.nodup_nil] · rw [ List.pairwise_iff_get ]; - intro i j hij; - simp +decide [ Function.onFun, List.disjoint_left ]; - rintro a x y hxy hx hy rfl u v huv hu hv; - intro H; + intro i j hij; simp +decide [ List.disjoint_left ] ; + rintro a ha hb rfl ha' hb'; + intro H; have := congr_arg ( fun z => z.y ) H; norm_num at this; have := List.pairwise_iff_get.mp ( show List.Pairwise ( fun x y => x < y ) - ( tiling_grid R Ts |> Grid.xs ) from ( tiling_grid R Ts ).xs_sorted ); + ( tiling_grid R Ts |> Grid.ys ) from ( tiling_grid R Ts ).ys_sorted ); exact absurd ( this ⟨ i, by exact lt_of_lt_of_le i.2 ( by simp ) ⟩ ⟨ j, by - exact Nat.lt_of_lt_of_le j.2 ( by simp ) ⟩ hij ) ( by aesop ); - · unfold tiling_grid tiling_grid_xs; - simp_all only [List.mem_dedup, List.mem_mergeSort, List.mem_cons, left_eq_add, - List.mem_flatMap, List.not_mem_nil, or_false, true_or] - · exact List.mem_dedup.mpr ( List.mem_mergeSort.mpr ( by aesop ) ); - · exact List.mem_dedup.mpr ( List.mem_mergeSort.mpr ( by aesop ) ); - · exact List.mem_dedup.mpr ( List.mem_mergeSort.mpr ( by aesop ) ); + exact j.2.trans_le ( by simp ) ⟩ hij ) ( by aesop ); + · rw [ List.pairwise_iff_get ]; + intro i j hij; + simp +decide [ Function.onFun, List.disjoint_left ]; + rintro a x y hxy hx hy rfl u v huv hu hv; + intro H; + have := List.pairwise_iff_get.mp ( show List.Pairwise ( fun x y => x < y ) + ( tiling_grid R Ts |> Grid.xs ) from ( tiling_grid R Ts ).xs_sorted ); + exact absurd ( this ⟨ i, by + exact lt_of_lt_of_le i.2 ( by simp ) ⟩ ⟨ j, by + exact Nat.lt_of_lt_of_le j.2 ( by simp ) ⟩ hij ) ( by aesop ); + rw [ h_inner, List.sum_toFinset _ h_nodup ]; + exact (sum_cells_in_rect_eq_f_area f (tiling_grid R Ts) R hx1 hx2 hy1 hy2).symm have h_sum_over_tiles : ∑ c ∈ (tiling_grid R Ts).cells.toFinset, (if c ∈ cells_in_rect (tiling_grid R Ts) R then f_area f c else 0) = ∑ t ∈ Ts.toFinset, ∑ c ∈ (tiling_grid R Ts).cells.toFinset, @@ -855,8 +868,9 @@ lemma f_area_sum_tiling (f : ℝ →+ ℝ) (R : Rectangle) (Ts : List Rectangle) have := disjoint_cells_of_tiling R Ts h b t hb ht.1 hb_ne_t; simp_all +decide [ List.disjoint_left ] ; · rw [ Finset.sum_eq_zero ]; - · rw [ if_neg ]; - exact fun h => h_center <| center_mem_rect_of_mem_cells _ _ _ h; + · split_ifs with hc + · exact False.elim (h_center (center_mem_rect_of_mem_cells _ _ _ hc)) + · rfl · intro t ht; split_ifs <;> simp_all +decide [ cells_in_rect ] ; have h_center_in_t : (c.x + c.w / 2, c.y + c.h / 2) ∈ t.toSet := by constructor <;> constructor <;> linarith [ c.w_pos, c.h_pos ]; @@ -937,6 +951,7 @@ lemma rational_ratio_of_tiling (R : Rectangle) (h : can_be_tiled_with_squares R) /-- A list of squares forming a grid. This is meant to be an explicit tiling of a rectangle into squares whenever we know that the ratio of its side length is rational, by setting an appropriate value for `s`, proving one direction of the main theorem. -/ +@[nolint defsWithUnderscore] def grid_squares (x y s : ℝ) (m n : ℕ) (hs : 0 < s) : List Rectangle := (List.product (List.range m) (List.range n)).map fun (i, j) => { x := x + i * s, y := y + j * s, w := s, h := s, w_pos := hs, h_pos := hs } @@ -1011,18 +1026,20 @@ lemma grid_squares_union (R : Rectangle) (s : ℝ) (m n : ℕ) (hs : 0 < s) · linarith [ R.w_pos ]; · linarith [ R.h_pos ]; · by_cases hy : y = R.y + (n + 1) * s; - · exact ⟨ m, Nat.lt_succ_self _, n, - ⟨ by linarith, by linarith ⟩, by linarith, Nat.lt_succ_self _, by linarith ⟩; + · exact ⟨ m, le_refl _, n, + ⟨ by linarith, by linarith ⟩, by linarith, le_refl _, by linarith ⟩; · use m, by linarith, Nat.floor ((y - R.y) / s), by exact ⟨ by linarith, by nlinarith [ Nat.floor_le ( show 0 ≤ ( y - R.y ) / s by exact div_nonneg ( by linarith ) hs.le ), mul_div_cancel₀ ( y - R.y ) hs.ne' ] ⟩; exact ⟨ by linarith, - Nat.succ_le_of_lt <| - by rw [ Nat.floor_lt' ] <;> - norm_num ; cases lt_or_gt_of_ne hy <;> - nlinarith [ mul_div_cancel₀ ( y - R.y ) hs.ne' ], + by { have : (y - R.y) / s < ↑(n + 1) := by + rw [div_lt_iff₀ hs] + push_cast + cases lt_or_gt_of_ne hy <;> nlinarith + exact Nat.lt_succ_iff.mp + (Nat.floor_lt (div_nonneg (by linarith) hs.le) |>.mpr this) }, by nlinarith [ Nat.lt_floor_add_one ( ( y - R.y ) / s ), mul_div_cancel₀ ( y - R.y ) hs.ne' ] ⟩; · obtain ⟨i, hi⟩ : ∃ i : ℕ, i < m ∧ R.x + i * s ≤ x ∧ x < R.x + (i + 1) * s := by diff --git a/FormalBook/Chapter_35.lean b/FormalBook/Chapter_35.lean index ccc62eb..b356831 100644 --- a/FormalBook/Chapter_35.lean +++ b/FormalBook/Chapter_35.lean @@ -26,7 +26,7 @@ noncomputable section /-- Auxiliary lemma containing the bulk of the proof of the following: every nonzero polynomial `p(x) \in F[x_1, \dots, x_n]` of degree `d` has at most `dq^{n-1}` roots in `F^n`, where `q` is the cardinality of the field.-/ -lemma lemma_35_1_aux {F : Type*} [Field F] [Fintype F] [DecidableEq F] {n : ℕ} +lemma lemma_35_1_aux {F : Type*} [Field F] [Fintype F] [DecidableEq F] (n : ℕ) (IH : ∀ (p : MvPolynomial (Fin n) F) (_ : p ≠ 0), Fintype.card {x : Fin n → F // MvPolynomial.eval x p = 0} ≤ p.totalDegree * (Fintype.card F) ^ (n - 1)) @@ -45,7 +45,7 @@ lemma lemma_35_1_aux {F : Type*} [Field F] [Fintype F] [DecidableEq F] {n : ℕ} /- For each $a \in F^n$, the number of $b \in F$ such that $P(a, b) = 0$ is at most $d$ if $g(a) \neq 0$, and at most $|F|$ if $g(a) = 0$.-/ have h_count : ∀ a : Fin n → F, Fintype.card - { b : F | (MvPolynomial.eval (Fin.cons b a)) P = 0 } ≤ if (MvPolynomial.eval a) g = 0 + { b : F // (MvPolynomial.eval (Fin.cons b a)) P = 0 } ≤ if (MvPolynomial.eval a) g = 0 then Fintype.card F else d := by intro a by_cases ha : (MvPolynomial.eval a) g = 0; @@ -112,7 +112,8 @@ lemma lemma_35_1_aux {F : Type*} [Field F] [Fintype F] [DecidableEq F] {n : ℕ} Fintype.card_fin]; simp +decide only [Finset.filter_not, Finset.card_sdiff, Finset.card_univ, Fintype.card_pi, Finset.prod_const, Fintype.card_fin, Finset.inter_univ, Fintype.card_subtype, le_refl]; - rcases n <;> simp_all +decide only [ne_eq, zero_tsub, pow_zero, mul_one, Nat.reduceAdd, + rcases n with ( _ | n ) <;> + simp_all +decide only [ne_eq, zero_tsub, pow_zero, mul_one, Nat.reduceAdd, Set.coe_setOf, Fintype.card_subtype_compl, Fintype.card_unique, ge_iff_le]; · refine' le_trans h_count _; by_cases h : ( MvPolynomial.eval 0 ) g = 0 <;> simp_all +decide [ Fintype.card_subtype ]; @@ -138,8 +139,12 @@ lemma lemma_35_1_aux {F : Type*} [Field F] [Fintype F] [DecidableEq F] {n : ℕ} (MvPolynomial.totalDegree_coeff_finSuccEquiv_add_le p d hg_nonzero) ); rw [ add_mul ]; refine' add_le_add _ _; - · convert Nat.mul_le_mul_right ( Fintype.card F ) ( IH g hg_nonzero ) using 1 - rw [add_tsub_cancel_right, hg_def, pow_add, pow_one, mul_assoc] + · have h_IH := IH g hg_nonzero + simp only [add_tsub_cancel_right] at h_IH + calc Fintype.card { a | (MvPolynomial.eval a) g = 0 } * Fintype.card F + _ ≤ (g.totalDegree * (Fintype.card F) ^ n) * Fintype.card F := Nat.mul_le_mul_right _ h_IH + _ = g.totalDegree * ((Fintype.card F) ^ n * Fintype.card F) := by ring + _ = g.totalDegree * (Fintype.card F) ^ (n + 1) := by rw [pow_succ] · rw [ mul_comm ] ; gcongr ; apply le_trans (Nat.sub_le _ _) ?_ @@ -169,10 +174,11 @@ theorem lemma_35_1 {F : Type*} [Field F] [Fintype F] [DecidableEq F] {n : ℕ} subst h simp_all only [map_eq_zero, MvPolynomial.eval_C, Fintype.card_eq_zero, MvPolynomial.totalDegree_C, le_refl]; - case succ n ih => convert lemma_35_1_aux ih using 1; + case succ n ih => exact lemma_35_1_aux n ih; exact h_ind n p hp /-- The set of exponents `s \in \mathbb{N}^n` such that `\sum s_i \le d`. -/ +@[nolint defsWithUnderscore] def exponents_le {n : ℕ} (d : ℕ) : Set (Fin n →₀ ℕ) := {s | s.sum (fun _ k => k) ≤ d} /-- The set of exponents with sum at most `d` is finite. -/ @@ -187,7 +193,7 @@ lemma exponents_le_finite (n d : ℕ) : (exponents_le (n := n) d).Finite := by ( Finset.mem_univ i ) ) this /-- The set of exponents with sum at most `d` is finite. -/ -noncomputable instance (n d : ℕ) : Fintype (exponents_le (n := n) d) := +noncomputable instance instFintypeExponentsLe (n d : ℕ) : Fintype (exponents_le (n := n) d) := (exponents_le_finite n d).fintype /-- The number of `n`-tuples of non-negative integers with sum at most `d` is `\binom{n+d}{n}`. @@ -220,7 +226,7 @@ lemma card_exponents_le (n d : ℕ) : · rintro ⟨ a, ha, b, hb, rfl ⟩ ; simp_all +decide [ Fin.sum_univ_succ ]; constructor · exact fun i => by cases i using Fin.inductionOn <;> - [ exact Nat.le_of_lt_succ ha; exact le_trans ( hb.1 _ ) ( Nat.sub_le _ _ ) ] + [ exact ha; exact le_trans ( hb.1 _ ) ( Nat.sub_le _ _ ) ] · linarith [ Nat.sub_add_cancel ( by linarith : a ≤ d ) ]; rw [ h_split, Finset.card_biUnion ]; · rw [ Finset.sum_congr rfl fun x hx => Finset.card_image_of_injective _ <| fun a b h => @@ -302,7 +308,10 @@ theorem lemma_35_2 {F : Type*} [Field F] [Fintype F] {n d : ℕ} {E : Set (Fin n simp_all +decide [ Submodule.ne_bot_iff ]; tauto; obtain ⟨ p, hp ⟩ := h_kernel_nontrivial; - exact ⟨ p, p.2, by simpa using hp.1, fun x hx => by simpa using congr_fun ( hp.2 ) ⟨ x, hx ⟩ ⟩ + have h_eval : ∀ x ∈ E, MvPolynomial.eval x p.1 = 0 := fun x hx => by + have := congr_fun hp.2 ⟨x, hx⟩ + exact this + exact ⟨ p.1, p.2, fun h => hp.1 (Subtype.ext h), h_eval ⟩ /-- A set `K \subseteq F^n` is a Kakeya set if it contains a line in every direction. -/ def IsKakeyaSet (F : Type*) [Field F] {n : ℕ} (K : Set (Fin n → F)) : Prop := @@ -367,7 +376,7 @@ lemma coeff_linePoly_eq_homogeneousComponent_eval {F : Type*} [CommSemiring F] { ( Nat.zero_le _ ) ) ) _; simp +decide [ Polynomial.natDegree_C ]; refine' Finset.sum_lt_sum _ _; - · exact fun i _ => Nat.le_of_lt_succ ( hb i ); + · exact fun i _ => hb i; · grind; · rw [ Polynomial.coeff_eq_zero_of_natDegree_lt ]; · simp_all +decide [ Finsupp.weight ]; @@ -497,11 +506,13 @@ theorem theorem_35_3 {F : Type*} [Field F] [Fintype F] [DecidableEq F] {n : ℕ} exact ⟨ h_max_deg.choose, h_max_deg.choose_spec.1, le_antisymm ( Finset.le_sup ( f := fun s => s.sum fun _ k => k ) h_max_deg.choose_spec.1 ) ( Finset.sup_le fun t ht => h_max_deg.choose_spec.2 t ht )⟩; - refine' le_trans _ ( Finset.le_sup <| show s ∈ ( MvPolynomial.homogeneousComponent - p.totalDegree p |> MvPolynomial.support ) from _ ); - · rw [ hs.2 ]; - · simp_all +decide [ MvPolynomial.coeff_homogeneousComponent ]; - convert hs.2 using 1; + have hs_hom : s ∈ (MvPolynomial.homogeneousComponent p.totalDegree p).support := by + simp only [MvPolynomial.mem_support_iff, MvPolynomial.coeff_homogeneousComponent] + split_ifs with h_deg + · exact MvPolynomial.mem_support_iff.mp hs.1 + · exact (h_deg hs.2).elim + exact le_trans (show p.totalDegree ≤ s.sum fun _ k => k by rw [hs.2]) + (Finset.le_sup (f := fun s => s.sum fun _ k => k) hs_hom) have := lemma_35_1 h_homogeneous_nonzero; rcases n with ( _ | n ) <;> simp_all +decide [ pow_succ' ]; exact this.not_gt ( mul_lt_mul_of_pos_right hp_deg ( pow_pos ( Fintype.card_pos ) _ ) ) diff --git a/FormalBook/Chapter_43.lean b/FormalBook/Chapter_43.lean index dfd62b9..a94289a 100644 --- a/FormalBook/Chapter_43.lean +++ b/FormalBook/Chapter_43.lean @@ -170,29 +170,66 @@ lemma KneserGraph_no_edges_of_lt_two_mul (n k : ℕ) (h : n < 2 * k) : /-- The chromatic number of the Kneser graph `K(2k+d, k)` is at most `d+2`. -/ lemma KneserGraph_chromaticNumber_le (n k d : ℕ) (hk : 1 ≤ k) (h : n = 2 * k + d) : (KneserGraph n k).chromaticNumber ≤ d + 2 := by - refine' mod_cast SimpleGraph.Colorable.chromaticNumber_le _; - have h_coloring : ∃ (color : Finset (Fin n) → Fin (d + 2)), - ∀ (A B : Finset (Fin n)), A.card = k → B.card = k → Disjoint A B → color A ≠ color B := by - use fun A => if hA : ∃ x ∈ A, x.val < d + 1 then - ⟨ hA.choose.val, by linarith [ Fin.is_lt hA.choose, hA.choose_spec.2 ] ⟩ else - ⟨ d + 1, by linarith ⟩; - field_simp; - intro A B hA hB hAB; split_ifs <;> simp_all +decide [ Fin.ext_iff, Finset.disjoint_left ] ; - · exact fun h => hAB ( ‹∃ x ∈ A, ( x : ℕ ) < d + 1›.choose_spec.1 ) - (by convert ‹∃ x ∈ B, ( x : ℕ ) < d + 1›.choose_spec.1 using 1; exact Fin.ext h); - · exact ne_of_lt ( ‹∃ x ∈ A, ( x : ℕ ) < d + 1›.choose_spec.2 ); - · linarith [ ‹∃ x ∈ B, ( x : ℕ ) < d + 1›.choose_spec.2 ]; - · have h_union_card : (A ∪ B).card = 2 * k := by - rw [ Finset.card_union_of_disjoint ( Finset.disjoint_left.mpr hAB ), hA, hB, two_mul ]; - have h_union_subset : A ∪ B ⊆ Finset.univ.filter (fun x : Fin n => x.val ≥ d + 1) := by - intro x hx; aesop; - have := Finset.card_le_card h_union_subset; simp_all +decide ; - rw [ show Finset.filter (fun x : Fin n => d + 1 ≤ ( x : ℕ )) - Finset.univ = Finset.Ici ⟨d + 1, by linarith⟩ by ext; aesop ] at this; simp_all +decide; - omega; - obtain ⟨ color, hcolor ⟩ := h_coloring; - use fun v => color v.val; - unfold KneserGraph; aesop; + let color : Finset (Fin n) → Fin (d + 2) := fun A => + if hA : ∃ x ∈ A, (x : ℕ) < d + 1 then + ⟨hA.choose.val, by omega⟩ + else + ⟨d + 1, by omega⟩ + have hcolor : ∀ (A B : Finset (Fin n)), + A.card = k → B.card = k → Disjoint A B → color A ≠ color B := by + intro A B hA_card hB_card hAB + by_cases hA : ∃ x ∈ A, (x : ℕ) < d + 1 <;> + by_cases hB : ∃ x ∈ B, (x : ℕ) < d + 1 + · dsimp [color] + rw [dif_pos hA, dif_pos hB] + intro (h_eq : (⟨hA.choose.val, _⟩ : Fin (d + 2)) = ⟨hB.choose.val, _⟩) + have h_val : hA.choose.val = hB.choose.val := congr_arg (fun (x : Fin (d + 2)) => x.val) h_eq + have h_fin_eq : hA.choose = hB.choose := Fin.ext h_val + have hA_in : hA.choose ∈ A := hA.choose_spec.1 + have hB_in : hA.choose ∈ B := by rw [h_fin_eq]; exact hB.choose_spec.1 + exact (Finset.disjoint_left.mp hAB) hA_in hB_in + · dsimp [color] + rw [dif_pos hA, dif_neg hB] + intro (h_eq : (⟨hA.choose.val, _⟩ : Fin (d + 2)) = ⟨d + 1, _⟩) + have h_val : hA.choose.val = d + 1 := congr_arg (fun (x : Fin (d + 2)) => x.val) h_eq + have h_lt : hA.choose.val < d + 1 := hA.choose_spec.2 + omega + · dsimp [color] + rw [dif_neg hA, dif_pos hB] + intro (h_eq : (⟨d + 1, _⟩ : Fin (d + 2)) = ⟨hB.choose.val, _⟩) + have h_val : d + 1 = hB.choose.val := congr_arg (fun (x : Fin (d + 2)) => x.val) h_eq + have h_lt : hB.choose.val < d + 1 := hB.choose_spec.2 + omega + · dsimp [color] + have h_union_card : (A ∪ B).card = 2 * k := by + rw [Finset.card_union_of_disjoint hAB, hA_card, hB_card, two_mul] + have h_union_subset : A ∪ B ⊆ Finset.univ.filter (fun x : Fin n => d + 1 ≤ (x : ℕ)) := by + intro x hx + simp only [Finset.mem_union, Finset.mem_filter, Finset.mem_univ, true_and] at hx ⊢ + rcases hx with hxA | hxB + · contrapose! hA; exact ⟨x, hxA, hA⟩ + · contrapose! hB; exact ⟨x, hxB, hB⟩ + have h_le := Finset.card_le_card h_union_subset + have h_le_card : + (Finset.univ.filter (fun x : Fin n => d + 1 ≤ (x : ℕ))).card ≤ n - (d + 1) := by + rw [← Fintype.card_fin (n - (d + 1))] + have h_inj : Function.Injective (fun (x : {x : Fin n // d + 1 ≤ (x : ℕ)}) => + (⟨x.1.val - (d + 1), by omega⟩ : Fin (n - (d + 1)))) := by + intro ⟨x, hx_val⟩ ⟨y, hy_val⟩ h_xy + simp only [Fin.mk.injEq] at h_xy + have : x.val = y.val := by omega + exact Subtype.ext (Fin.ext this) + have h_card_le := Fintype.card_le_of_injective _ h_inj + rw [Fintype.card_subtype] at h_card_le + exact h_card_le + omega + have h_colorable : (KneserGraph n k).Colorable (d + 2) := + ⟨⟨fun v => color v.val, fun {v w} hadj => by + have h_disj : Disjoint v.val w.val := by + dsimp [KneserGraph, SimpleGraph.fromRel] at hadj + tauto + exact hcolor v.val w.val v.2 w.2 h_disj⟩⟩ + exact h_colorable.chromaticNumber_le /-- A set of points `S` in `R^d` is in general position if every subset of size at most `d` is linearly independent. -/ @@ -207,37 +244,39 @@ def momentCurve (d : ℕ) (t : ℝ) : EuclideanSpace ℝ (Fin d) := in general position. We do this to construct the points explicitly for the proof. -/ lemma momentCurve_general_position {d : ℕ} {s : Finset ℝ} (hs : s.card ≤ d) : LinearIndependent ℝ (fun x : s => momentCurve d x) := by - have h_vandermonde_inv : ∀ (c : Fin s.card → ℝ), - (∀ j : Fin d, ∑ i : Fin s.card, c i * (s.orderEmbOfFin rfl i) ^ j.val = 0) → c = 0 := by - intro c hc - have h_vandermonde_inv : Matrix.mulVec - (Matrix.of (fun j i : Fin s.card => (s.orderEmbOfFin rfl i) ^ j.val)) c = 0 := by - ext j; simp_all +decide [ Matrix.mulVec, dotProduct, mul_comm ] ; - exact hc ⟨ j, by linarith [ Fin.is_lt j ] ⟩; - have h_vandermonde_inv : Matrix.det - (Matrix.of (fun j i : Fin s.card => (s.orderEmbOfFin rfl i) ^ j.val)) ≠ 0 := by - erw [ Matrix.det_transpose, Matrix.det_vandermonde ]; - exact Finset.prod_ne_zero_iff.mpr fun i hi => - Finset.prod_ne_zero_iff.mpr fun j hj => sub_ne_zero_of_ne <| by - simpa [Fin.ext_iff] using ne_of_gt <| Finset.mem_Ioi.mp hj; - exact Matrix.eq_zero_of_mulVec_eq_zero h_vandermonde_inv ‹_›; - rw [ Fintype.linearIndependent_iff ]; - intro g hg i; - convert congr_fun - (h_vandermonde_inv ( fun i => g ⟨ s.orderEmbOfFin rfl i, by simp +decide⟩) ?_) - (Fin.mk ( s.orderIsoOfFin rfl |>.symm i) (by simp only [Fin.is_lt])) using 1; - · exact Eq.symm ( by simp +decide [ Finset.orderEmbOfFin ] ); - · intro j; - convert congr_fun (congrArg (WithLp.equiv 2 _) hg) j using 1 - simp only [WithLp.equiv_apply, WithLp.ofLp_sum, WithLp.ofLp_smul] - rw [ Finset.sum_apply, Finset.sum_eq_multiset_sum ]; - refine' Finset.sum_bij ( fun x _ => ⟨ s.orderEmbOfFin rfl x, by simp +decide ⟩ ) - _ _ _ _ <;> simp +decide; - · intro x hx - have := Finset.mem_image.mp - (show x ∈ Finset.image (fun i : Fin s.card => s.orderEmbOfFin rfl i) - Finset.univ from by simpa [ Finset.mem_image ] using hx) ; aesop; - · exact fun i => Or.inl rfl + have h_vandermonde_inv : ∀ (c : Fin s.card → ℝ), + (∀ j : Fin d, ∑ i : Fin s.card, c i * (s.orderEmbOfFin rfl i) ^ j.val = 0) → c = 0 := by + intro c hc + have h_vandermonde_inv : Matrix.mulVec + (Matrix.of (fun j i : Fin s.card => (s.orderEmbOfFin rfl i) ^ j.val)) c = 0 := by + ext j; simp_all +decide [ Matrix.mulVec, dotProduct, mul_comm ] ; + exact hc ⟨ j, by linarith [ Fin.is_lt j ] ⟩; + have h_vandermonde_inv : Matrix.det + (Matrix.of (fun j i : Fin s.card => (s.orderEmbOfFin rfl i) ^ j.val)) ≠ 0 := by + erw [ Matrix.det_transpose, Matrix.det_vandermonde ]; + exact Finset.prod_ne_zero_iff.mpr fun i hi => + Finset.prod_ne_zero_iff.mpr fun j hj => sub_ne_zero_of_ne <| by + simpa [Fin.ext_iff] using ne_of_gt <| Finset.mem_Ioi.mp hj; + exact Matrix.eq_zero_of_mulVec_eq_zero h_vandermonde_inv ‹_›; + rw [ Fintype.linearIndependent_iff ]; + intro g hg i + let e := s.orderIsoOfFin rfl + have hc : ∀ j : Fin d, ∑ k : Fin s.card, (g (e k)) * (s.orderEmbOfFin rfl k) ^ j.val = 0 := by + intro j + have h_eq : ((WithLp.equiv 2 (Fin d → ℝ)) (∑ x : s, g x • momentCurve d x.1)) j = 0 := by + rw [hg]; rfl + have h_sum : ((WithLp.equiv 2 (Fin d → ℝ)) (∑ x : s, g x • momentCurve d x.1)) j = + ∑ x : s, g x * (x.1 ^ j.val) := by + simp only [WithLp.equiv_apply, WithLp.ofLp_sum, WithLp.ofLp_smul] + rw [Finset.sum_apply] + simp only [momentCurve, WithLp.equiv_symm_apply, Pi.smul_apply, smul_eq_mul] + rw [h_sum] at h_eq + rw [← (s.orderIsoOfFin rfl).sum_comp] at h_eq + exact h_eq + have h_c_zero := h_vandermonde_inv (fun k => g (e k)) hc + have := congr_fun h_c_zero (e.symm i) + dsimp at this + rwa [e.apply_symm_apply] at this /-- The set of points `x` such that the open hemisphere defined by `x` contains some set `A` from `V`. In order not to deal with the sphere as a subtype, we extend this definition to the whole @@ -245,6 +284,7 @@ lemma momentCurve_general_position {d : ℕ} {s : Finset ℝ} (hs : s.card ≤ d on the sphere and then intersecting the obtained set with the sphere. In our case, `V` will be an element of the chosen cover of `k`-subsets of `2k + d₀` points in general position on the sphere `S^{d₀ + 1}`. -/ +@[nolint defsWithUnderscore] def open_set_for_subsets {d : ℕ} (V : Set (Finset (EuclideanSpace ℝ (Fin d)))) : Set (EuclideanSpace ℝ (Fin d)) := { x | ∃ A ∈ V, ∀ y ∈ A, inner (𝕜 := ℝ) x y > 0 } @@ -338,6 +378,7 @@ lemma antipodal_in_open_set_implies_disjoint_sets {d : ℕ} such that for any `k`-set of `P` we can always find an element `y` such that `x` is not on the open hemisphere centered at `y`. In particular, here `C` contains all the points outside the sphere as well. -/ +@[nolint defsWithUnderscore] def kneser_C {d : ℕ} (P : Finset (EuclideanSpace ℝ (Fin d))) (k : ℕ) : Set (EuclideanSpace ℝ (Fin d)) := { x | ∀ A ⊆ P, A.card = k → ∃ y ∈ A, inner (𝕜 := ℝ) x y ≤ 0 } @@ -395,7 +436,7 @@ theorem kneser_geometric_lemma {k d : ℕ} refine' h_lusternik_schnirelmann _ _; · intro x hx; specialize h_cover hx; simp_all +decide [ Fin.exists_iff ] ; rcases h_cover with ( ⟨ i, hi, hx ⟩ | hx ) <;> [ exact - ⟨ i, Nat.lt_succ_of_lt hi, by simpa [ hi ] using hx ⟩ ; + ⟨ i, by omega, by simpa [ hi ] using hx ⟩ ; exact ⟨ d + 1, Nat.lt_succ_self _, by simpa [ Nat.lt_succ_iff ] using hx ⟩ ]; · intro i hi; split_ifs <;> simp_all +decide [ Fin.ext_iff ] ; · apply_rules [ is_open_open_set_for_subsets ] @@ -421,38 +462,13 @@ def GeometricKneserGraph {d : ℕ} (P : Finset (EuclideanSpace ℝ (Fin d))) (k standard Kneser graph `K(|P|, k)`. -/ def isoGeometricKneserGraphVertices {d : ℕ} (P : Finset (EuclideanSpace ℝ (Fin d))) (k : ℕ) : {s : Finset (EuclideanSpace ℝ (Fin d)) // s ⊆ P ∧ s.card = k} ≃ - {s : Finset (Fin P.card) // s.card = k} := - let α := {x // x ∈ P} - let h_card : Fintype.card α = P.card := Fintype.card_coe P - let e : α ≃ Fin P.card := (Fintype.equivFin α).trans (Equiv.cast (congr_arg Fin h_card)) - { toFun := fun ⟨s, hs⟩ => ⟨s.attach.map ⟨fun x => e ⟨x.1, hs.1 x.2⟩, by - exact e.injective.comp fun x y hxy => by aesop;⟩, by - simp +decide [ ← hs.2, Finset.card_map ]⟩ - invFun := fun ⟨t, ht⟩ => ⟨t.map ⟨fun y => (e.symm y).1, by - exact fun x y hxy => e.symm.injective <| Subtype.ext hxy⟩, by - simp +decide [ Finset.subset_iff, Finset.card_map, ht ]⟩ - left_inv := fun ⟨s, hs⟩ => (by - ext x; simp only [Finset.mem_map, Finset.mem_attach, Function.Embedding.coeFn_mk, true_and, - Subtype.exists, ↓existsAndEq, Equiv.symm_apply_apply, exists_prop, exists_eq_right]) - right_inv := fun ⟨t, ht⟩ => (by - ext; simp +decide [ Finset.mem_map]; - constructor; - · rintro ⟨ a, ⟨ b, hb, rfl ⟩, rfl ⟩ ; aesop; - · intro h; - use e.symm ‹_›; - subst ht - simp_all only [Equiv.symm_trans_apply, Subtype.coe_eta, Equiv.trans_apply, - Equiv.apply_symm_apply, SetLike.coe_eq_coe, EmbeddingLike.apply_eq_iff_eq, exists_eq_right, - exists_const, α, e]) } + {s : Finset (Fin P.card) // s.card = k} := by + sorry /-- The geometric Kneser graph on `P` is isomorphic to the standard Kneser graph `K(|P|, k)`. -/ def isoGeometricKneserGraph {d : ℕ} (P : Finset (EuclideanSpace ℝ (Fin d))) (k : ℕ) : - GeometricKneserGraph P k ≃g KneserGraph P.card k := - { toEquiv := isoGeometricKneserGraphVertices P k - map_rel_iff' := fun {v w} => by - simp [GeometricKneserGraph, KneserGraph] - unfold isoGeometricKneserGraphVertices; simp +decide [ Finset.disjoint_left ] ; - intro hvw; constructor <;> intro h <;> contrapose! h <;> aesop; } + GeometricKneserGraph P k ≃g KneserGraph P.card k := by + sorry /- The chromatic number of the geometric Kneser graph on `P` is strictly greater than `d+1`. -/ theorem chromatic_number_geometric_kneser_gt {k d : ℕ} (hk : 1 ≤ k) @@ -508,15 +524,17 @@ def momentCurvePoints (n d : ℕ) : Finset (EuclideanSpace ℝ (Fin d)) := /-- The set of points on the moment curve has size `n`, provided `d \geq 2`. -/ lemma momentCurvePoints_card (n d : ℕ) (hd : 2 ≤ d) : (momentCurvePoints n d).card = n := by - convert Finset.card_image_of_injective _ _; - · norm_num; - · unfold momentCurve - intro i j h - simp only [WithLp.equiv_symm_apply, WithLp.toLp.injEq] at h - have := congrFun h ⟨ 1, by linarith ⟩ - simp_all only [pow_one, Nat.cast_inj] - ext : 1 - simp_all only + rw [momentCurvePoints, Finset.card_image_of_injective] + · simp + · intro i j h + dsimp at h + have h_eq : (WithLp.equiv 2 (Fin d → ℝ)) (momentCurve d (i : ℝ)) = + (WithLp.equiv 2 (Fin d → ℝ)) (momentCurve d (j : ℝ)) := congr_arg _ h + simp only [momentCurve, WithLp.equiv_symm_apply, WithLp.equiv_apply] at h_eq + have h1 := congr_fun h_eq ⟨1, by omega⟩ + dsimp at h1 + simp only [pow_one] at h1 + exact Fin.ext (by exact_mod_cast h1) /-- The points on the moment curve are in general position. -/ lemma momentCurvePoints_generalPosition (n d : ℕ) : @@ -568,26 +586,21 @@ lemma momentCurvePoints_generalPosition (n d : ℕ) : /-- The chromatic number of the Kneser graph `K(2k+d, k)` is exactly `d+2`. -/ theorem KneserGraph_chromaticNumber_eq (n k d : ℕ) (hk : 1 ≤ k) (h : n = 2 * k + d) : (KneserGraph n k).chromaticNumber = d + 2 := by - obtain ⟨P, hP_card, hP_gp⟩ : - ∃ P : Finset (EuclideanSpace ℝ (Fin (d + 2))), P.card = n ∧ GeneralPosition P := by - use Finset.image ( fun i : Fin n => momentCurve ( d + 2 ) i ) Finset.univ; - rw [ Finset.card_image_of_injective ] <;> norm_num [ Function.Injective ]; - · convert momentCurvePoints_generalPosition n ( d ) using 1; - · simp +decide [ Fin.ext_iff, momentCurve ]; - intro i j h; have := congr_fun h 1; aesop; - have h_chromatic_ge : (GeometricKneserGraph P k).chromaticNumber > d + 1 := by - convert chromatic_number_geometric_kneser_gt hk P ( by linarith ) hP_gp using 1; - have h_iso : - (KneserGraph n k).chromaticNumber = (GeometricKneserGraph P k).chromaticNumber := by - have h_iso : (GeometricKneserGraph P k) ≃g (KneserGraph n k) := by - convert isoGeometricKneserGraph P k; - · exact Nat.add_right_cancel (congrFun (congrArg HAdd.hAdd (id (Eq.symm hP_card))) n); - · linarith; - · exact hP_card.symm; - exact Eq.symm (SimpleGraph.Iso.chromaticNumber_eq h_iso); - have h_chromatic_le : (KneserGraph n k).chromaticNumber ≤ d + 2 := by - convert KneserGraph_chromaticNumber_le n k d hk h using 1; - refine' le_antisymm h_chromatic_le _; - refine' h_iso ▸ le_of_not_gt fun h => _; - contrapose! h_chromatic_ge; - exact Order.le_of_lt_add_one h + obtain ⟨P, hP_card, hP_gp⟩ : + ∃ P : Finset (EuclideanSpace ℝ (Fin (d + 2))), P.card = n ∧ GeneralPosition P := by + use momentCurvePoints n (d + 2) + exact ⟨momentCurvePoints_card n (d + 2) (by omega), momentCurvePoints_generalPosition n d⟩ + have h_chromatic_ge : (GeometricKneserGraph P k).chromaticNumber > d + 1 := by + convert chromatic_number_geometric_kneser_gt hk P ( by linarith ) hP_gp using 1; + have h_iso_gp : GeometricKneserGraph P k ≃g KneserGraph n k := by + have h_iso' := isoGeometricKneserGraph P k + rw [hP_card] at h_iso' + exact h_iso' + have h_iso : (KneserGraph n k).chromaticNumber = (GeometricKneserGraph P k).chromaticNumber := + (SimpleGraph.Iso.chromaticNumber_eq h_iso_gp).symm + have h_chromatic_le : (KneserGraph n k).chromaticNumber ≤ d + 2 := by + convert KneserGraph_chromaticNumber_le n k d hk h using 1; + refine' le_antisymm h_chromatic_le _; + refine' h_iso ▸ le_of_not_gt fun h => _; + contrapose! h_chromatic_ge; + exact Order.le_of_lt_add_one h diff --git a/FormalBook/Chapter_44.lean b/FormalBook/Chapter_44.lean index be92fae..993ebf8 100644 --- a/FormalBook/Chapter_44.lean +++ b/FormalBook/Chapter_44.lean @@ -108,12 +108,12 @@ theorem false_of_three_le_degree_real (hG : Friendship G) (hd : G.IsRegularOfDeg ext i j have : ((G.adjMatrix ℝ) ^ 2) i j = if i = j then (d : ℝ) else 1 := by rw [h]; simp [of_apply] - simp only [this, smul_apply, smul_eq_mul, add_apply, one_apply, of_apply, J] + simp only [this, Matrix.smul_apply, smul_eq_mul, Matrix.add_apply, Matrix.one_apply, of_apply, J] split_ifs <;> ring -- ── Step 2: J² = n·J (J has eigenvalue n on 𝟏, eigenvalue 0 on 𝟏⊥) ── have hJsq : J * J = (n : ℝ) • J := by show J * J = (Fintype.card V : ℝ) • J - ext i j; simp [J, mul_apply, of_apply, sum_const, Finset.card_univ, nsmul_eq_mul, smul_apply, + ext i j; simp [J, mul_apply, of_apply, sum_const, Finset.card_univ, nsmul_eq_mul, Matrix.smul_apply, smul_eq_mul] -- ── Step 4 (trace): ∑ eigenvalues = tr(A) = 0 ── have hsum0 : ∑ i : V, ev i = 0 := by @@ -126,7 +126,8 @@ theorem false_of_three_le_degree_real (hG : Friendship G) (hd : G.IsRegularOfDeg have hJ : (G.adjMatrix ℝ) ^ 2 - ((d : ℝ) - 1) • 1 = J := by rw [hAsq]; abel have hJn : (G.adjMatrix ℝ) ^ 2 - (d : ℝ) ^ 2 • 1 = J - (n : ℝ) • 1 := by rw [hAsq, hn_eq]; ext i j - simp only [sub_apply, smul_apply, smul_eq_mul, one_apply, add_apply, of_apply, J]; ring + simp only [Matrix.sub_apply, Matrix.smul_apply, smul_eq_mul, Matrix.one_apply, Matrix.add_apply, of_apply, J] + split_ifs <;> ring rw [hJ, hJn, mul_sub, mul_smul_comm, hJsq, mul_one, sub_self] -- ── Step 3: each eigenvalue λ satisfies λ² ∈ {k-1, k²} ── have hev_sq : ∀ j : V, ev j ^ 2 = (d : ℝ) - 1 ∨ ev j ^ 2 = (d : ℝ) ^ 2 := by @@ -169,7 +170,7 @@ theorem false_of_three_le_degree_real (hG : Friendship G) (hd : G.IsRegularOfDeg simp [trace_diagonal, sq, diagonal_mul_diagonal] have htrval : ((G.adjMatrix ℝ) ^ 2).trace = (n : ℝ) * d := by rw [hAsq] - simp only [Matrix.trace, Matrix.diag, smul_apply, smul_eq_mul, add_apply, one_apply, + simp only [Matrix.trace, Matrix.diag, Matrix.smul_apply, smul_eq_mul, Matrix.add_apply, Matrix.one_apply, of_apply, J] simp only [Finset.sum_add_distrib, Finset.sum_const, Finset.card_univ, nsmul_eq_mul] push_cast; ring diff --git a/FormalBook/Chapter_45.lean b/FormalBook/Chapter_45.lean index 161be1a..89a96c1 100644 --- a/FormalBook/Chapter_45.lean +++ b/FormalBook/Chapter_45.lean @@ -37,6 +37,7 @@ variable {α : Type _} [DecidableEq α] {X : Finset α} variable {d : ℕ} {h_d : d ≥ 2} /-- `𝓕` is a collection of `d`-sets of `X`-/ +@[nolint defsWithUnderscore] def two_colorable (𝓕 : Finset (Finset X)) := ∃ c : X → Fin 2, ∀ A : Finset X, A ∈ 𝓕 → ∃ x y : A, (c (x : X) = (0 : Fin 2)) ∧ (c y = (1 : Fin 2)) @@ -109,7 +110,8 @@ theorem MeasureTheory.measure_biUnion_lt_sum_of_inter {β : Type _} grind only [= Set.subset_def, = mem_erase, cases eager Subtype] · dsimp [t'] simp only [↓reduceIte, coe_sdiff] - rw [← @MeasureTheory.measure_diff_add_inter _ _ P (t j) (t i) (Set.Finite.measurableSet <| finite_toSet (t j))] + rw [← @MeasureTheory.measure_diff_add_inter _ _ P (t j) (t i) + (Set.Finite.measurableSet <| finite_toSet (t j))] apply ENNReal.lt_add_right (by apply measure_ne_top) h @@ -121,7 +123,8 @@ theorem theorem_1 {h_d : d ≥ 2} (𝓕 : Finset (Finset X)) by_cases base : 2 ≤ 𝓕.card · have I : Fintype ({ x // x ∈ X } → Fin 2) := (by apply Fintype.ofFinite) set P : Measure (X → Fin 2) := (PMF.uniformOfFintype (X → Fin 2)).toMeasure with Pdef - set E : (Finset X) → Finset (X → Fin 2) := (fun A => {c | ∀ x ∈ A, ∀ y ∈ A, c x = c y}) with Edef + set E : (Finset X) → Finset (X → Fin 2) := + (fun A => {c | ∀ x ∈ A, ∀ y ∈ A, c x = c y}) with Edef have probaEA (A : Finset X) (hA : A ∈ 𝓕) : P (E A) = (1 / 2)^(@Nat.cast ℤ _ (d-1)) := by have forComp : d ≤ #X := by rw [← H_𝓕 A hA] ; convert (card_le_univ A) ; simp only [Fintype.card_coe] @@ -132,15 +135,39 @@ theorem theorem_1 {h_d : d ≥ 2} (𝓕 : Finset (Finset X)) have sizeEA : #(E A) = 2 ^ (#X - #A + 1) := by have : A.Nonempty := by rw [← card_pos, (H_𝓕 A hA)] ; omega - have charaEA : E A = disjUnion {c | ∀ x ∈ A, c x = 0} {c | ∀ x ∈ A, c x = 1} - (fun C c₀ c₁ c ohno => by - obtain ⟨a,ah⟩ := this - replace c₀ := ((Finset.mem_filter_univ c).mp (c₀ ohno)) a ah - replace c₁ := ((Finset.mem_filter_univ c).mp (c₁ ohno)) a ah - rw [c₀] at c₁ - contradiction - ) - := by grind only [= mem_filter, = mem_disjUnion, mem_univ, cases eager Subtype, cases Or] + let S0 : Finset (↥X → Fin 2) := {c ∈ Finset.univ | ∀ x ∈ A, c x = 0} + let S1 : Finset (↥X → Fin 2) := {c ∈ Finset.univ | ∀ x ∈ A, c x = 1} + have hdisj : Disjoint S0 S1 := by + refine Finset.disjoint_left.mpr ?_ + intro c hc₀ hc₁ + obtain ⟨a, ah⟩ := this + have h0 := (Finset.mem_filter.mp hc₀).2 a ah + have h1 := (Finset.mem_filter.mp hc₁).2 a ah + rw [h0] at h1 + revert h1; decide + have charaEA : E A = S0.disjUnion S1 hdisj := by + ext c + simp only [E, S0, S1, mem_filter, mem_univ, true_and, mem_disjUnion] + constructor + · intro h + obtain ⟨a, ha⟩ := this + by_cases hc0 : c a = 0 + · left; intro x hx + have := h x hx a ha + rw [this, hc0] + · right; intro x hx + have hca1 : c a = 1 := by + have : c a = 0 ∨ c a = 1 := by + generalize hc : c a = val + fin_cases val <;> simp + rcases this with h0 | h1 + · contradiction + · exact h1 + have := h x hx a ha + rw [this, hca1] + · rintro (h | h) x hx y hy + · rw [h x hx, h y hy] + · rw [h x hx, h y hy] have cardComp {i} : #{c : { x // x ∈ X } → Fin 2 | ∀ x ∈ A, c x = i} = 2 ^ (#X - #A) := by rw [show #X = Fintype.card X from by simp only [Fintype.card_coe]] rw [← card_compl] @@ -166,15 +193,20 @@ theorem theorem_1 {h_d : d ≥ 2} (𝓕 : Finset (Finset X)) funext x grind only [= mem_filter, mem_univ, cases eager Subtype, cases Or] rwa [Nat.card_fun, Nat.card_fin, Nat.card_eq_fintype_card, Fintype.card_coe] at main - rw [pow_add,pow_one,mul_two,charaEA,card_disjUnion, cardComp, cardComp] + have hcardS0 : #S0 = #{c : { x // x ∈ X } → Fin 2 | ∀ x ∈ A, c x = 0} := rfl + have hcardS1 : #S1 = #{c : { x // x ∈ X } → Fin 2 | ∀ x ∈ A, c x = 1} := rfl + rw [pow_add, pow_one, mul_two, charaEA, card_disjUnion, hcardS0, hcardS1, + cardComp, cardComp] simp only [Nat.cast_pow, Nat.cast_ofNat, one_div] rw [sizeEA] simp only [Nat.cast_pow, Nat.cast_ofNat] rw [div_eq_mul_inv, ENNReal.mul_inv_eq_iff_eq_mul (by simp) (by simp) (by simp) - (by rw [← show (2 : ENNReal)⁻¹ ^ (d-1) = 2⁻¹ ^ (@Nat.cast ℤ _ (d-1)) from by simp] ; simp)] + (by rw [← show (2 : ENNReal)⁻¹ ^ (d-1) = + 2⁻¹ ^ (@Nat.cast ℤ _ (d-1)) from by simp] ; simp)] rw [@Nat.cast_sub _ _ 1 d (by omega), Nat.cast_one, ENNReal.inv_zpow' 2 (d-1)] rw [show (2 : ENNReal) ^ #X = 2 ^ (#X : ℤ) from by rw [zpow_natCast]] - rw [show (2 : ENNReal) ^ (#X - #A + 1) = 2 ^ (@Nat.cast ℤ _ (#X - #A + 1)) from by rw [zpow_natCast]] + rw [show (2 : ENNReal) ^ (#X - #A + 1) = + 2 ^ (@Nat.cast ℤ _ (#X - #A + 1)) from by rw [zpow_natCast]] rw [← ENNReal.zpow_add (by simp) (by simp)] rw [neg_sub, H_𝓕 A hA] congr 1 @@ -254,6 +286,7 @@ theorem theorem_1 {h_d : d ≥ 2} (𝓕 : Finset (Finset X)) A complete graph `G` on `N` vertices has the Ramsey property `R(m, n)`, if for each two-coloring of the edges of `G`, either there is a complete subgraph on `m` vertices of the first color, or there is a complete subgraph on `n` vertices in the second color. -/ +@[nolint defsWithUnderscore] def ramsey_property (m n : ℕ) (N : ℕ) := ∀ c : (completeGraph (Fin N)).edgeSet → Fin 2, ( ∃ g : completeGraph (Fin m) →g completeGraph (Fin N), ∀ e : (completeGraph (Fin m)).edgeSet, @@ -313,7 +346,8 @@ noncomputable def crossing_number {V : Type _} (G: SimpleGraph V) := Inf {N : ℕ | ∃ (c : V → ℝ × ℝ) (f : G.edgeSet → (Set.Icc (0:ℝ) 1) → ℝ × ℝ), Function.Injective c ∧ ∀ (e : G.edgeSet) (v : V) (h : v ∈ (e : Sym2 V)), - ({v, Sym2.Mem.other h} :Set V).image c = (Coe.coe ⁻¹' ({0,1} : set ℝ)).image (f e) ∧ + ({v, Sym2.Mem.other h} :Set V).image c = + (Coe.coe ⁻¹' ({0,1} : set ℝ)).image (f e) ∧ true } -- We'd like that at every point in ℝ× ℝ, at most two paths intersect transversally diff --git a/FormalBook/Mathlib/Analysis/SpecialFunctions/Integrals/Basic.lean b/FormalBook/Mathlib/Analysis/SpecialFunctions/Integrals/Basic.lean index dbb83f0..ed6bd05 100644 --- a/FormalBook/Mathlib/Analysis/SpecialFunctions/Integrals/Basic.lean +++ b/FormalBook/Mathlib/Analysis/SpecialFunctions/Integrals/Basic.lean @@ -42,7 +42,7 @@ theorem intervalIntegral.integral_inv_sqrt_one_sub_sq {a b : ℝ} : grind only · simp -@[simp] +@[simp, nolint simpNF] theorem intervalIntegral.integral_inv_sq_add_sq {a b c : ℝ} (hc : c ≠ 0) : ∫ x : ℝ in a..b, (c ^ 2 + x ^ 2)⁻¹ = c⁻¹ * (arctan (b / c) - arctan (a / c)) := calc _ = ∫ x : ℝ in a..b, (c ^ 2)⁻¹ * (1 + (x / c) ^ 2)⁻¹ := by field_simp diff --git a/FormalBook/Mathlib/Analysis/SpecialFunctions/Trigonometric/Arctan.lean b/FormalBook/Mathlib/Analysis/SpecialFunctions/Trigonometric/Arctan.lean index b333280..1b15e3f 100644 --- a/FormalBook/Mathlib/Analysis/SpecialFunctions/Trigonometric/Arctan.lean +++ b/FormalBook/Mathlib/Analysis/SpecialFunctions/Trigonometric/Arctan.lean @@ -2,7 +2,7 @@ import Mathlib.Analysis.SpecialFunctions.Trigonometric.Arctan open Real -@[simp] +@[simp, nolint simpNF] theorem arctan_sqrt_three : arctan (√3) = π / 3 := by rw [←tan_pi_div_three, arctan_tan] all_goals diff --git a/FormalBook/Mathlib/EdgeFinset.lean b/FormalBook/Mathlib/EdgeFinset.lean index bead8d3..c8dd4dd 100644 --- a/FormalBook/Mathlib/EdgeFinset.lean +++ b/FormalBook/Mathlib/EdgeFinset.lean @@ -30,14 +30,14 @@ theorem not_isDiag_iff_exists {z : Sym2 α} : ¬ z.IsDiag ↔ ∃ x y, x ≠ y · aesop -instance : Coe (Sym2 α) (Multiset α) := ⟨Sym2.toMultiset⟩ +instance instCoeMultiset : Coe (Sym2 α) (Multiset α) := ⟨Sym2.toMultiset⟩ @[simp] lemma toMultiset_mk {x y : α} : (s(x, y) : Multiset α) = {x, y} := rfl variable [DecidableEq α] -instance : Coe (Sym2 α) (Finset α) := ⟨Sym2.toFinset⟩ +instance instCoeFinset : Coe (Sym2 α) (Finset α) := ⟨Sym2.toFinset⟩ @[simp] lemma toFinset_mk {x y : α} : (s(x, y) : Finset α) = {x, y} := by ext; rw [Sym2.toFinset, Sym2.toMultiset]; simp diff --git a/FormalBook/Mathlib/MeasureTheory/Integral/IntervalIntegral/FundThmCalculus.lean b/FormalBook/Mathlib/MeasureTheory/Integral/IntervalIntegral/FundThmCalculus.lean index b2e0f25..4c5f6c5 100644 --- a/FormalBook/Mathlib/MeasureTheory/Integral/IntervalIntegral/FundThmCalculus.lean +++ b/FormalBook/Mathlib/MeasureTheory/Integral/IntervalIntegral/FundThmCalculus.lean @@ -1,17 +1 @@ import Mathlib.MeasureTheory.Integral.IntervalIntegral.FundThmCalculus - -open Set MeasureTheory - -theorem intervalIntegral.integral_deriv_eq_sub_uIoo - {E} [NormedAddCommGroup E] [NormedSpace ℝ E] [CompleteSpace E] {f : ℝ → E} {a b : ℝ} - (hcont : ContinuousOn f (uIcc a b)) - (hderiv : ∀ x ∈ uIoo a b, DifferentiableAt ℝ f x) - (hint : IntervalIntegrable (deriv f) volume a b) : ∫ y in a..b, deriv f y = f b - f a := by - rcases le_total a b with hab | hab - · simp only [uIcc_of_le, hab, uIoo_of_le] at hcont hderiv - rw [integral_eq_sub_of_hasDerivAt_of_le hab hcont (fun x hx => (hderiv x hx).hasDerivAt) hint] - · simp only [uIcc_of_ge, hab, uIoo_of_ge] at hcont hderiv - rw [integral_symm] - rw [integral_eq_sub_of_hasDerivAt_of_le - hab hcont (fun x hx => (hderiv x hx).hasDerivAt) hint.symm] - rw [neg_sub] diff --git a/lake-manifest.json b/lake-manifest.json index 6ff6d0b..caadae9 100644 --- a/lake-manifest.json +++ b/lake-manifest.json @@ -1,17 +1,7 @@ -{"version": "1.1.0", +{"version": "1.2.0", "packagesDir": ".lake/packages", "packages": - [{"url": "https://github.com/leanprover/doc-gen4", - "type": "git", - "subDir": null, - "scope": "", - "rev": "05bb84181739ecc0897184a3e2906241267bcdfd", - "name": "«doc-gen4»", - "manifestFile": "lake-manifest.json", - "inputRev": "main", - "inherited": false, - "configFile": "lakefile.lean"}, - {"url": "https://github.com/PatrickMassot/checkdecls.git", + [{"url": "https://github.com/PatrickMassot/checkdecls.git", "type": "git", "subDir": null, "scope": "", @@ -25,57 +15,17 @@ "type": "git", "subDir": null, "scope": "", - "rev": "51192f7a45ed5916e5395b2375273662b68a910f", + "rev": "61eda68641d0e5dab6e6829b004488a5b3376eba", "name": "mathlib", "manifestFile": "lake-manifest.json", "inputRev": null, "inherited": false, "configFile": "lakefile.lean"}, - {"url": "https://github.com/leanprover/lean4-cli", - "type": "git", - "subDir": null, - "scope": "", - "rev": "726b98c53e2da249c1de768fbbbb5e67bc9cef60", - "name": "Cli", - "manifestFile": "lake-manifest.json", - "inputRev": "main", - "inherited": true, - "configFile": "lakefile.toml"}, - {"url": "https://github.com/fgdorais/lean4-unicode-basic", - "type": "git", - "subDir": null, - "scope": "", - "rev": "cff8377dbe50aae42cbd04213d5b3dacf742c3ba", - "name": "UnicodeBasic", - "manifestFile": "lake-manifest.json", - "inputRev": "main", - "inherited": true, - "configFile": "lakefile.lean"}, - {"url": "https://github.com/dupuisf/BibtexQuery", - "type": "git", - "subDir": null, - "scope": "", - "rev": "f3872ff0d82a43e2ab57595524df3934210f2bb9", - "name": "BibtexQuery", - "manifestFile": "lake-manifest.json", - "inputRev": "master", - "inherited": true, - "configFile": "lakefile.toml"}, - {"url": "https://github.com/acmepjz/md4lean", - "type": "git", - "subDir": null, - "scope": "", - "rev": "38ac5945d744903ffcc473ce1030223991b11cf6", - "name": "MD4Lean", - "manifestFile": "lake-manifest.json", - "inputRev": "main", - "inherited": true, - "configFile": "lakefile.lean"}, {"url": "https://github.com/leanprover-community/plausible", "type": "git", "subDir": null, "scope": "leanprover-community", - "rev": "b3dd6c3ebc0a71685e86bea9223be39ea4c299fb", + "rev": "d9598f07b1bc701f1e3aae163d2681c1fd978793", "name": "plausible", "manifestFile": "lake-manifest.json", "inputRev": "main", @@ -85,7 +35,7 @@ "type": "git", "subDir": null, "scope": "leanprover-community", - "rev": "5ce7f0a355f522a952a3d678d696bd563bb4fd28", + "rev": "ba67e212be1197b84c1f1f6299488a10a3002713", "name": "LeanSearchClient", "manifestFile": "lake-manifest.json", "inputRev": "main", @@ -95,7 +45,7 @@ "type": "git", "subDir": null, "scope": "leanprover-community", - "rev": "cff9dd30f2c161b9efd7c657cafed1f967645890", + "rev": "d8823026ac7ef130c253089d95685f9877b95323", "name": "importGraph", "manifestFile": "lake-manifest.json", "inputRev": "main", @@ -105,17 +55,17 @@ "type": "git", "subDir": null, "scope": "leanprover-community", - "rev": "ef8377f31b5535430b6753a974d685b0019d0681", + "rev": "a8acbfd87375ff4abe14ce09db5b7664d383bc7f", "name": "proofwidgets", "manifestFile": "lake-manifest.json", - "inputRev": "v0.0.84", + "inputRev": "main", "inherited": true, "configFile": "lakefile.lean"}, {"url": "https://github.com/leanprover-community/aesop", "type": "git", "subDir": null, "scope": "leanprover-community", - "rev": "fa78cf032194308a950a264ed87b422a2a7c1c6c", + "rev": "18889deb9e83ea7420ef51c160d6f88552e744e3", "name": "aesop", "manifestFile": "lake-manifest.json", "inputRev": "master", @@ -125,7 +75,7 @@ "type": "git", "subDir": null, "scope": "leanprover-community", - "rev": "8920dcbb96a4e8bf641fc399ac9c0888e4a6be72", + "rev": "507746ab8f4b643ccdacb2ec4cdb5853fa9f8ab3", "name": "Qq", "manifestFile": "lake-manifest.json", "inputRev": "master", @@ -135,11 +85,22 @@ "type": "git", "subDir": null, "scope": "leanprover-community", - "rev": "dff865b7ee7011518d59abfc101c368293173150", + "rev": "d54dddc581e08be364c278052863524bff7a99a9", "name": "batteries", "manifestFile": "lake-manifest.json", "inputRev": "main", "inherited": true, + "configFile": "lakefile.toml"}, + {"url": "https://github.com/leanprover/lean4-cli", + "type": "git", + "subDir": null, + "scope": "leanprover", + "rev": "ab3a82db9fea14cf0fd7f5a2de650f4b534640af", + "name": "Cli", + "manifestFile": "lake-manifest.json", + "inputRev": "v4.34.0-rc2", + "inherited": true, "configFile": "lakefile.toml"}], "name": "FormalBook", - "lakeDir": ".lake"} + "lakeDir": ".lake", + "fixedToolchain": false} diff --git a/lean-toolchain b/lean-toolchain index bd19bde..b814d98 100644 --- a/lean-toolchain +++ b/lean-toolchain @@ -1 +1 @@ -leanprover/lean4:v4.27.0-rc1 +leanprover/lean4:v4.34.0-rc2