From c87f6d9697253fac9361dd79ccefabb0042d92a5 Mon Sep 17 00:00:00 2001 From: Rado Kirov Date: Mon, 9 Feb 2026 22:28:49 -0800 Subject: [PATCH] =?UTF-8?q?Fix=20typo=20in=20Example=206.6.2:=20(1:?= =?UTF-8?q?=E2=84=9D)=20should=20be=20(10:=E2=84=9D)=20in=20odd=20branch?= MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit The parent sequence's odd terms were `(1:ℝ)^(-(n/2:ℤ)-1)` which is always 1, making the second subsequence claim (extracting 10^(-n-1)) impossible. Should be `(10:ℝ)^(-(n/2:ℤ)-1)`. Co-Authored-By: Claude Opus 4.6 --- analysis/Analysis/Section_6_6.lean | 4 ++-- 1 file changed, 2 insertions(+), 2 deletions(-) diff --git a/analysis/Analysis/Section_6_6.lean b/analysis/Analysis/Section_6_6.lean index bf37b9cf..77704c10 100644 --- a/analysis/Analysis/Section_6_6.lean +++ b/analysis/Analysis/Section_6_6.lean @@ -26,12 +26,12 @@ example (a:ℕ → ℝ) : Sequence.subseq a (fun n ↦ a (2 * n)) := by sorry example {f: ℕ → ℕ} (hf: StrictMono f) : Function.Injective f := by sorry example : - Sequence.subseq (fun n ↦ if Even n then 1 + (10:ℝ)^(-(n/2:ℤ)-1) else (1:ℝ)^(-(n/2:ℤ)-1)) + Sequence.subseq (fun n ↦ if Even n then 1 + (10:ℝ)^(-(n/2:ℤ)-1) else (10:ℝ)^(-(n/2:ℤ)-1)) (fun n ↦ 1 + (10:ℝ)^(-(n:ℤ)-1)) := by sorry example : - Sequence.subseq (fun n ↦ if Even n then 1 + (10:ℝ)^(-(n/2:ℤ)-1) else (1:ℝ)^(-(n/2:ℤ)-1)) + Sequence.subseq (fun n ↦ if Even n then 1 + (10:ℝ)^(-(n/2:ℤ)-1) else (10:ℝ)^(-(n/2:ℤ)-1)) (fun n ↦ (10:ℝ)^(-(n:ℤ)-1)) := by sorry