From edb5cabc9c1f288f03587d3e1fa8a2f3bdcbf4df Mon Sep 17 00:00:00 2001 From: Taksh Date: Sat, 18 Jul 2026 19:08:35 +0300 Subject: [PATCH] fix: insert missing space before Verso docstring closers MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit Several /-- …-/ comments lacked a space before -/, so they were not valid one-line Verso/Lean docstrings. Co-authored-by: Cursor --- Analysis/Appendix_A_4.lean | 2 +- Analysis/MeasureTheory/Section_1_2_2.lean | 32 +++++++++++------------ Analysis/MeasureTheory/Section_1_3_4.lean | 2 +- Analysis/Misc/UnitsSystem.lean | 4 +-- Analysis/Misc/UnitsSystemExamples.lean | 2 +- Analysis/Misc/erdos_379.lean | 8 +++--- Analysis/Section_10_5.lean | 2 +- Analysis/Section_11_1.lean | 2 +- Analysis/Section_11_10.lean | 4 +-- Analysis/Section_11_4.lean | 2 +- Analysis/Section_11_5.lean | 2 +- Analysis/Section_2_1.lean | 2 +- Analysis/Section_2_2.lean | 4 +-- Analysis/Section_2_3.lean | 2 +- Analysis/Section_2_epilogue.lean | 2 +- Analysis/Section_3_1.lean | 8 +++--- Analysis/Section_3_5.lean | 2 +- Analysis/Section_4_3.lean | 4 +-- Analysis/Section_5_4.lean | 4 +-- Analysis/Section_5_5.lean | 2 +- Analysis/Section_6_1.lean | 4 +-- Analysis/Section_6_3.lean | 2 +- Analysis/Section_8_2.lean | 8 +++--- Analysis/Section_8_5.lean | 4 +-- Analysis/Section_9_1.lean | 6 ++--- 25 files changed, 58 insertions(+), 58 deletions(-) diff --git a/Analysis/Appendix_A_4.lean b/Analysis/Appendix_A_4.lean index 171f1e68a..e5fa04122 100644 --- a/Analysis/Appendix_A_4.lean +++ b/Analysis/Appendix_A_4.lean @@ -51,7 +51,7 @@ example : ∀ (x:ℝ), (x+1)^2 = x^2 + 2*x + 1 := by end VariableExample2 -/-- A dummy statement is in place here for this example.-/ +/-- A dummy statement is in place here for this example. -/ example : 0 = 0 := by set x := 342 have : x + 155 = 497 := by diff --git a/Analysis/MeasureTheory/Section_1_2_2.lean b/Analysis/MeasureTheory/Section_1_2_2.lean index 6103ad3f6..544f57d31 100644 --- a/Analysis/MeasureTheory/Section_1_2_2.lean +++ b/Analysis/MeasureTheory/Section_1_2_2.lean @@ -355,7 +355,7 @@ theorem IsClosed.measurable {d:ℕ} {E: Set (EuclideanSpace' d)} (hE: IsClosed E abbrev IsNull {d:ℕ} (E: Set (EuclideanSpace' d)) : Prop := Lebesgue_outer_measure E = 0 -/-- Lemma 1.2.13(iii) (Every null set is Lebesgue measurable).-/ +/-- Lemma 1.2.13(iii) (Every null set is Lebesgue measurable). -/ theorem IsNull.measurable {d:ℕ} {E: Set (EuclideanSpace' d)} (hE: IsNull E) : LebesgueMeasurable E := by -- Strategy: For any ε > 0, since m*(E) = 0, get a box cover with total volume < ε, -- then inflate boxes to open sets. The union is open and contains E. @@ -518,7 +518,7 @@ lemma IsNull.subset {d:ℕ} {E F : Set (EuclideanSpace' d)} (hE : IsNull E) (hFE rw [hE] at this exact le_antisymm this (Lebesgue_outer_measure.nonneg F) -/-- Lemma 1.2.13(iv) (Empty set is measurable).-/ +/-- Lemma 1.2.13(iv) (Empty set is measurable). -/ theorem LebesgueMeasurable.empty {d:ℕ} : LebesgueMeasurable (∅: Set (EuclideanSpace' d)) := -- use (i) directly IsOpen.measurable isOpen_empty @@ -536,7 +536,7 @@ theorem LebesgueMeasurable.empty' {d:ℕ} : LebesgueMeasurable (∅: Set (Euclid rw [Lebesgue_outer_measure.of_empty d] exact le_of_lt hε -/-- Lemma 1.2.13(vi) (Countable union of measurable sets is measurable).-/ +/-- Lemma 1.2.13(vi) (Countable union of measurable sets is measurable). -/ theorem LebesgueMeasurable.countable_union {d:ℕ} {E: ℕ → Set (EuclideanSpace' d)} (hE: ∀ n, LebesgueMeasurable (E n)) : LebesgueMeasurable (⋃ n, E n) := by -- Use the ε/2^n trick: let ε > 0 be arbitrary intro ε hε @@ -901,7 +901,7 @@ lemma LebesgueMeasurable.closedBall {d : ℕ} (c : EuclideanSpace' d) (r : ℝ) LebesgueMeasurable (Metric.closedBall c r) := Metric.isClosed_closedBall.measurable -/-- Exercise 1.2.7 (Criteria for measurability)-/ +/-- Exercise 1.2.7 (Criteria for measurability) -/ theorem LebesgueMeasurable.TFAE {d:ℕ} (E: Set (EuclideanSpace' d)) : [ LebesgueMeasurable E, @@ -932,7 +932,7 @@ theorem CantorSet.uncountable : Uncountable CantorSet := by theorem CantorSet.null : IsNull (Real.equiv_EuclideanSpace' '' CantorSet) := by sorry -/-- Exercise 1.2.10 (\[0,1) is not the countable union of pairwise disjoint closed intervals)-/ +/-- Exercise 1.2.10 (\[0,1) is not the countable union of pairwise disjoint closed intervals) -/ example : ¬ ∃ (I: ℕ → BoundedInterval), (∀ n, IsClosed (I n).toSet) ∧ (Set.univ.PairwiseDisjoint (fun n ↦ (I n).toSet) ) ∧ (⋃ n, (I n).toSet = Set.Ico 0 1) := by sorry @@ -1636,15 +1636,15 @@ theorem Lebesgue_measure.union {d:ℕ} {E F: Set (EuclideanSpace' d)} (hE: Lebes rw [tsum_fintype] simp only [S, Fin.sum_univ_two, Fin.isValue, Matrix.cons_val_zero, Matrix.cons_val_one] -/-- Exercise 1.2.11(a) (Upward monotone convergence)-/ +/-- Exercise 1.2.11(a) (Upward monotone convergence) -/ theorem Lebesgue_measure.upward_monotone_convergence {d:ℕ} {E: ℕ → Set (EuclideanSpace' d)} (hE: ∀ n, LebesgueMeasurable (E n)) (hmono: ∀ n, E n ⊆ E (n + 1)) : Filter.atTop.Tendsto (fun n ↦ Lebesgue_measure (E n)) (nhds (Lebesgue_measure (⋃ n, E n))) := by sorry -/-- Exercise 1.2.11(b) (Downward monotone convergence)-/ +/-- Exercise 1.2.11(b) (Downward monotone convergence) -/ theorem Lebesgue_measure.downward_monotone_convergence {d:ℕ} {E: ℕ → Set (EuclideanSpace' d)} (hE: ∀ n, LebesgueMeasurable (E n)) (hmono: ∀ n, E (n+1) ⊆ E n) (hfin: ∃ n, Lebesgue_measure (E n) < ⊤) : Filter.atTop.Tendsto (fun n ↦ Lebesgue_measure (E n)) (nhds (Lebesgue_measure (⋂ n, E n))) := by sorry -/-- Exercise 1.2.11 (c) (counterexample)-/ +/-- Exercise 1.2.11 (c) (counterexample) -/ example : ∃ (d:ℕ) (E: ℕ → Set (EuclideanSpace' d)) (hE: ∀ n, LebesgueMeasurable (E n)) (hmono: ∀ n, E (n+1) ⊆ E n), ¬ Filter.atTop.Tendsto (fun n ↦ Lebesgue_measure (E n)) (nhds (Lebesgue_measure (⋂ n, E n))) := by sorry /-- Exercise 1.2.12(a) -/ @@ -1679,11 +1679,11 @@ example : ∃ (d:ℕ) (E: ℕ → Set (EuclideanSpace' d)) (E₀ F: Set (Euclide /-- Exercise 1.2.14 -/ example {d:ℕ} (E: Set (EuclideanSpace' d)) : ∃ (F: Set (EuclideanSpace' d)), E ⊆ F ∧ LebesgueMeasurable F ∧ Lebesgue_measure F = Lebesgue_outer_measure E := by sorry -/-- Exercise 1.2.15 (Inner regularity)-/ +/-- Exercise 1.2.15 (Inner regularity) -/ theorem Lebesgue_measure.eq {d:ℕ} {E: Set (EuclideanSpace' d)} (hE: LebesgueMeasurable E): Lebesgue_measure E = sSup { M | ∃ K, K ⊆ E ∧ IsCompact K ∧ M = Lebesgue_measure K} := by sorry -/-- Exercise 1.2.16 (Criteria for finite measure)-/ +/-- Exercise 1.2.16 (Criteria for finite measure) -/ theorem LebesgueMeasurable.finite_TFAE {d:ℕ} (E: Set (EuclideanSpace' d)) : [ LebesgueMeasurable E ∧ Lebesgue_measure E < ⊤, @@ -1698,7 +1698,7 @@ theorem LebesgueMeasurable.finite_TFAE {d:ℕ} (E: Set (EuclideanSpace' d)) : ].TFAE := by sorry -/-- Exercise 1.2.17 (Caratheodory criterion one direction)-/ +/-- Exercise 1.2.17 (Caratheodory criterion one direction) -/ theorem LebesgueMeasurable.caratheodory {d:ℕ} (E: Set (EuclideanSpace' d)) : [ LebesgueMeasurable E, @@ -1711,17 +1711,17 @@ theorem Bornology.IsBounded.inElementary {d:ℕ} {E: Set (EuclideanSpace' d)} (h noncomputable def inner_measure {d:ℕ} {E: Set (EuclideanSpace' d)} (hE: Bornology.IsBounded E) : ℝ := (Lebesgue_measure hE.inElementary.choose).toReal - (Lebesgue_measure (hE.inElementary.choose \ E)).toReal -/-- Exercise 1.2.18(i) (Inner measure)-/ +/-- Exercise 1.2.18(i) (Inner measure) -/ theorem inner_measure.eq {d:ℕ} {E A: Set (EuclideanSpace' d)} (hE: Bornology.IsBounded E) (hA: IsElementary A) (hsub: E ⊆ A) : inner_measure hE = Lebesgue_measure A - Lebesgue_outer_measure (A \ E) := by sorry -/-- Exercise 1.2.18(ii) (Inner measure)-/ +/-- Exercise 1.2.18(ii) (Inner measure) -/ theorem inner_measure.le {d:ℕ} {E: Set (EuclideanSpace' d)} (hE: Bornology.IsBounded E) : inner_measure hE ≤ Lebesgue_outer_measure E := by sorry -/-- Exercise 1.2.18(iii) (Inner measure)-/ +/-- Exercise 1.2.18(iii) (Inner measure) -/ theorem inner_measure.eq_iff {d:ℕ} {E: Set (EuclideanSpace' d)} (hE: Bornology.IsBounded E) : inner_measure hE = Lebesgue_outer_measure E ↔ LebesgueMeasurable E := by sorry @@ -1780,7 +1780,7 @@ theorem Lebesgue_measure.unique {d:ℕ} (m: Set (EuclideanSpace' d) → EReal) (hnorm: m (Box.unit_cube d) = 1) : ∀ E, LebesgueMeasurable E → m E = Lebesgue_measure E := by sorry -/-- Exercise 1.2.24(i) (Lebesgue measure as the completion of elementary measure)-/ +/-- Exercise 1.2.24(i) (Lebesgue measure as the completion of elementary measure) -/ instance IsElementary.ae_equiv {d:ℕ} {A: Set (EuclideanSpace' d)} (hA: IsElementary A): Setoid (Set A) := { r E F := IsNull (Subtype.val '' (_root_.symmDiff E F)) @@ -1817,7 +1817,7 @@ noncomputable def IsElementary.ae_measure {d:ℕ} {A: Set (EuclideanSpace' d)} ( noncomputable def IsElementary.ae_elem_measure {d:ℕ} {A: Set (EuclideanSpace' d)} (hA: IsElementary A) (E: hA.ae_elem) : ℝ := E.property.choose_spec.1.measure -/-- Exercise 1.2.24(iv) (Lebesgue measure as the completion of elementary measure)-/ +/-- Exercise 1.2.24(iv) (Lebesgue measure as the completion of elementary measure) -/ theorem IsElementary.ae_measure_eq_completion {d:ℕ} {A: Set (EuclideanSpace' d)} (hA: IsElementary A) (m: hA.ae_subsets → ℝ) : ContinuousOn m hA.ae_measurable ∧ (∀ (E:hA.ae_elem), m E.val = hA.ae_elem_measure E) ↔ (∀ (E:hA.ae_measurable), m E.val = hA.ae_measure E) := by sorry diff --git a/Analysis/MeasureTheory/Section_1_3_4.lean b/Analysis/MeasureTheory/Section_1_3_4.lean index ea2c0ce4d..e00e5490f 100644 --- a/Analysis/MeasureTheory/Section_1_3_4.lean +++ b/Analysis/MeasureTheory/Section_1_3_4.lean @@ -1024,7 +1024,7 @@ theorem RiemannIntegrableOn.realAbsolutelyIntegrable {I: BoundedInterval} {f: theorem RiemannIntegral.eq_integ {I: BoundedInterval} {f: ℝ → ℝ} (hf: RiemannIntegrableOn f I) : riemannIntegral f I = hf.realAbsolutelyIntegrable.integ := by sorry -/-- Exercise 1.3.21 (Absolute summability is a special case of absolute integrability)-/ +/-- Exercise 1.3.21 (Absolute summability is a special case of absolute integrability) -/ theorem AbsolutelySummable.realAbsolutelyIntegrable_iff {a: ℤ → ℝ} : ∑' n, |a n|.toEReal < ⊤ ↔ RealAbsolutelyIntegrable (fun x ↦ a ⌊EuclideanSpace'.equiv_Real x⌋) := by sorry theorem AbsolutelySummable.complexAbsolutelyIntegrable_iff {a: ℤ → ℂ} : ∑' n, ‖a n‖.toEReal < ⊤ ↔ ComplexAbsolutelyIntegrable (fun x ↦ a ⌊EuclideanSpace'.equiv_Real x⌋) := by sorry diff --git a/Analysis/Misc/UnitsSystem.lean b/Analysis/Misc/UnitsSystem.lean index 29aec3406..1d56adef9 100644 --- a/Analysis/Misc/UnitsSystem.lean +++ b/Analysis/Misc/UnitsSystem.lean @@ -300,7 +300,7 @@ theorem Scalar.toFormal_hMul {d₁ d₂:Dimensions} (q₁:Scalar d₁) (q₂:Sca not to do this, implementing an inversion relation instead. -/ noncomputable def Scalar.pow {d:Dimensions} (q: Scalar d) (n:ℕ) : Scalar (n • d) := ⟨ q.val^n ⟩ -/-- {given -show}`n : ℕ, d` One cannot use the Mathlib classes {name}`Pow` or {name}`HPow` here because the output type {lean}`Scalar (n • d)` depends on the input {name}`n`. As the symbol {kw (of := «term_^_»)}`^` is reserved for such classes, we use the symbol `**` instead.-/ +/-- {given -show}`n : ℕ, d` One cannot use the Mathlib classes {name}`Pow` or {name}`HPow` here because the output type {lean}`Scalar (n • d)` depends on the input {name}`n`. As the symbol {kw (of := «term_^_»)}`^` is reserved for such classes, we use the symbol `**` instead. -/ infix:80 "**" => Scalar.pow @[simp] @@ -346,7 +346,7 @@ theorem Scalar.mul_inv {d₁ d₂:Dimensions} (q₁:Scalar d₁) (q₂:Scalar d theorem Scalar.pow_inv {d:Dimensions} (q:Scalar d) (n:ℕ) : (q ** n).inv = (q.inv ** n).cast := by simp [←toFormal_inj, toFormal] -/-- Multiplication and inversion combine to give division in the usual fashion.-/ +/-- Multiplication and inversion combine to give division in the usual fashion. -/ noncomputable instance Scalar.instHDiv {d₁ d₂:Dimensions} : HDiv (Scalar d₁) (Scalar d₂) (Scalar (d₁ - d₂)) where hDiv q₁ q₂ := ⟨q₁.val / q₂.val⟩ diff --git a/Analysis/Misc/UnitsSystemExamples.lean b/Analysis/Misc/UnitsSystemExamples.lean index 5b0f41fa3..36f2101e6 100644 --- a/Analysis/Misc/UnitsSystemExamples.lean +++ b/Analysis/Misc/UnitsSystemExamples.lean @@ -27,6 +27,6 @@ theorem UnitsSystem.Scalar.right_distrib {d₁ d₂:Dimensions} (a b:Scalar d₁ theorem UnitsSystem.Scalar.sq_add {d:Dimensions} (a b:Scalar d) : (a+b)**2 = a**2 + (2 • a * b).cast + b**2 := by simp [←toFormal_inj]; ring -/-- An alternate proof based on working in coordinates-/ +/-- An alternate proof based on working in coordinates -/ theorem UnitsSystem.Scalar.sq_add' {d:Dimensions} (a b:Scalar d) : (a+b)**2 = a**2 + (2 • a * b).cast + b**2 := by simp [←val_inj]; ring diff --git a/Analysis/Misc/erdos_379.lean b/Analysis/Misc/erdos_379.lean index 764c2ecb0..0d4c04fdd 100644 --- a/Analysis/Misc/erdos_379.lean +++ b/Analysis/Misc/erdos_379.lean @@ -12,7 +12,7 @@ theorem binom_eq {n k:ℕ} (hk: 1 ≤ k) : (n.choose k) * k = ((n-1).choose (k-1 all_goals omega simp [choose_eq_zero_of_lt hn, choose_eq_zero_iff]; omega -/-- $$`\binom\{n\}\{k\} \cdot k \cdot (k-1) = \binom\{n-2\}\{k-2\} \cdot (n-1) \cdot n`.-/ +/-- $$`\binom\{n\}\{k\} \cdot k \cdot (k-1) = \binom\{n-2\}\{k-2\} \cdot (n-1) \cdot n`. -/ theorem binom_eq_2 {n k:ℕ} (hk: 2 ≤ k) : (n.choose k) * k * (k-1) = ((n-2).choose (k-2)) * (n-1) * n := calc _ = ((n-1).choose (k-1)) * n * (k-1) := by rw [binom_eq]; omega _ = ((n-1).choose (k-1)) * (k-1) * n := by ring @@ -35,7 +35,7 @@ theorem lemma_2 {n k p r:ℕ} (hk: 2 ≤ k) (hn: k ≤ n) replace h3 : ¬p∣k-1 := by contrapose! h3; convert dvd_sub h1' h3 using 1; omega exact hp.prime.pow_dvd_of_dvd_mul_right _ h2 (hp.prime.pow_dvd_of_dvd_mul_right _ h3 h1) -/-- If $$`n=2^\{\phi(p^R)\}$$ and $$p>2^\{r-1\}$$, then $$2^r \mid \binom\{n\}\{k\}$$ or $$p^R \mid \binom\{n\}\{k\}`.-/ +/-- If $$`n=2^\{\phi(p^R)\}$$ and $$p>2^\{r-1\}$$, then $$2^r \mid \binom\{n\}\{k\}$$ or $$p^R \mid \binom\{n\}\{k\}`. -/ theorem key_prop {k n p r R:ℕ} (hn: n = 2^((p^R).totient)) (hk: 1 ≤ k) (hkn: k < n) (hp: p.Prime) (hpr: p > 2^(r-1)) (hr: 1 < r) (hr' : r ≤ (p^R).totient): @@ -71,7 +71,7 @@ theorem S_ge {n r:ℕ} (hn: 1 < n) (h: ∀ k ∈ Finset.Ico 1 n, ∃ p, p.Prime all_goals grind aesop -/-- If $$p>2^\{r-1\}$$, then $$S(2^\{\phi(p^R)\}) \ge r$$.-/ +/-- If $$p>2^\{r-1\}$$, then $$S(2^\{\phi(p^R)\}) \ge r$$. -/ theorem key_cor {p r:ℕ} (hp: p.Prime) (hpr: p > 2^(r-1)) (hr: 1 < r) : r ≤ S (2^((p^r).totient)) := by apply S_ge; simp; grind @@ -86,7 +86,7 @@ theorem key_cor {p r:ℕ} (hp: p.Prime) (hpr: p > 2^(r-1)) (hr: 1 < r) : . use 2; simp_all [prime_two] use p -/-- A positive resolution to Erdos problem \#379.-/ +/-- A positive resolution to Erdos problem \#379. -/ theorem erdos_379 : Filter.atTop.limsup (fun n ↦ (S n:ENat)) = ⊤ := by rw [Filter.limsup_eq_iInf_iSup_of_nat] simp; intro N; rw [iSup₂_eq_top]; intro r hr; lift r to ℕ using (by order) diff --git a/Analysis/Section_10_5.lean b/Analysis/Section_10_5.lean index d5b2402b9..bbfa9c0b4 100644 --- a/Analysis/Section_10_5.lean +++ b/Analysis/Section_10_5.lean @@ -20,7 +20,7 @@ Main constructions and results of this section: open Chapter9 namespace Chapter10 -/-- Proposition 10.5.1 (L'Hôpital's rule, I) / Exercise 10.5.1-/ +/-- Proposition 10.5.1 (L'Hôpital's rule, I) / Exercise 10.5.1 -/ theorem _root_.Filter.Tendsto.of_div {X: Set ℝ} {f g: ℝ → ℝ} {x₀ f'x₀ g'x₀:ℝ} (hfx₀: f x₀ = 0) (hgx₀: g x₀ = 0) (hg_non: g'x₀ ≠ 0) (hf'x₀: HasDerivWithinAt f f'x₀ X x₀) (hg'x₀: HasDerivWithinAt g g'x₀ X x₀) : diff --git a/Analysis/Section_11_1.lean b/Analysis/Section_11_1.lean index a9334f890..5f71505c2 100644 --- a/Analysis/Section_11_1.lean +++ b/Analysis/Section_11_1.lean @@ -26,7 +26,7 @@ inductive BoundedInterval where open BoundedInterval -/-- There is a technical issue in that this coercion is not injective: the empty set is represented by multiple bounded intervals. This causes some of the statements in this section to be a little uglier than necessary.-/ +/-- There is a technical issue in that this coercion is not injective: the empty set is represented by multiple bounded intervals. This causes some of the statements in this section to be a little uglier than necessary. -/ @[coe] def BoundedInterval.toSet (I: BoundedInterval) : Set ℝ := match I with | Ioo a b => .Ioo a b diff --git a/Analysis/Section_11_10.lean b/Analysis/Section_11_10.lean index 06d0c3342..27bdcef4c 100644 --- a/Analysis/Section_11_10.lean +++ b/Analysis/Section_11_10.lean @@ -125,7 +125,7 @@ theorem RS_integ_eq_integ_of_mul_deriv upper_integral (f * α') (Icc a b) := lower_integral_le_upper hfα'_bound refine ⟨ ⟨ hfα'_bound, ?_ ⟩, ?_ ⟩ <;> linarith -/-- Lemma 11.10.5 / Exercise 11.10.2-/ +/-- Lemma 11.10.5 / Exercise 11.10.2 -/ theorem PiecewiseConstantOn.RS_integ_of_comp {a b:ℝ} (hab: a < b) {φ f:ℝ → ℝ} (hφ_cont: Continuous φ) (hφ_mono: Monotone φ) (hf: PiecewiseConstantOn f (Icc (φ a) (φ b))) : PiecewiseConstantOn (f ∘ φ) (Icc a b) ∧ RS_integ (f ∘ φ) (Icc a b) φ = @@ -218,7 +218,7 @@ theorem integ_of_comp {a b:ℝ} (hab: a < b) {φ f: ℝ → ℝ} have h2 := RS_integ_eq_integ_of_mul_deriv hab hφ_mono hφ_diff hφ_cont hφ' h1.1 refine ⟨ h2.1, by aesop ⟩ -/-- Exercise 11.10.3-/ +/-- Exercise 11.10.3 -/ example {a b:ℝ} (hab: a < b) {f: ℝ → ℝ} (hf: IntegrableOn f (Icc a b)) : IntegrableOn (fun x ↦ f (-x)) (Icc (-b) (-a)) ∧ integ (fun x ↦ f (-x)) (Icc (-b) (-a)) = integ f (Icc a b) := by diff --git a/Analysis/Section_11_4.lean b/Analysis/Section_11_4.lean index 60c6a367d..fa71d47c0 100644 --- a/Analysis/Section_11_4.lean +++ b/Analysis/Section_11_4.lean @@ -144,7 +144,7 @@ theorem IntegrableOn.max {I: BoundedInterval} {f g:ℝ → ℝ} (hf: IntegrableO -/-- Theorem 11.4.5 / Exercise 11.4.3. The objective here is to create a shorter proof than the one above.-/ +/-- Theorem 11.4.5 / Exercise 11.4.3. The objective here is to create a shorter proof than the one above. -/ theorem IntegrableOn.min {I: BoundedInterval} {f g:ℝ → ℝ} (hf: IntegrableOn f I) (hg: IntegrableOn g I) : IntegrableOn (f ⊓ g) I := by sorry diff --git a/Analysis/Section_11_5.lean b/Analysis/Section_11_5.lean index 188d9b539..29fa52790 100644 --- a/Analysis/Section_11_5.lean +++ b/Analysis/Section_11_5.lean @@ -89,7 +89,7 @@ example : ¬ IntegrableOn (fun x:ℝ ↦ 1/x) (Icc 0 1) := by sorry open PiecewiseConstantOn ConstantOn in set_option maxHeartbeats 300000 in -/-- Proposition 11.5.3-/ +/-- Proposition 11.5.3 -/ theorem integ_of_bdd_cts {I: BoundedInterval} {f:ℝ → ℝ} (hbound: BddOn f I) (hf: ContinuousOn f I) : IntegrableOn f I := by -- This proof is written to follow the structure of the original text. diff --git a/Analysis/Section_2_1.lean b/Analysis/Section_2_1.lean index 6d09df3eb..1472acab1 100644 --- a/Analysis/Section_2_1.lean +++ b/Analysis/Section_2_1.lean @@ -63,7 +63,7 @@ lemma Nat.zero_succ : 0++ = 1 := by rfl lemma Nat.one_succ : 1++ = 2 := by rfl #check (2:Nat) -/-- Proposition 2.1.4 (3 is a natural number)-/ +/-- Proposition 2.1.4 (3 is a natural number) -/ lemma Nat.two_succ : 2++ = 3 := by rfl #check (3:Nat) diff --git a/Analysis/Section_2_2.lean b/Analysis/Section_2_2.lean index d0f003f79..32076d441 100644 --- a/Analysis/Section_2_2.lean +++ b/Analysis/Section_2_2.lean @@ -126,7 +126,7 @@ instance Nat.addCommMonoid : AddCommMonoid Nat where textbook. -/ example (a b c d:Nat) : (a+b)+(c+0+d) = (b+c)+(d+a) := by abel -/-- Definition 2.2.7 (Positive natural numbers).-/ +/-- Definition 2.2.7 (Positive natural numbers). -/ def Nat.IsPos (n:Nat) : Prop := n ≠ 0 theorem Nat.isPos_iff (n:Nat) : n.IsPos ↔ n ≠ 0 := by rfl @@ -269,7 +269,7 @@ theorem Nat.lt_iff_succ_le (a b:Nat) : a < b ↔ a++ ≤ b := by theorem Nat.lt_iff_add_pos (a b:Nat) : a < b ↔ ∃ d:Nat, d.IsPos ∧ b = a + d := by sorry -/-- If a < b then a ̸= b,-/ +/-- If a < b then a ̸= b, -/ theorem Nat.ne_of_lt (a b:Nat) : a < b → a ≠ b := by intro h; exact h.2 diff --git a/Analysis/Section_2_3.lean b/Analysis/Section_2_3.lean index aa322e4b4..51017219c 100644 --- a/Analysis/Section_2_3.lean +++ b/Analysis/Section_2_3.lean @@ -209,7 +209,7 @@ theorem Nat.pow_succ (m n: Nat) : (m:Nat) ^ n++ = m^n * m := theorem Nat.pow_one (m: Nat) : m ^ (1:Nat) = m := by rw [←zero_succ, pow_succ]; simp -/-- Exercise 2.3.4-/ +/-- Exercise 2.3.4 -/ theorem Nat.sq_add_eq (a b: Nat) : (a + b) ^ (2 : Nat) = a ^ (2 : Nat) + 2 * a * b + b ^ (2 : Nat) := by sorry diff --git a/Analysis/Section_2_epilogue.lean b/Analysis/Section_2_epilogue.lean index f06aebd77..7bdcb207c 100644 --- a/Analysis/Section_2_epilogue.lean +++ b/Analysis/Section_2_epilogue.lean @@ -170,7 +170,7 @@ theorem Equiv.uniq {P Q : PeanoAxioms} (equiv1 equiv2 : PeanoAxioms.Equiv P Q) : ext n sorry -/-- A sample result: recursion is well-defined on any structure obeying the Peano axioms-/ +/-- A sample result: recursion is well-defined on any structure obeying the Peano axioms -/ theorem Nat.recurse_uniq {P : PeanoAxioms} (f: P.Nat → P.Nat → P.Nat) (c: P.Nat) : ∃! (a: P.Nat → P.Nat), a P.zero = c ∧ ∀ n, a (P.succ n) = f n (a n) := by sorry diff --git a/Analysis/Section_3_1.lean b/Analysis/Section_3_1.lean index 79e182286..2a624eeb7 100644 --- a/Analysis/Section_3_1.lean +++ b/Analysis/Section_3_1.lean @@ -793,15 +793,15 @@ theorem SetTheory.Set.union_eq_partition (A B:Set) : A ∪ B = (A \ B) ∪ (A theorem SetTheory.Set.specification_from_replacement {A:Set} {P: A → Prop} : ∃ B, B ⊆ A ∧ ∀ x, x.val ∈ B ↔ P x := by sorry -/-- Exercise 3.1.12.-/ +/-- Exercise 3.1.12. -/ theorem SetTheory.Set.subset_union_subset {A B A' B':Set} (hA'A: A' ⊆ A) (hB'B: B' ⊆ B) : A' ∪ B' ⊆ A ∪ B := by sorry -/-- Exercise 3.1.12.-/ +/-- Exercise 3.1.12. -/ theorem SetTheory.Set.subset_inter_subset {A B A' B':Set} (hA'A: A' ⊆ A) (hB'B: B' ⊆ B) : A' ∩ B' ⊆ A ∩ B := by sorry -/-- Exercise 3.1.12.-/ +/-- Exercise 3.1.12. -/ theorem SetTheory.Set.subset_diff_subset_counter : ∃ (A B A' B':Set), (A' ⊆ A) ∧ (B' ⊆ B) ∧ ¬ (A' \ B') ⊆ (A \ B) := by sorry @@ -869,7 +869,7 @@ theorem SetTheory.Set.coe_subtype (X: Set) : (X : _root_.Set Object) = X.toSubt theorem SetTheory.Set.coe_intersection (X Y: Set) : ((X ∩ Y:Set) : _root_.Set Object) = (X : _root_.Set Object) ∩ (Y : _root_.Set Object) := by sorry -/-- Compatibility of set difference-/ +/-- Compatibility of set difference -/ theorem SetTheory.Set.coe_diff (X Y: Set) : ((X \ Y:Set) : _root_.Set Object) = (X : _root_.Set Object) \ (Y : _root_.Set Object) := by sorry diff --git a/Analysis/Section_3_5.lean b/Analysis/Section_3_5.lean index 7fb747590..4ab6ac01b 100644 --- a/Analysis/Section_3_5.lean +++ b/Analysis/Section_3_5.lean @@ -472,7 +472,7 @@ theorem SetTheory.Set.direct_sum {X Y Z:Set} (f: Z → X) (g: Z → Y) : theorem SetTheory.Set.iProd_empty_iff {n:ℕ} {X: Fin n → Set} : iProd X = ∅ ↔ ∃ i, X i = ∅ := by sorry -/-- Exercise 3.5.9-/ +/-- Exercise 3.5.9 -/ theorem SetTheory.Set.iUnion_inter_iUnion {I J: Set} (A: I → Set) (B: J → Set) : (iUnion I A) ∩ (iUnion J B) = iUnion (I ×ˢ J) (fun p ↦ (A (fst p)) ∩ (B (snd p))) := by sorry diff --git a/Analysis/Section_4_3.lean b/Analysis/Section_4_3.lean index 9e7432a3a..619df48ea 100644 --- a/Analysis/Section_4_3.lean +++ b/Analysis/Section_4_3.lean @@ -173,12 +173,12 @@ theorem close_mul_mul' {ε δ x y z w:ℚ} (hxy: ε.Close x y) (hzw: δ.Close z (ε*|z|+δ*|y|).Close (x * z) (y * w) := by sorry -/-- Definition 4.3.9 (exponentiation). Here we use the Mathlib definition.-/ +/-- Definition 4.3.9 (exponentiation). Here we use the Mathlib definition. -/ lemma pow_zero (x:ℚ) : x^0 = 1 := _root_.pow_zero x example : (0:ℚ)^0 = 1 := pow_zero 0 -/-- Definition 4.3.9 (exponentiation). Here we use the Mathlib definition.-/ +/-- Definition 4.3.9 (exponentiation). Here we use the Mathlib definition. -/ lemma pow_succ (x:ℚ) (n:ℕ) : x^(n+1) = x^n * x := _root_.pow_succ x n /-- Proposition 4.3.10(a) (Properties of exponentiation, I) / Exercise 4.3.3 -/ diff --git a/Analysis/Section_5_4.lean b/Analysis/Section_5_4.lean index b1a0dbf6d..f2d2c0d71 100644 --- a/Analysis/Section_5_4.lean +++ b/Analysis/Section_5_4.lean @@ -106,7 +106,7 @@ theorem Real.not_pos_neg (x:Real) : ¬(x.IsPos ∧ x.IsNeg) := by sorry @[simp] theorem Real.neg_iff_pos_of_neg (x:Real) : x.IsNeg ↔ (-x).IsPos := by sorry -/-- Proposition 5.4.4 (basic properties of positive reals) / Exercise 5.4.1-/ +/-- Proposition 5.4.4 (basic properties of positive reals) / Exercise 5.4.1 -/ theorem Real.pos_add {x y:Real} (hx: x.IsPos) (hy: y.IsPos) : (x+y).IsPos := by sorry /-- Proposition 5.4.4 (basic properties of positive reals) / Exercise 5.4.1 -/ @@ -246,7 +246,7 @@ instance Real.instIsStrictOrderedRing : IsStrictOrderedRing Real where le_of_add_le_add_left := by sorry zero_le_one := by sorry -/-- Proposition 5.4.9 (The non-negative reals are closed)-/ +/-- Proposition 5.4.9 (The non-negative reals are closed) -/ theorem Real.LIM_of_nonneg {a: ℕ → ℚ} (ha: ∀ n, a n ≥ 0) (hcauchy: (a:Sequence).IsCauchy) : LIM a ≥ 0 := by -- This proof is written to follow the structure of the original text. diff --git a/Analysis/Section_5_5.lean b/Analysis/Section_5_5.lean index ad751358c..2861a06a8 100644 --- a/Analysis/Section_5_5.lean +++ b/Analysis/Section_5_5.lean @@ -304,7 +304,7 @@ theorem Real.exist_irrational : ∃ x:Real, ¬ ∃ q:ℚ, x = (q:Real) := by sor /-- Helper lemma for Exercise 5.5.1. -/ theorem Real.mem_neg (E: Set Real) (x:Real) : x ∈ -E ↔ -x ∈ E := Set.mem_neg -/-- Exercise 5.5.1-/ +/-- Exercise 5.5.1 -/ theorem Real.inf_neg {E: Set Real} {M:Real} (h: IsLUB E M) : IsGLB (-E) (-M) := by sorry theorem Real.GLB_exist {E: Set Real} (hE: Set.Nonempty E) (hbound: BddBelow E): ∃ S, IsGLB E S := by diff --git a/Analysis/Section_6_1.lean b/Analysis/Section_6_1.lean index 3b6324f40..62fcd024c 100644 --- a/Analysis/Section_6_1.lean +++ b/Analysis/Section_6_1.lean @@ -301,7 +301,7 @@ noncomputable abbrev lim (a:Sequence) : ℝ := if h: a.Convergent then h.choose theorem Sequence.lim_def {a:Sequence} (h: a.Convergent) : a.TendsTo (lim a) := by simp [lim, h]; exact h.choose_spec -/-- Definition 6.1.8-/ +/-- Definition 6.1.8 -/ theorem Sequence.lim_eq {a:Sequence} {L:ℝ} : a.TendsTo L ↔ a.Convergent ∧ lim a = L := by constructor @@ -349,7 +349,7 @@ example : ¬ ((fun n ↦ (-1:ℝ)^n):Sequence).IsCauchy := by sorry /-- Example 6.1.13 -/ example : ¬ ((fun n ↦ (-1:ℝ)^n):Sequence).Convergent := by sorry -/-- Proposition 6.1.15 / Exercise 6.1.6 (Formal limits are genuine limits)-/ +/-- Proposition 6.1.15 / Exercise 6.1.6 (Formal limits are genuine limits) -/ theorem Sequence.lim_eq_LIM {a:ℕ → ℚ} (h: (a:Chapter5.Sequence).IsCauchy) : ((a:Chapter5.Sequence):Sequence).TendsTo (Chapter5.Real.equivR (Chapter5.LIM a)) := by sorry diff --git a/Analysis/Section_6_3.lean b/Analysis/Section_6_3.lean index 69f9d5b51..d50dbd6e3 100644 --- a/Analysis/Section_6_3.lean +++ b/Analysis/Section_6_3.lean @@ -117,7 +117,7 @@ example : (Example_6_3_9:Sequence).Convergent := by sorry /-- Example 6.3.9 -/ example : lim (Example_6_3_9:Sequence) ≤ 4 := by sorry -/-- Proposition 6.3.1-/ +/-- Proposition 6.3.1 -/ theorem lim_of_exp {x:ℝ} (hpos: 0 < x) (hbound: x < 1) : ((fun (n:ℕ) ↦ x^n):Sequence).Convergent ∧ lim ((fun (n:ℕ) ↦ x^n):Sequence) = 0 := by -- This proof is written to follow the structure of the original text. diff --git a/Analysis/Section_8_2.lean b/Analysis/Section_8_2.lean index 3654832de..f34fc1c71 100644 --- a/Analysis/Section_8_2.lean +++ b/Analysis/Section_8_2.lean @@ -235,12 +235,12 @@ theorem AbsConvergent'.of_countable {X:Type} (hX:CountablyInfinite X) {f:X → intro n; by_cases h: n ≥ 0 <;> simp [h] intro hf; rwa [AbsConvergent.iff hX f] at hf -/-- Lemma 8.2.5 / Exercise 8.2.2-/ +/-- Lemma 8.2.5 / Exercise 8.2.2 -/ theorem AbsConvergent'.countable_supp {X:Type} {f:X → ℝ} (hf: AbsConvergent' f) : AtMostCountable { x | f x ≠ 0 } := by sorry -/-- Compare with Mathlib's {name}`Summable.subtype`-/ +/-- Compare with Mathlib's {name}`Summable.subtype` -/ theorem AbsConvergent'.subtype {X:Type} {f:X → ℝ} (hf: AbsConvergent' f) (A: Set X) : AbsConvergent' (fun x:A ↦ f x) := by apply BddAbove.mono _ hf @@ -365,7 +365,7 @@ theorem AbsConvergent'.iff_Summable {X:Type} (f:X → ℝ) : AbsConvergent' f . exact inter_subset_right apply le_of_lt (lt_of_abs_lt (hS _ disjoint_sdiff_self_left)) -/-- Maybe suitable for porting to Mathlib?-/ +/-- Maybe suitable for porting to Mathlib? -/ theorem Filter.Eventually.int_natCast_atTop (p: ℤ → Prop) : (∀ᶠ n in .atTop, p n) ↔ ∀ᶠ n:ℕ in .atTop, p ↑n := by refine ⟨ Eventually.natCast_atTop, ?_ ⟩ @@ -419,7 +419,7 @@ theorem Sum'.smul {X:Type} {f:X → ℝ} (hf: AbsConvergent' f) (c: ℝ) : AbsConvergent' (c • f) ∧ Sum' (c • f) = c * Sum' f := by sorry -/-- This law is not explicitly stated in Proposition 8.2.6, but follows easily from parts (a) and (b).-/ +/-- This law is not explicitly stated in Proposition 8.2.6, but follows easily from parts (a) and (b). -/ theorem Sum'.sub {X:Type} {f g:X → ℝ} (hf: AbsConvergent' f) (hg: AbsConvergent' g) : AbsConvergent' (f-g) ∧ Sum' (f - g) = Sum' f - Sum' g := by convert add hf (smul hg (-1)).1 using 2 diff --git a/Analysis/Section_8_5.lean b/Analysis/Section_8_5.lean index d52cfb1ff..e5981556e 100644 --- a/Analysis/Section_8_5.lean +++ b/Analysis/Section_8_5.lean @@ -172,7 +172,7 @@ example : ¬ IsStrictUpperBound (.Icc 1 2: Set ℝ) 2 := by sorry example : IsStrictUpperBound (.Icc 1 2: Set ℝ) 3 := by sorry -/-- A convenient way to simplify the notion of having {name}`x₀` as a minimal element.-/ +/-- A convenient way to simplify the notion of having {name}`x₀` as a minimal element. -/ theorem IsMin.iff_lowerbound {X:Type} [PartialOrder X] {Y: Set X} (hY: IsTotal Y) (x₀ : X) : (∃ hx₀ : x₀ ∈ Y, IsMin (⟨ x₀, hx₀ ⟩:Y)) ↔ x₀ ∈ Y ∧ ∀ x ∈ Y, x₀ ≤ x := by constructor . rintro ⟨ hx₀, hmin ⟩; simp [IsMin, hx₀] at * @@ -189,7 +189,7 @@ theorem IsMin.iff_lowerbound' {X:Type} [PartialOrder X] {Y: Set X} (hY: IsTotal /-- Exercise 8.5.11 -/ example {X:Type} [PartialOrder X] {Y Y':Set X} (hY: IsTotal Y) (hY': IsTotal Y') (hY_well: WellFoundedLT Y) (hY'_well: WellFoundedLT Y') (hYY': IsTotal (Y ∪ Y': Set X)) : WellFoundedLT (Y ∪ Y': Set X) := by sorry -/-- Lemma 8.5.14-/ +/-- Lemma 8.5.14 -/ theorem WellFoundedLT.partialOrder {X:Type} [PartialOrder X] (x₀ : X) : ∃ Y : Set X, IsTotal Y ∧ WellFoundedLT Y ∧ (∃ hx₀ : x₀ ∈ Y, IsMin (⟨ x₀, hx₀ ⟩: Y)) ∧ ¬ ∃ x, IsStrictUpperBound Y x := by -- This proof is based on the original text with some technical simplifications. diff --git a/Analysis/Section_9_1.lean b/Analysis/Section_9_1.lean index a8254638f..5d7668623 100644 --- a/Analysis/Section_9_1.lean +++ b/Analysis/Section_9_1.lean @@ -164,7 +164,7 @@ theorem closure_of_Q : closure ((fun n:ℚ ↦ (n:ℝ)) '' .univ) = .univ := by sorry -/-- Lemma 9.1.14 / Exercise 9.1.4-/ +/-- Lemma 9.1.14 / Exercise 9.1.4 -/ theorem limit_of_AdherentPt (X: Set ℝ) (x:ℝ) : AdherentPt x X ↔ ∃ a : ℕ → ℝ, (∀ n, a n ∈ X) ∧ Filter.atTop.Tendsto a (nhds x) := by sorry @@ -226,7 +226,7 @@ theorem isClosed_iff_limits_mem (X: Set ℝ) : /-- Definition 9.1.18 (Limit points) -/ abbrev LimitPt (x:ℝ) (X: Set ℝ) := AdherentPt x (X \ {x}) -/-- Identification with Mathlib's {name}`AccPt`-/ +/-- Identification with Mathlib's {name}`AccPt` -/ theorem LimitPt.iff_AccPt (x:ℝ) (X: Set ℝ) : LimitPt x X ↔ AccPt x (.principal X) := by rw [accPt_principal_iff_clusterPt,←AdherentPt_def] @@ -290,7 +290,7 @@ theorem mem_Iio_isLimit {a x:ℝ} (hx: x ∈ Set.Iio a) : LimitPt x (.Iio a) := theorem mem_R_isLimit {x:ℝ} : LimitPt x (.univ) := by sorry -/-- Definition 9.1.22. We use here Mathlib's {name}`Bornology.IsBounded`-/ +/-- Definition 9.1.22. We use here Mathlib's {name}`Bornology.IsBounded` -/ theorem isBounded_def (X: Set ℝ) : Bornology.IsBounded X ↔ ∃ M > 0, X ⊆ .Icc (-M) M := by simp [isBounded_iff_forall_norm_le]