diff --git a/analysis/Analysis/Section_8_1.lean b/analysis/Analysis/Section_8_1.lean index d891e67..db11c4f 100644 --- a/analysis/Analysis/Section_8_1.lean +++ b/analysis/Analysis/Section_8_1.lean @@ -30,8 +30,8 @@ abbrev EqualCard (X Y : Type) : Prop := ∃ f : X → Y, Function.Bijective f theorem EqualCard.iff {X Y : Type} : EqualCard X Y ↔ Nonempty (X ≃ Y) := by simp [EqualCard] constructor - . rintro ⟨ f, hf ⟩; exact ⟨ Equiv.ofBijective f hf ⟩ - rintro ⟨ e ⟩; exact ⟨ e.toFun, e.bijective ⟩ + . intro ⟨ f, hf ⟩; exact ⟨ .ofBijective f hf ⟩ + intro ⟨ e ⟩; exact ⟨ e.toFun, e.bijective ⟩ /-- Equivalence with Mathlib's `Cardinal.mk` concept -/ theorem EqualCard.iff' {X Y : Type} : EqualCard X Y ↔ Cardinal.mk X = Cardinal.mk Y := by @@ -59,9 +59,7 @@ theorem CountablyInfinite.equiv {X Y: Type} (hXY : EqualCard X Y) : CountablyInfinite X ↔ CountablyInfinite Y := ⟨ hXY.symm.trans, hXY.trans ⟩ theorem Finite.equiv {X Y: Type} (hXY : EqualCard X Y) : - Finite X ↔ Finite Y := by - obtain ⟨ f, hf ⟩ := hXY - exact Equiv.finite_iff (Equiv.ofBijective f hf) + Finite X ↔ Finite Y := by obtain ⟨ f, hf ⟩ := hXY; exact (Equiv.ofBijective f hf).finite_iff theorem AtMostCountable.equiv {X Y: Type} (hXY : EqualCard X Y) : AtMostCountable X ↔ AtMostCountable Y := by @@ -71,43 +69,40 @@ theorem AtMostCountable.equiv {X Y: Type} (hXY : EqualCard X Y) : theorem CountablyInfinite.iff (X : Type) : CountablyInfinite X ↔ Nonempty (Denumerable X) := by simp [CountablyInfinite, EqualCard.iff] constructor - . rintro ⟨ e ⟩; exact ⟨ Denumerable.mk' e ⟩ - rintro ⟨ h ⟩; exact ⟨ Denumerable.eqv X ⟩ + . intro ⟨ e ⟩; exact ⟨ Denumerable.mk' e ⟩ + intro ⟨ h ⟩; exact ⟨ h.eqv X ⟩ /-- Equivalence with Mathlib's `Countable` typeclass -/ theorem CountablyInfinite.iff' (X : Type) : CountablyInfinite X ↔ Countable X ∧ Infinite X := by rw [iff, nonempty_denumerable_iff] theorem CountablyInfinite.toCountable {X : Type} (hX: CountablyInfinite X) : Countable X := by - rw [iff'] at hX; tauto + simp_all [iff'] theorem CountablyInfinite.toInfinite {X : Type} (hX: CountablyInfinite X) : Infinite X := by - rw [iff'] at hX; tauto + simp_all [iff'] theorem AtMostCountable.iff (X : Type) : AtMostCountable X ↔ Countable X := by observe h1 : CountablyInfinite X ↔ Countable X ∧ Infinite X observe h2 : Finite X ∨ Infinite X observe h3 : Finite X → Countable X - unfold AtMostCountable; tauto + tauto theorem CountablyInfinite.iff_image_inj {A:Type} (X: Set A) : CountablyInfinite X ↔ ∃ f : ℕ ↪ A, X = f '' .univ := by constructor - . rintro ⟨ g, hg ⟩ + . intro ⟨ g, hg ⟩ obtain ⟨ f, hleft, hright ⟩ := Function.bijective_iff_has_inverse.mp hg refine ⟨ ⟨ Subtype.val ∘ f, ?_ ⟩, ?_ ⟩ - . intro x y hxy; simp [Subtype.val_inj] at hxy; rw [←hright x, ←hright y, hxy] - ext x; simp; constructor - . intro hx; use g ⟨ x, hx ⟩; simp [hleft _] - rintro ⟨ n, rfl ⟩; aesop - rintro ⟨ f, hf ⟩ + . intro x y hxy; apply hright.injective; simp_all [Subtype.val_inj] + ext; simp; constructor + . intro hx; use g ⟨ _, hx ⟩; simp [hleft _] + rintro ⟨ _, rfl ⟩; aesop + intro ⟨ f, hf ⟩ have := Function.leftInverse_invFun (Function.Embedding.injective f) - set g := Function.invFun f - use g ∘ Subtype.val + use (Function.invFun f) ∘ Subtype.val constructor - . rintro ⟨ x, hx ⟩ ⟨ y, hy ⟩ h - simp [hf] at h ⊢ hx hy - obtain ⟨ n, rfl ⟩ := hx - obtain ⟨ m, rfl ⟩ := hy + . rintro ⟨ x, hx ⟩ ⟨ y, hy ⟩ h; simp [hf] at h ⊢ hx hy + obtain ⟨ n, rfl ⟩ := hx; obtain ⟨ m, rfl ⟩ := hy simp [this n, this m] at h; aesop intro n; use ⟨ f n, by aesop ⟩; simp [this n] @@ -136,8 +131,7 @@ def NNRat.exists_unique_min : Decidable (∀ (X : Set NNRat) (hX : X.Nonempty), open Classical in noncomputable abbrev Nat.min (X : Set ℕ) : ℕ := if hX : X.Nonempty then (exists_unique_min hX).exists.choose else 0 -theorem Nat.min_spec {X : Set ℕ} (hX : X.Nonempty) : - min X ∈ X ∧ ∀ n ∈ X, min X ≤ n := by +theorem Nat.min_spec {X : Set ℕ} (hX : X.Nonempty) : min X ∈ X ∧ ∀ n ∈ X, min X ≤ n := by simp [hX, min]; exact (exists_unique_min hX).exists.choose_spec theorem Nat.min_eq {X : Set ℕ} (hX : X.Nonempty) {a:ℕ} (ha : a ∈ X ∧ ∀ n ∈ X, a ≤ n) : min X = a := @@ -175,7 +169,7 @@ theorem Nat.monotone_enum_of_infinite (X : Set ℕ) [Infinite X] : ∃! f : ℕ have hf_injective : Function.Injective f := by intro x y hxy; simp [f] at hxy; solve_by_elim have hf_surjective : Function.Surjective f := by - rintro ⟨ x, hx ⟩; simp [f]; by_contra + intro ⟨ x, hx ⟩; simp [f]; by_contra have h1 (n:ℕ) : x ∈ { x ∈ X | ∀ (m:ℕ) (h:m < n), x ≠ a m } := by sorry have h2 (n:ℕ) : x ≥ a n := by @@ -184,50 +178,41 @@ theorem Nat.monotone_enum_of_infinite (X : Set ℕ) [Infinite X] : ∃! f : ℕ sorry have h4 (n:ℕ) : x ≥ n := (h3 n).trans (h2 n) linarith [h4 (x+1)] - apply ExistsUnique.intro f ⟨ ⟨ hf_injective, hf_surjective ⟩, ha_mono ⟩ - rintro g ⟨ hg_bijective, hg_mono ⟩; by_contra! + apply ExistsUnique.intro _ ⟨ ⟨ hf_injective, hf_surjective ⟩, ha_mono ⟩ + intro g ⟨ hg_bijective, hg_mono ⟩; by_contra! replace : { n | g n ≠ f n }.Nonempty := by contrapose! this - simp [Set.eq_empty_iff_forall_notMem] at this - ext n; simp [this n] + apply funext; simpa [Set.eq_empty_iff_forall_notMem] using this set m := min { n | g n ≠ f n } have hm : g m ≠ f m := (min_spec this).1 have hm' {n:ℕ} (hn: n < m) : g n = f n := by by_contra hgfn; linarith [(min_spec this).2 n (by simp [hgfn])] have hgm : g m = min { x ∈ X | ∀ (n:ℕ) (h:n < m), x ≠ a n } := by sorry - rw [←ha m] at hgm - contrapose! hm; exact Subtype.val_injective hgm + rw [←ha m] at hgm; contrapose! hm; exact Subtype.val_injective hgm theorem Nat.countable_of_infinite (X : Set ℕ) [Infinite X] : CountablyInfinite X := by - apply EqualCard.symm have := (monotone_enum_of_infinite X).exists - exact ⟨ this.choose, this.choose_spec.1 ⟩ + exact EqualCard.symm ⟨ this.choose, this.choose_spec.1 ⟩ /-- Corollary 8.1.6 -/ theorem Nat.atMostCountable_subset (X: Set ℕ) : AtMostCountable X := by - unfold AtMostCountable - rcases finite_or_infinite X with h | h + rcases finite_or_infinite X with _ | _ . tauto - simp [countable_of_infinite] + simp [AtMostCountable, countable_of_infinite] /-- Corollary 8.1.7 -/ theorem AtMostCountable.subset {X: Type} (hX : AtMostCountable X) (Y: Set X) : AtMostCountable Y := by -- This proof is written to follow the structure of the original text. - rcases hX with h | h - . obtain ⟨ f, hf ⟩ := h - let f' : Y → f '' Y := fun y ↦ ⟨ f y, by aesop ⟩ + rcases hX with ⟨ f, hf ⟩ | h + . let f' : Y → f '' Y := fun y ↦ ⟨ f y, by aesop ⟩ have hf' : Function.Bijective f' := by sorry - rw [AtMostCountable.equiv ⟨ f', hf' ⟩ ]; exact Nat.atMostCountable_subset _ + rw [equiv ⟨ _, hf' ⟩ ]; apply Nat.atMostCountable_subset simp [AtMostCountable, show Finite Y by infer_instance] theorem AtMostCountable.subset' {A: Type} {X Y: Set A} (hX: AtMostCountable X) (hY: Y ⊆ X) : AtMostCountable Y := by - set Y' := { x : X | ↑x ∈ Y } - have : AtMostCountable Y' := subset hX _ - apply (equiv _).mp this - use (fun y ↦ ⟨ ↑↑y, y.property ⟩ ) - constructor - . rintro ⟨ ⟨ y, hy ⟩, hy2 ⟩ ⟨ ⟨ y', hy' ⟩, hy2' ⟩ h; simp_all [Y'] + refine (equiv ⟨ fun y ↦ ⟨ ↑↑y, y.property ⟩, ?_, ?_ ⟩).mp (subset hX { x : X | ↑x ∈ Y }) + . intro ⟨ ⟨ _, _ ⟩, _ ⟩ ⟨ ⟨ _, _ ⟩, _ ⟩ _; simp_all rintro ⟨ y, hy ⟩; use ⟨ ⟨ y, hY hy ⟩, by aesop ⟩ /-- Proposition 8.1.8 / Exercise 8.1.4 -/ @@ -248,18 +233,16 @@ theorem Int.countablyInfinite : CountablyInfinite ℤ := by -- This proof is written to follow the structure of the original text. have h1 : CountablyInfinite {n:ℤ | n ≥ 0} := by rw [CountablyInfinite.iff_image_inj] - use ⟨ (↑·:ℕ → ℤ), by intro x y hxy; simpa using hxy ⟩ - ext n; simp; constructor + use ⟨ (↑·:ℕ → ℤ), by intro _ _ _; simp_all ⟩ + ext n; simp; refine ⟨ ?_, by aesop ⟩ . intro h; use n.toNat; simp [h] - rintro ⟨ m, rfl ⟩; simp have h2 : CountablyInfinite {n:ℤ | n ≤ 0} := by rw [CountablyInfinite.iff_image_inj] - use ⟨ (-↑·:ℕ → ℤ), by intro x y hxy; simpa using hxy ⟩ - ext n; simp; constructor - . intro h; use (-n).toNat; simp [h] - rintro ⟨ m, rfl ⟩; simp + use ⟨ (-↑·:ℕ → ℤ), by intro _ _ _; simp_all ⟩ + ext n; simp; refine ⟨ ?_, by aesop ⟩ + intro h; use (-n).toNat; simp [h] have : CountablyInfinite (.univ : Set ℤ) := by - convert CountablyInfinite.union h1 h2; ext n; simp; omega + convert h1.union h2; ext; simp; omega exact (CountablyInfinite.equiv (.univ _)).mp this /-- Lemma 8.1.12 -/ @@ -277,23 +260,23 @@ theorem CountablyInfinite.lower_diag : CountablyInfinite { n : ℕ × ℕ | n.2 . have : a n' + m' > a n + m := by calc _ ≥ a n' := by linarith _ ≥ a (n+1) := ha.monotone (by linarith) - _ = a n + (n + 1) := Finset.sum_range_succ (fun x ↦ x) _ + _ = a n + (n + 1) := Finset.sum_range_succ id _ _ > a n + m := by linarith linarith - . simp at h; tauto + . simpa using h have : a n + m > a n' + m' := by calc _ ≥ a n := by linarith _ ≥ a (n'+1) := ha.monotone (by linarith) - _ = a n' + (n' + 1) := Finset.sum_range_succ (fun x ↦ x) _ + _ = a n' + (n' + 1) := Finset.sum_range_succ id _ _ > a n' + m' := by linarith linarith let f' : A → f '' .univ := fun p ↦ ⟨ f p, by aesop ⟩ have hf' : Function.Bijective f' := by constructor . intro p q hpq; simp [f'] at hpq; solve_by_elim - rintro ⟨ l, hl ⟩; simp at hl + intro ⟨ l, hl ⟩; simp at hl obtain ⟨ n, m, q, rfl ⟩ := hl; use ⟨ (n, m), q ⟩ - have : AtMostCountable A := by rw [AtMostCountable.equiv ⟨ f', hf' ⟩]; exact Nat.atMostCountable_subset _ + have : AtMostCountable A := by rw [AtMostCountable.equiv ⟨ f', hf' ⟩]; apply Nat.atMostCountable_subset have hfin : ¬ Finite A := by sorry simp [AtMostCountable] at this; tauto @@ -301,11 +284,9 @@ theorem CountablyInfinite.lower_diag : CountablyInfinite { n : ℕ × ℕ | n.2 /-- Corollary 8.1.13 -/ theorem CountablyInfinite.prod_nat : CountablyInfinite (ℕ × ℕ) := by have upper_diag : CountablyInfinite { n : ℕ × ℕ | n.1 ≤ n.2 } := by - apply (equiv _).mp lower_diag - use fun ⟨ (n, m), hnm ⟩ ↦ ⟨ (m, n), by aesop ⟩ - constructor - . intro ⟨ (n, m), hnm ⟩ ⟨ (n', m'), hn'm' ⟩ h; simp at hnm hn'm' h ⊢; tauto - intro ⟨ (n, m), hnm ⟩; use ⟨ (m, n), by aesop ⟩ + refine (equiv ⟨ fun ⟨ (n, m), _ ⟩ ↦ ⟨ (m, n), by aesop ⟩, ?_, ?_ ⟩).mp lower_diag + . intro ⟨ (_, _), _ ⟩ ⟨ (_, _), _ ⟩ _; aesop + intro ⟨ (n, m), _ ⟩; use ⟨ (m, n), by aesop ⟩ have : CountablyInfinite (.univ : Set (ℕ × ℕ)) := by convert union lower_diag upper_diag; ext ⟨ n, m ⟩; simp; omega exact (equiv (.univ _)).mp this @@ -329,10 +310,9 @@ theorem Rat.countablyInfinite : CountablyInfinite ℚ := by have hfin : ¬ Finite ℚ := by by_contra! replace : Finite (.univ : Set ℕ) := by - apply Finite.Set.finite_of_finite_image (f := fun n:ℕ ↦ (n:ℚ)) - intro x _ y _; simp + apply @Finite.Set.finite_of_finite_image ℕ ℚ _ (↑·); intro _ _ _ _; simp rw [Set.finite_coe_iff, Set.finite_univ_iff,←not_infinite_iff_finite] at this - exact this (by infer_instance) + apply this; infer_instance tauto /-- Exercise 8.1.1 -/ diff --git a/analysis/Analysis/Section_8_2.lean b/analysis/Analysis/Section_8_2.lean index 01853c1..de33ab9 100644 --- a/analysis/Analysis/Section_8_2.lean +++ b/analysis/Analysis/Section_8_2.lean @@ -27,7 +27,7 @@ After this section, the summation notation developed here will be deprecated in -/ namespace Chapter8 -open Chapter7 +open Chapter7 Chapter7.Series /-- Definition 8.2.1 (Series on countable sets). Note that with this definition, functions defined on finite sets will not be absolutely convergent; one should use `AbsConvergent'` instead for such @@ -47,14 +47,14 @@ theorem Sum.of_finite {X:Type} [hX:Finite X] (f:X → ℝ) : Sum f = ∑ x ∈ @ by_contra! obtain ⟨ g, hg, _ ⟩ := this rw [←hg.finite_iff, ←not_infinite_iff_finite] at hX - exact hX (by infer_instance) + apply hX; infer_instance simp [Sum, this, hX] theorem AbsConvergent.comp {X: Type} {f:X → ℝ} {g:ℕ → X} (h: Function.Bijective g) (hf: AbsConvergent f) : (f ∘ g:Series).absConverges := by choose g' hbij hconv using hf obtain ⟨ g'_inv, hleft, hright ⟩ := Function.bijective_iff_has_inverse.mp hbij have hG : Function.Bijective (g'_inv ∘ g) := .comp ⟨hright.injective, hleft.surjective⟩ h - convert (Series.absConverges_of_permute hconv hG).1 using 4 with n + convert (absConverges_of_permute hconv hG).1 using 4 with n simp [hright (g n.toNat)] theorem Sum.eq {X: Type} {f:X → ℝ} {g:ℕ → X} (h: Function.Bijective g) (hfg: (f ∘ g:Series).absConverges) : (f ∘ g:Series).convergesTo (Sum f) := by @@ -63,30 +63,29 @@ theorem Sum.eq {X: Type} {f:X → ℝ} {g:ℕ → X} (h: Function.Bijective g) ( obtain ⟨ hbij, hconv ⟩ := this.choose_spec set g' := this.choose obtain ⟨ g'_inv, hleft, hright ⟩ := Function.bijective_iff_has_inverse.mp hbij - convert Series.convergesTo_sum (Series.converges_of_absConverges hfg) using 1 + convert convergesTo_sum (converges_of_absConverges hfg) using 1 have hG : Function.Bijective (g'_inv ∘ g) := .comp ⟨hright.injective, hleft.surjective⟩ h - convert (Series.absConverges_of_permute hconv hG).2 using 4 with _ n + convert (absConverges_of_permute hconv hG).2 using 4 with _ n by_cases hn : n ≥ 0 <;> simp [hn, hright (g n.toNat)] theorem Sum.of_comp {X Y:Type} {f:X → ℝ} (h: AbsConvergent f) {g: Y → X} (hbij: Function.Bijective g) : AbsConvergent (f ∘ g) ∧ Sum f = Sum (f ∘ g) := by - obtain ⟨ hbij', hconv' ⟩ := h.choose_spec - set g' := h.choose + choose g' hbij' hconv' using h obtain ⟨ g_inv, hleft, hright ⟩ := Function.bijective_iff_has_inverse.mp hbij have hbij_g_inv_g' : Function.Bijective (g_inv ∘ g') := .comp ⟨hright.injective, hleft.surjective⟩ hbij' have hident : (f ∘ g) ∘ g_inv ∘ g' = f ∘ g' := by ext n; simp [hright (g' n)] refine ⟨ ⟨ g_inv ∘ g', ⟨ hbij_g_inv_g', by convert hconv' ⟩ ⟩, ?_ ⟩ have h := eq (f := f ∘ g) hbij_g_inv_g' (by convert hconv') rw [hident] at h - exact Series.convergesTo_uniq (eq hbij' hconv') h + exact convergesTo_uniq (eq hbij' hconv') h @[simp] -theorem Finset.Icc_eq_cast (N:ℕ) : Finset.Icc 0 (N:ℤ) = Finset.map Nat.castEmbedding (Finset.Icc 0 N) := by +theorem Finset.Icc_eq_cast (N:ℕ) : .Icc 0 (N:ℤ) = Finset.map Nat.castEmbedding (.Icc 0 N) := by ext n; simp; constructor - . intro ⟨ hn, hn' ⟩; lift n to ℕ using hn; use n; simp_all - rintro ⟨ m, ⟨ hm, rfl ⟩ ⟩; simp_all + . intro ⟨ hn, _ ⟩; lift n to ℕ using hn; use n; simp_all + rintro ⟨ _, ⟨ _, rfl ⟩ ⟩; simp_all theorem Finset.Icc_empty {N:ℤ} (h: ¬ N ≥ 0) : Finset.Icc 0 N = ∅ := by - ext n; simp; intro hn; contrapose! h; linarith + ext; simp; intros; contrapose! h; linarith /-- Theorem 8.2.2, preliminary version. The arguments here are rearranged slightly from the text. -/ theorem sum_of_sum_of_AbsConvergent_nonneg {f:ℕ × ℕ → ℝ} (hf:AbsConvergent f) (hpos: ∀ n m, 0 ≤ f (n, m)) : @@ -94,7 +93,7 @@ theorem sum_of_sum_of_AbsConvergent_nonneg {f:ℕ × ℕ → ℝ} (hf:AbsConverg (fun n ↦ ((fun m ↦ f (n, m)):Series).sum:Series).convergesTo (Sum f) := by set L := Sum f have hLpos : 0 ≤ L := by - simp [L, Sum, hf]; apply Series.sum_of_nonneg; intro n; by_cases h: n ≥ 0 <;> simp [h]; exact hpos _ _ + simp [L, Sum, hf]; apply sum_of_nonneg; intro n; by_cases h: n ≥ 0 <;> simp [h]; apply hpos have hfinsum (X: Finset (ℕ × ℕ)) : ∑ p ∈ X, f p ≤ L := by sorry have hfinsum' (n M:ℕ) : ((fun m ↦ f (n, m)):Series).partial M ≤ L := by simp [Series.partial, Finset.Icc_eq_cast] @@ -102,12 +101,12 @@ theorem sum_of_sum_of_AbsConvergent_nonneg {f:ℕ × ℕ → ℝ} (hf:AbsConverg . simp solve_by_elim have hnon (n:ℕ) : ((fun m ↦ f (n, m)):Series).nonneg := by - simp [Series.nonneg]; intro m; by_cases h: m ≥ 0 <;> simp [h, hpos] + simp [nonneg]; intro m; by_cases h: m ≥ 0 <;> simp [h, hpos] have hconv (n:ℕ) : ((fun m ↦ f (n, m)):Series).converges := by - rw [Series.converges_of_nonneg_iff (hnon n)] + rw [converges_of_nonneg_iff (hnon n)] use L; intro N; by_cases h: N ≥ 0 . lift N to ℕ using h; solve_by_elim - rw [Series.partial_of_lt (by simp; linarith)]; simp [hLpos] + rw [partial_of_lt (by simp; linarith)]; simp [hLpos] have (N M:ℤ) : ∑ n ∈ .Icc 0 N, ((fun m ↦ f (n.toNat, m)):Series).partial M ≤ L := by by_cases hN : N ≥ 0; swap . simp [Finset.Icc_empty hN, hLpos] @@ -122,16 +121,16 @@ theorem sum_of_sum_of_AbsConvergent_nonneg {f:ℕ × ℕ → ℝ} (hf:AbsConverg solve_by_elim replace (N:ℤ) : ∑ n ∈ .Icc 0 N, ((fun m ↦ f (n.toNat, m)):Series).sum ≤ L := by apply le_of_tendsto' (x := .atTop) (tendsto_finset_sum _ _) (this N) - intro n _; exact Series.convergesTo_sum (by solve_by_elim) + intro n _; exact convergesTo_sum (by solve_by_elim) replace (N:ℤ) : (fun n ↦ ((fun m ↦ f (n, m)):Series).sum:Series).partial N ≤ L := by convert this N with n hn; simp_all have hnon' : (fun n ↦ ((fun m ↦ f (n, m)):Series).sum:Series).nonneg := by intro n; by_cases h: n ≥ 0 <;> simp [h] - exact Series.sum_of_nonneg (hnon n.toNat) + exact sum_of_nonneg (hnon n.toNat) have hconv' : (fun n ↦ ((fun m ↦ f (n, m)):Series).sum:Series).converges := by - rw [Series.converges_of_nonneg_iff hnon']; use L + rw [converges_of_nonneg_iff hnon']; use L replace : (fun n ↦ ((fun m ↦ f (n, m)):Series).sum:Series).sum ≤ L := - le_of_tendsto' ( Series.convergesTo_sum hconv') this + le_of_tendsto' (convergesTo_sum hconv') this replace : (fun n ↦ ((fun m ↦ f (n, m)):Series).sum:Series).sum = L := by apply le_antisymm this (le_of_forall_sub_le _); intro ε hε replace : ∃ X, ∑ p ∈ X, f p ≥ L - ε := by @@ -146,10 +145,10 @@ theorem sum_of_sum_of_AbsConvergent_nonneg {f:ℕ × ℕ → ℝ} (hf:AbsConverg _ = ∑ n ∈ .Icc 0 N, ∑ m ∈ .Icc 0 M, f (n, m) := Finset.sum_product _ _ _ _ ≤ ∑ n ∈ .Icc 0 N, ((fun m ↦ f (n, m)):Series).sum := by apply Finset.sum_le_sum; intro n _ - convert Series.partial_le_sum_of_nonneg (hnon n) (hconv n) M + convert partial_le_sum_of_nonneg (hnon n) (hconv n) M simp [Series.partial] _ = (fun n ↦ ((fun m ↦ f (n, m)):Series).sum:Series).partial N := by simp [Series.partial] - _ ≤ _ := Series.partial_le_sum_of_nonneg hnon' hconv' _ + _ ≤ _ := partial_le_sum_of_nonneg hnon' hconv' _ simp [hconv, ← this, Series.convergesTo_sum hconv'] /-- Theorem 8.2.2, second version -/ @@ -168,7 +167,7 @@ theorem sum_of_sum_of_AbsConvergent {f:ℕ × ℕ → ℝ} (hf:AbsConvergent f) constructor . intro n sorry - convert Series.convergesTo.sub hfplus_sum hfminus_sum using 1 + convert convergesTo.sub hfplus_sum hfminus_sum using 1 . -- encountered surprising difficulty with definitional equivalence here simp [hdiff] change (fun n ↦ ((fun m ↦ (fplus - fminus) (n, m)):Series).sum:Series) = @@ -176,9 +175,9 @@ theorem sum_of_sum_of_AbsConvergent {f:ℕ × ℕ → ℝ} (hf:AbsConvergent f) - (fun n ↦ ((fun m ↦ (fminus) (n, m)):Series).sum:Series) convert_to (fun n ↦ ((fun m ↦ (fplus - fminus) (n, m)):Series).sum:Series) = (((fun n ↦ ((fun m ↦ fplus (n, m)):Series).sum) - (fun n ↦ ((fun m ↦ (fminus) (n, m)):Series).sum):ℕ → ℝ):Series) - . convert Series.sub_coe _ _ + . convert sub_coe _ _ rcongr _ n; simp - convert (Series.sub _ _).2 with m; rfl + convert (sub _ _).2 with m; rfl by_cases h: m ≥ 0 <;> simp [h, HSub.hSub, Sub.sub] . solve_by_elim convert hfminus_conv' n.toNat @@ -186,8 +185,8 @@ theorem sum_of_sum_of_AbsConvergent {f:ℕ × ℕ → ℝ} (hf:AbsConvergent f) have h1 := Sum.eq hg (hf.comp hg) have hplus := Sum.eq hg (hfplus_conv.comp hg) have hminus := Sum.eq hg (hfminus_conv.comp hg) - apply Series.convergesTo_uniq h1 _ - convert (Series.convergesTo.sub hplus hminus) using 3 with n + apply convergesTo_uniq h1 _ + convert (convergesTo.sub hplus hminus) using 3 with n by_cases h:n ≥ 0 <;> simp [h,hdiff, HSub.hSub, Sub.sub] /-- Theorem 8.2.2, third version -/ @@ -199,14 +198,14 @@ theorem sum_of_sum_of_AbsConvergent' {f:ℕ × ℕ → ℝ} (hf:AbsConvergent f) have ⟨ g, hg, hconv ⟩ := hf convert sum_of_sum_of_AbsConvergent (f := f ∘ π) _ using 2 . exact (Sum.of_comp hf hπ).2 - refine ⟨ π ∘ g, Function.Bijective.comp hπ hg, ?_ ⟩ + refine ⟨ _, hπ.comp hg, ?_ ⟩ convert hconv using 2 /-- Theorem 8.2.2, fourth version -/ theorem sum_comm {f:ℕ × ℕ → ℝ} (hf:AbsConvergent f) : (fun n ↦ ((fun m ↦ f (n, m)):Series).sum:Series).sum = (fun m ↦ ((fun n ↦ f (n, m)):Series).sum:Series).sum := by - simp [Series.sum_of_converges (sum_of_sum_of_AbsConvergent hf).2, - Series.sum_of_converges (sum_of_sum_of_AbsConvergent' hf).2] + simp [sum_of_converges (sum_of_sum_of_AbsConvergent hf).2, + sum_of_converges (sum_of_sum_of_AbsConvergent' hf).2] /-- Lemma 8.2.3 / Exercise 8.2.1 -/ theorem AbsConvergent.iff {X:Type} (hX:CountablyInfinite X) (f : X → ℝ) : @@ -224,17 +223,17 @@ theorem AbsConvergent'.of_countable {X:Type} (hX:CountablyInfinite X) {f:X → AbsConvergent' f ↔ AbsConvergent f := by constructor . intro hf; simp [bddAbove_def] at hf; obtain ⟨ L, hL ⟩ := hf - obtain ⟨ g, hg ⟩ := hX.symm; refine ⟨ g, hg, ?_ ⟩ - unfold Series.absConverges - rw [Series.converges_of_nonneg_iff] + have ⟨ g, hg ⟩ := hX.symm; refine ⟨ g, hg, ?_ ⟩ + unfold absConverges + rw [converges_of_nonneg_iff] . use L; intro N; by_cases hN: N ≥ 0 . lift N to ℕ using hN set g':= Function.Embedding.mk g hg.1 convert hL (Finset.map g' (Finset.Icc 0 N)) simp [Series.partial]; rfl convert hL ∅ - simp; apply Series.partial_of_lt; simp; contrapose! hN; assumption - simp [Series.nonneg] + simp; apply partial_of_lt; simp; contrapose! hN; assumption + simp [nonneg] intro n; by_cases h: n ≥ 0 <;> simp [h] intro hf; rwa [AbsConvergent.iff hX f] at hf @@ -258,7 +257,7 @@ to establish without this) -/ theorem Sum'.of_finsupp {X:Type} {f:X → ℝ} {A: Finset X} (h: ∀ x ∉ A, f x = 0) : Sum' f = ∑ x ∈ A, f x := by unfold Sum' set E := { x | f x ≠ 0 } - have hE : E ⊆ A := by intro x; simp [E]; by_contra!; specialize h x this.2; tauto + have hE : E ⊆ A := by intro x; simp [E]; by_contra!; aesop have hfin : Finite E := .Set.subset _ hE set E' := E.toFinite.toFinset rw [Sum.of_finite (fun x:E ↦ f x), ←Finset.sum_subtype E' (by simp [E'])] @@ -278,16 +277,15 @@ theorem Sum'.of_countable_supp {X:Type} {f:X → ℝ} {A: Set X} (hA: CountablyI unfold Sum' set E := { x | f x ≠ 0 } -- The main challenge here is to relate a sum on E with a sum on A. First, we show containment. - have hE : E ⊆ A := by - intro x; simp [E]; by_contra!; specialize hfA x this.2; tauto + have hE : E ⊆ A := by intro _; simp [E]; by_contra!; aesop -- Now, we map A back to the natural numbers, thus identifying E with a subset E' of ℕ. obtain ⟨ g, hg ⟩ := hA.symm - have hsum := Sum.eq hg (AbsConvergent.comp hg hconv') + have hsum := Sum.eq hg (hconv'.comp hg) set E' := { n | ↑(g n) ∈ E } - set ι : E' → E := fun ⟨ n, hn ⟩ ↦ ⟨ (g n).val, by aesop ⟩ + set ι : E' → E := fun ⟨ n, hn ⟩ ↦ ⟨ g n, by aesop ⟩ have hι: Function.Bijective ι := by constructor - . intro ⟨ n, hn ⟩ ⟨ m, hm ⟩ h; simp [ι, E', Subtype.val_inj] at hn hm h ⊢; exact hg.1 h + . intro ⟨ n, hn ⟩ ⟨ m, hm ⟩ h; simp [ι, E', Subtype.val_inj] at *; exact hg.1 h . intro ⟨ x, hx ⟩; obtain ⟨ n, hn ⟩ := hg.2 ⟨ x, hE hx ⟩; use ⟨ n, by aesop ⟩; simp [ι, hn] -- The cases of infinite and finite E' are handled separately. rcases Nat.atMostCountable_subset E' with hE' | hE' @@ -296,59 +294,51 @@ theorem Sum'.of_countable_supp {X:Type} {f:X → ℝ} {A: Set X} (hA: CountablyI set hinf : Infinite E' := hE'.toInfinite obtain ⟨ a, ha_bij, ha_mono ⟩ := (Nat.monotone_enum_of_infinite E').exists have : Filter.atTop.Tendsto (Nat.cast ∘ Subtype.val ∘ a: ℕ → ℤ) .atTop := by - apply tendsto_natCast_atTop_atTop.comp - apply StrictMono.tendsto_atTop - intro n m hnm; simp [ha_mono hnm] - replace hsum := hsum.comp this - apply tendsto_nhds_unique _ hsum + apply tendsto_natCast_atTop_atTop.comp (StrictMono.tendsto_atTop _) + intro _ _ hnm; simp [ha_mono hnm] + apply tendsto_nhds_unique _ (hsum.comp this) have hconv'' : AbsConvergent (fun x:E ↦ f x) := by rw [←AbsConvergent'.of_countable] . exact hconv.subtype E apply (CountablyInfinite.equiv _).mp hE'; use ι replace := Sum.eq (hι.comp ha_bij) (hconv''.comp (hι.comp ha_bij)) - replace := this.comp tendsto_natCast_atTop_atTop - convert this using 1; ext N + convert this.comp tendsto_natCast_atTop_atTop using 1; ext N simp [Series.partial, ι] calc _ = ∑ x ∈ .image (Subtype.val ∘ a) (.Icc 0 N), f ↑(g x) := by - apply (Finset.sum_subset _ _).symm - . intro m hm; simp at hm ⊢ - obtain ⟨ n, hn, rfl ⟩ := hm + symm; apply Finset.sum_subset + . intro m hm; simp at hm ⊢; obtain ⟨ n, hn, rfl ⟩ := hm simp [ha_mono.monotone hn] - intro x hx hx'; simp at hx hx' - contrapose! hx' - obtain ⟨ n, hn ⟩ := (hι.comp ha_bij).2 ⟨ ↑(g x), hx' ⟩ + intro x hx hx'; simp at hx hx'; contrapose! hx' + obtain ⟨ n, hn ⟩ := (hι.comp ha_bij).2 ⟨ g x, hx' ⟩ simp [ι, Subtype.val_inj] at hn replace hn := hg.1 hn; subst hn use n; simpa [ha_mono.le_iff_le] using hx _ = _ := by - apply Finset.sum_image _ - intro n hn m hm h - simp [Subtype.val_inj] at h - exact ha_bij.1 h + apply Finset.sum_image + intro _ _ _ _ h; simp [Subtype.val_inj] at h; exact ha_bij.1 h -- When E' is finite, we show that all sufficiently large partial sums of A are equal to -- the sum of E'. let hEfin : Finite E := hι.finite_iff.mp hE' let hE'fintype : Fintype E' := .ofFinite _ let hEfintype : Fintype E := .ofFinite _ - apply Series.convergesTo_uniq _ hsum + apply convergesTo_uniq _ hsum simp [Sum.of_finite, Series.convergesTo] apply tendsto_nhds_of_eventually_eq have hE'bound : BddAbove E' := Set.Finite.bddAbove hE' rw [bddAbove_def] at hE'bound; obtain ⟨ N, hN ⟩ := hE'bound rw [Filter.eventually_atTop] use N; intro N' hN' - have : N' ≥ 0 := by apply LE.le.trans _ hN'; positivity - lift N' to ℕ using this + lift N' to ℕ using (LE.le.trans (by positivity) hN') simp [Series.partial] at hN' ⊢ calc - _ = ∑ n ∈ E', f ↑(g n) := by - apply (Finset.sum_subset _ _).symm - . intro x hx; simp at hx ⊢; linarith [hN x hx] + _ = ∑ n ∈ E', f (g n) := by + symm; apply Finset.sum_subset + . intro x hx; simp at hx ⊢; linarith [hN _ hx] intro _ _ hx'; simpa [E',E] using hx' - _ = ∑ n:E', f ↑(g ↑n) := by convert (Finset.sum_set_coe _).symm - _ = ∑ n, f ↑(ι n) := by apply Finset.sum_congr rfl; intros; simp [ι] - _ = _ := hι.sum_comp (g := fun x ↦ f ↑x) + _ = ∑ n:E', f (g n) := by convert (Finset.sum_set_coe _).symm + _ = ∑ n, f (ι n) := Finset.sum_congr rfl (by intros; simp [ι]) + _ = _ := hι.sum_comp (g := fun x ↦ f x) /-- Connection with Mathlib's `Summable` property. Some version of this might be suitable for Mathlib? -/ @@ -384,7 +374,7 @@ theorem Filter.Eventually.int_natCast_atTop (p: ℤ → Prop) : refine ⟨ Filter.Eventually.natCast_atTop, ?_ ⟩ simp [Filter.eventually_atTop] intro N hN; use N; intro n hn - lift n to ℕ using (by apply LE.le.trans (by positivity) hn) + lift n to ℕ using (by omega) simp at hn; solve_by_elim theorem Filter.Tendsto.int_natCast_atTop {R:Type} (f: ℤ → R) (l: Filter R) : @@ -407,7 +397,7 @@ theorem Sum'.eq_tsum {X:Type} (f:X → ℝ) (h: AbsConvergent' f) : simp [←AbsConvergent'.of_countable hE,] exact h.subtype E replace this := Sum.eq hg this - convert Series.convergesTo_uniq this _ + convert convergesTo_uniq this _ replace : ∑' x, f x = ∑' n, f (g n) := calc _ = ∑' x:E, f x := by rw [←tsum_univ f] @@ -415,7 +405,7 @@ theorem Sum'.eq_tsum {X:Type} (f:X → ℝ) (h: AbsConvergent' f) : convert (tsum_setElem_eq_tsum_setElem_diff _ {x | f x = 0} (by aesop)) _ = _ := (Equiv.tsum_eq (Equiv.ofBijective _ hg) _).symm rw [this] - unfold Series.convergesTo + unfold convergesTo rw [Filter.Tendsto.int_natCast_atTop] convert (Summable.tendsto_sum_tsum_nat ?_).comp (Filter.tendsto_add_atTop_nat 1) with n . ext N; simp [Series.partial, Nat.range_succ_eq_Icc_zero] @@ -460,14 +450,14 @@ theorem Sum'.of_comp {X Y:Type} {f:X → ℝ} (hf: AbsConvergent' f) {φ: Y → sorry /-- Lemma 8.2.7 / Exercise 8.2.4 -/ -theorem Series.divergent_parts_of_divergent {a: ℕ → ℝ} (ha: (a:Series).converges) +theorem divergent_parts_of_divergent {a: ℕ → ℝ} (ha: (a:Series).converges) (ha': ¬ (a:Series).absConverges) : ¬ AbsConvergent (fun n : {n | a n ≥ 0} ↦ a n) ∧ ¬ AbsConvergent (fun n : {n | a n < 0} ↦ a n) := by sorry /-- Theorem 8.2.8 (Riemann rearrangement theorem) / Exercise 8.2.5 -/ -theorem Series.permute_convergesTo_of_divergent {a: ℕ → ℝ} (ha: (a:Series).converges) +theorem permute_convergesTo_of_divergent {a: ℕ → ℝ} (ha: (a:Series).converges) (ha': ¬ (a:Series).absConverges) (L:ℝ) : ∃ f : ℕ → ℕ, Function.Bijective f ∧ (a ∘ f:Series).convergesTo L := by @@ -506,12 +496,12 @@ theorem Series.permute_convergesTo_of_divergent {a: ℕ → ℝ} (ha: (a:Series) refine ⟨ ⟨ hn'_inj, hn'_surj ⟩, ?_ ⟩; convert hsum /-- Exercise 8.2.6 -/ -theorem Series.permute_diverges_of_divergent {a: ℕ → ℝ} (ha: (a:Series).converges) +theorem permute_diverges_of_divergent {a: ℕ → ℝ} (ha: (a:Series).converges) (ha': ¬ (a:Series).absConverges) : ∃ f : ℕ → ℕ, Function.Bijective f ∧ Filter.atTop.Tendsto (fun N ↦ ((a ∘ f:Series).partial N : EReal)) (nhds ⊤) := by sorry -theorem Series.permute_diverges_of_divergent' {a: ℕ → ℝ} (ha: (a:Series).converges) +theorem permute_diverges_of_divergent' {a: ℕ → ℝ} (ha: (a:Series).converges) (ha': ¬ (a:Series).absConverges) : ∃ f : ℕ → ℕ, Function.Bijective f ∧ Filter.atTop.Tendsto (fun N ↦ ((a ∘ f:Series).partial N : EReal)) (nhds ⊥) := by sorry