Skip to content

fix: disambiguate Verso labels for 11.2.16, 11.8.8, and 7.5.3 #607

New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

Sign up for GitHub

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Open
Chessing234 wants to merge 9 commits into
base: main
Choose a base branch
from
+7 −7
Open

fix: disambiguate Verso labels for 11.2.16, 11.8.8, and 7.5.3 #607

Show file tree
Hide file tree
Changes from all commits
Commits
Show all changes
9 commits
Select commit Hold shift + click to select a range
531023f
Disambiguate Theorem 11.2.16(f') label for integ_const'.
Chessing234 Jul 23, 2026
fc93b86
Disambiguate Theorem 11.2.16(g') label for integ_of_extend.
Chessing234 Jul 23, 2026
c512092
Disambiguate Theorem 11.2.16(h') label for integ_of_join.
Chessing234 Jul 23, 2026
fbe2bef
Disambiguate Theorem 11.8.8(f') label for RS_integ_const'.
Chessing234 Jul 23, 2026
e084232
Disambiguate Theorem 11.8.8(g') label for RS_integ_of_extend.
Chessing234 Jul 23, 2026
ae926ea
Split Corollary 7.5.3 into (i)/(ii) for diverge vs absConverge cases.
Chessing234 Jul 23, 2026
d13e6a7
Merge Theorem 11.2.16(f)/(g)/(h) label fixes.
Chessing234 Jul 23, 2026
09f542b
Merge Theorem 11.8.8(f)/(g) label fixes.
Chessing234 Jul 23, 2026
68e7cdc
Merge Corollary 7.5.3(i)/(ii) label split.
Chessing234 Jul 23, 2026
File filter

Filter by extension

Filter by extension
Conversations
Failed to load comments.
Loading
Jump to
Jump to file
Failed to load files.
Loading
Diff view
Diff view
6 changes: 3 additions & 3 deletions Analysis/Section_11_2.lean
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -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
Expand All @@ -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
Expand All @@ -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
Expand Down
4 changes: 2 additions & 2 deletions Analysis/Section_11_8.lean
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -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
Expand All @@ -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
Expand Down
4 changes: 2 additions & 2 deletions Analysis/Section_7_5.lean
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -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
Expand Down
Loading