From 531023f9ebd7ccdef3fd0599eed7040d87127467 Mon Sep 17 00:00:00 2001 From: Taksh Date: Thu, 23 Jul 2026 16:04:12 +0300 Subject: [PATCH 1/6] Disambiguate Theorem 11.2.16(f') label for integ_const'. --- Analysis/Section_11_2.lean | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/Analysis/Section_11_2.lean b/Analysis/Section_11_2.lean index 8eeb5550..9986801b 100644 --- a/Analysis/Section_11_2.lean +++ b/Analysis/Section_11_2.lean @@ -266,7 +266,7 @@ theorem PiecewiseConstantOn.integ_const (c: ℝ) (I: BoundedInterval) : integ (fun _ ↦ c) I = c * |I|ₗ := by sorry -/-- Theorem 11.2.16 (f) (Laws of integration) / Exercise 11.2.4 -/ +/-- Theorem 11.2.16 (f') (Laws of integration) / Exercise 11.2.4 -/ theorem PiecewiseConstantOn.integ_const' {f:ℝ → ℝ} {I: BoundedInterval} (h: ConstantOn f I) : integ f I = (constant_value_on f I) * |I|ₗ := by sorry From fc93b86f8c42d7e935bb65d63b7b509ea9777ca2 Mon Sep 17 00:00:00 2001 From: Taksh Date: Thu, 23 Jul 2026 16:04:12 +0300 Subject: [PATCH 2/6] Disambiguate Theorem 11.2.16(g') label for integ_of_extend. --- Analysis/Section_11_2.lean | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/Analysis/Section_11_2.lean b/Analysis/Section_11_2.lean index 9986801b..239a3689 100644 --- a/Analysis/Section_11_2.lean +++ b/Analysis/Section_11_2.lean @@ -279,7 +279,7 @@ theorem PiecewiseConstantOn.of_extend {I J: BoundedInterval} (hIJ: I ⊆ J) sorry open Classical in -/-- Theorem 11.2.16 (g) (Laws of integration) / Exercise 11.2.4 -/ +/-- Theorem 11.2.16 (g') (Laws of integration) / Exercise 11.2.4 -/ theorem PiecewiseConstantOn.integ_of_extend {I J: BoundedInterval} (hIJ: I ⊆ J) {f: ℝ → ℝ} (h: PiecewiseConstantOn f I) : integ (fun x ↦ if x ∈ I then f x else 0) J = integ f I := by From c5120926e59adc19041535300bfe838ade7ac799 Mon Sep 17 00:00:00 2001 From: Taksh Date: Thu, 23 Jul 2026 16:04:12 +0300 Subject: [PATCH 3/6] Disambiguate Theorem 11.2.16(h') label for integ_of_join. --- Analysis/Section_11_2.lean | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/Analysis/Section_11_2.lean b/Analysis/Section_11_2.lean index 239a3689..5b9aebb6 100644 --- a/Analysis/Section_11_2.lean +++ b/Analysis/Section_11_2.lean @@ -290,7 +290,7 @@ theorem PiecewiseConstantOn.of_join {I J K: BoundedInterval} (hIJK: K.joins I J) (f: ℝ → ℝ) : PiecewiseConstantOn f K ↔ PiecewiseConstantOn f I ∧ PiecewiseConstantOn f J := by sorry -/-- Theorem 11.2.16 (h) (Laws of integration) / Exercise 11.2.4 -/ +/-- Theorem 11.2.16 (h') (Laws of integration) / Exercise 11.2.4 -/ theorem PiecewiseConstantOn.integ_of_join {I J K: BoundedInterval} (hIJK: K.joins I J) {f: ℝ → ℝ} (h: PiecewiseConstantOn f K) : integ f K = integ f I + integ f J := by From fbe2bef4144f18d04228dea8dea544315da4074c Mon Sep 17 00:00:00 2001 From: Taksh Date: Thu, 23 Jul 2026 16:04:32 +0300 Subject: [PATCH 4/6] Disambiguate Theorem 11.8.8(f') label for RS_integ_const'. --- Analysis/Section_11_8.lean | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/Analysis/Section_11_8.lean b/Analysis/Section_11_8.lean index 3a62bffa..47c31248 100644 --- a/Analysis/Section_11_8.lean +++ b/Analysis/Section_11_8.lean @@ -315,7 +315,7 @@ theorem PiecewiseConstantOn.RS_integ_const (c: ℝ) (I: BoundedInterval) {α:ℝ RS_integ (fun _ ↦ c) I α = c * α[I]ₗ := by sorry -/-- Theorem 11.8.8 (f) (Laws of RS integration) / Exercise 11.8.3 -/ +/-- Theorem 11.8.8 (f') (Laws of RS integration) / Exercise 11.8.3 -/ theorem PiecewiseConstantOn.RS_integ_const' {f:ℝ → ℝ} {I: BoundedInterval} {α:ℝ → ℝ} (hα: Monotone α) (h: ConstantOn f I) : RS_integ f I α = (constant_value_on f I) * α[I]ₗ := by From e084232b3ba3e61ead64dd0aeae529d8fdf30c9d Mon Sep 17 00:00:00 2001 From: Taksh Date: Thu, 23 Jul 2026 16:04:33 +0300 Subject: [PATCH 5/6] Disambiguate Theorem 11.8.8(g') label for RS_integ_of_extend. --- Analysis/Section_11_8.lean | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/Analysis/Section_11_8.lean b/Analysis/Section_11_8.lean index 47c31248..d4b7cd60 100644 --- a/Analysis/Section_11_8.lean +++ b/Analysis/Section_11_8.lean @@ -329,7 +329,7 @@ theorem PiecewiseConstantOn.RS_of_extend {I J: BoundedInterval} (hIJ: I ⊆ J) sorry open Classical in -/-- Theorem 11.8.8 (g) (Laws of RS integration) / Exercise 11.8.3 -/ +/-- Theorem 11.8.8 (g') (Laws of RS integration) / Exercise 11.8.3 -/ theorem PiecewiseConstantOn.RS_integ_of_extend {I J: BoundedInterval} (hIJ: I ⊆ J) {f: ℝ → ℝ} (h: PiecewiseConstantOn f I) {α:ℝ → ℝ} (hα: Monotone α): RS_integ (fun x ↦ if x ∈ I then f x else 0) J α = RS_integ f I α := by From ae926ea9f40f567d683483b46683630c8cd7a361 Mon Sep 17 00:00:00 2001 From: Taksh Date: Thu, 23 Jul 2026 16:04:33 +0300 Subject: [PATCH 6/6] Split Corollary 7.5.3 into (i)/(ii) for diverge vs absConverge cases. --- Analysis/Section_7_5.lean | 4 ++-- 1 file changed, 2 insertions(+), 2 deletions(-) diff --git a/Analysis/Section_7_5.lean b/Analysis/Section_7_5.lean index a677b7ea..1336e151 100644 --- a/Analysis/Section_7_5.lean +++ b/Analysis/Section_7_5.lean @@ -190,12 +190,12 @@ theorem Series.ratio_test_neg {s : Series} (hnon: ∀ n ≥ s.m, s.seq n ≠ 0) convert (ratio_ineq s.m _).1.trans (ratio_ineq s.m _).2.1 with n; rfl all_goals convert hnon using 1 with n; simp -/-- Corollary 7.5.3 (Ratio test) / Exercise 7.5.3 -/ +/-- Corollary 7.5.3(i) (Ratio test inconclusive, diverges) / Exercise 7.5.3 -/ theorem Series.ratio_test_inconclusive: ∃ s:Series, (∀ n ≥ s.m, s.seq n ≠ 0) ∧ atTop.Tendsto (fun n ↦ |s.seq (n+1)| / |s.seq n|) (nhds 1) ∧ s.diverges := by sorry -/-- Corollary 7.5.3 (Ratio test) / Exercise 7.5.3 -/ +/-- Corollary 7.5.3(ii) (Ratio test inconclusive, absConverges) / Exercise 7.5.3 -/ theorem Series.ratio_test_inconclusive' : ∃ s:Series, (∀ n ≥ s.m, s.seq n ≠ 0) ∧ atTop.Tendsto (fun n ↦ |s.seq (n+1)| / |s.seq n|) (nhds 1) ∧ s.absConverges := by sorry