From bfe082716591cff38ebc3946fcf69191b5eb4288 Mon Sep 17 00:00:00 2001 From: Rado Kirov Date: Sun, 8 Mar 2026 20:19:18 -0700 Subject: [PATCH] Fix Riemann rearrangement scaffold (Theorem 8.2.8) MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit Switch greedy construction to pick from A_plus when partial sum < L (nonneg terms to increase), A_minus when ≥ L (neg terms to decrease). Replace filled proofs with sorry scaffolds for incremental development. Co-Authored-By: Claude Opus 4.6 --- analysis/Analysis/Section_8_2.lean | 8 ++++---- 1 file changed, 4 insertions(+), 4 deletions(-) diff --git a/analysis/Analysis/Section_8_2.lean b/analysis/Analysis/Section_8_2.lean index f166071d..1921a98a 100644 --- a/analysis/Analysis/Section_8_2.lean +++ b/analysis/Analysis/Section_8_2.lean @@ -471,12 +471,12 @@ theorem permute_convergesTo_of_divergent {a: ℕ → ℝ} (ha: (a:Series).conver obtain ⟨ a_plus, ha_plus_bij, ha_plus_mono ⟩ := (Nat.monotone_enum_of_infinite A_plus).exists obtain ⟨ a_minus, ha_minus_bij, ha_minus_mono ⟩ := (Nat.monotone_enum_of_infinite A_minus).exists let F : (n : ℕ) → ((m : ℕ) → m < n → ℕ) → ℕ := - fun j n' ↦ if ∑ i:Fin j, n' i (by simp) > L then + fun j n' ↦ if ∑ i:Fin j, a (n' i (by simp)) < L then Nat.min { n ∈ A_plus | ∀ i:Fin j, n ≠ n' i (by simp) } else Nat.min { n ∈ A_minus | ∀ i:Fin j, n ≠ n' i (by simp) } let n' : ℕ → ℕ := Nat.strongRec F - have hn' (j:ℕ) : n' j = if ∑ i:Fin j, n' i > L then + have hn' (j:ℕ) : n' j = if ∑ i:Fin j, a (n' i) < L then Nat.min { n ∈ A_plus | ∀ i:Fin j, n ≠ n' i } else Nat.min { n ∈ A_minus | ∀ i:Fin j, n ≠ n' i } @@ -484,8 +484,8 @@ theorem permute_convergesTo_of_divergent {a: ℕ → ℝ} (ha: (a:Series).conver have hn'_plus_inf (j:ℕ) : Infinite { n ∈ A_plus | ∀ i:Fin j, n ≠ n' i } := by sorry have hn'_minus_inf (j:ℕ) : Infinite { n ∈ A_minus | ∀ i:Fin j, n ≠ n' i } := by sorry have hn'_inj : Injective n' := by sorry - have h_case_I : Infinite { j | ∑ i:Fin j, n' i > L } := by sorry - have h_case_II : Infinite { j | ∑ i:Fin j, n' i ≤ L } := by sorry + have h_case_I : Infinite { j | ∑ i:Fin j, a (n' i) < L } := by sorry + have h_case_II : Infinite { j | ∑ i:Fin j, a (n' i) ≥ L } := by sorry have hn'_surj : Surjective n' := by sorry have hconv : atTop.Tendsto (a ∘ n') (nhds 0) := by sorry have hsum : (a ∘ n':Series).convergesTo L := by sorry