teorth · teorth · Aug 2, 2026 · Jul 31, 2026
diff --git a/Analysis/MeasureTheory/Section_1_1_1.lean b/Analysis/MeasureTheory/Section_1_1_1.lean
@@ -289,12 +289,12 @@ def witness_upperBound_lowerBounds {X : Set ℝ} (y : ℝ) (hy : y ∈ X)
 
 /- If x < sSup X and X is not empty, then there exists z ∈ X with x < z -/
 /- We don't need to assume that X is BddAbove
--(if X is not Bddabove, we get that sSup X = 0 (the junk value) and the result still follows -/
+-(if X is not BddAbove, we get that sSup X = 0 (the junk value) and the result still follows -/
 #check exists_lt_of_lt_csSup
 
 /- If sInf X < x and X is not empty, then there exists w ∈ X with w ≤ x -/
 /- We don't need to assume that X is BddBelow.
--(if X if not BddBelow, we get that sInf X = 0 (the junk value) and the result still follows-/
+-(if X is not BddBelow, we get that sInf X = 0 (the junk value) and the result still follows -/
 #check exists_lt_of_csInf_lt
 
 /-- Show x < b when b = sSup X and b ∉ X -/

diff --git a/Analysis/Section_11_3.lean b/Analysis/Section_11_3.lean
@@ -120,7 +120,7 @@ lemma gt_of_lt_lower_integral {f:ℝ → ℝ} {I: BoundedInterval} (hf: BddOn f
   simp at hY; peel hY; simp_all; tauto
 
 /-- Definition 11.3.4 (Riemann integral)
-As we permit junk values, the simplest definition for the Riemann integral is the upper integral.-/
+As we permit junk values, the simplest definition for the Riemann integral is the upper integral. -/
 noncomputable abbrev integ (f:ℝ → ℝ) (I: BoundedInterval) : ℝ := upper_integral f I
 
 theorem integ_congr {f g:ℝ → ℝ} {I: BoundedInterval} (h: Set.EqOn f g I) :

diff --git a/Analysis/Section_11_4.lean b/Analysis/Section_11_4.lean
@@ -157,7 +157,7 @@ theorem IntegrableOn.abs {I: BoundedInterval} {f:ℝ → ℝ} (hf: IntegrableOn
   ext x; obtain h | h := (show f x ≤ 0 ∨ f x ≥ 0 by grind) <;> simp [h]
 
 /-- Theorem 11.4.5 (Products preserve Riemann integrability).
-It is convenient to first establish the non-negative case.-/
+It is convenient to first establish the non-negative case. -/
 theorem integ_of_mul_nonneg {I: BoundedInterval} {f g:ℝ → ℝ} (hf: IntegrableOn f I) (hg: IntegrableOn g I)
   (hf_nonneg: MajorizesOn f 0 I) (hg_nonneg: MajorizesOn g 0 I) :
   IntegrableOn (f * g) I := by

diff --git a/Analysis/Section_2_2.lean b/Analysis/Section_2_2.lean
@@ -38,7 +38,7 @@ namespace Chapter2
 abbrev Nat.add (n m : Nat) : Nat := Nat.recurse (fun _ sum ↦ sum++) m n
 
 /-- This instance allows for the {kw (of := «term_+_»)}`+` notation to be used for natural number
-    addition.-/
+    addition. -/
 instance Nat.instAdd : Add Nat where add := add
 
 /-- Compare with Mathlib's {name}`Nat.zero_add`. -/
@@ -225,7 +225,7 @@ theorem Nat.succ_gt_self (n:Nat) : n++ > n := by
 
 /-- Proposition 2.2.12 (Basic properties of order for natural numbers) / Exercise 2.2.3
 
-(a) (Order is reflexive). Compare with Mathlib's {name}`Nat.le_refl`.-/
+(a) (Order is reflexive). Compare with Mathlib's {name}`Nat.le_refl`. -/
 theorem Nat.ge_refl (a:Nat) : a ≥ a := by
   sorry
 

diff --git a/Analysis/Section_3_4.lean b/Analysis/Section_3_4.lean
@@ -276,7 +276,7 @@ Interestingly, it is not needed for U to be a subset of Y. -/
 -- theorem SetTheory.Set.image_of_preimage {X Y:Set} (f:X → Y) (U: Set) : sorry := by sorry
 
 /- Exercise 3.4.2.  State and prove an assertion connecting `preimage f (image f (preimage f U))` and `preimage f U`.
-Interestingly, it is not needed for U to be a subset of Y.-/
+Interestingly, it is not needed for U to be a subset of Y. -/
 -- theorem SetTheory.Set.preimage_of_image_of_preimage {X Y:Set} (f:X → Y) (U: Set) : sorry := by sorry
 
 /--

diff --git a/Analysis/Section_8_2.lean b/Analysis/Section_8_2.lean
@@ -31,7 +31,7 @@ open Chapter7 Chapter7.Series Finset Function Filter
 
 /-- 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 {lit}`AbsConvergent'` instead for such
-cases.-/
+cases. -/
 abbrev AbsConvergent {X:Type} (f: X → ℝ) : Prop := ∃ g: ℕ → X, Bijective g ∧ (f ∘ g: Series).absConverges
 
 theorem AbsConvergent.mk {X: Type} {f:X → ℝ} {g:ℕ → X} (h: Bijective g) (hfg: (f ∘ g:Series).absConverges) : AbsConvergent f := by use g
@@ -434,7 +434,7 @@ theorem Sum'.of_disjoint_union {X:Type} {f:X → ℝ} (hf: AbsConvergent' f) {X
   sorry
 
 /-- This technical claim, the analogue of {name}`tsum_univ`, is required due to the way Mathlib handles
-    sets.-/
+    sets. -/
 theorem Sum'.of_univ {X:Type} {f:X → ℝ} (hf: AbsConvergent' f) :
   Sum' (fun x: (.univ : Set X) ↦ f x) = Sum' f := by
   sorry