From ec4fd5e2219aa6e963325f9e1cb28eb0902a2ee9 Mon Sep 17 00:00:00 2001 From: Rado Kirov Date: Tue, 10 Feb 2026 22:17:09 -0800 Subject: [PATCH] Add missing (hx : x > 0) hypothesis to rpow_eq_rpow MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit The theorem `rpow x α = x ^ α` is false at (x, α) = (0, 0): Mathlib gives 0^0 = 1 (by rpow_zero), but the custom rpow 0 0 computes lim(0^q_n) where q_n → 0 with q_n ≠ 0, giving 0^q_n = 0 for all n, so the limit is 0. Co-Authored-By: Claude Opus 4.6 --- analysis/Analysis/Section_6_epilogue.lean | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/analysis/Analysis/Section_6_epilogue.lean b/analysis/Analysis/Section_6_epilogue.lean index 94f238a0..6e33b198 100644 --- a/analysis/Analysis/Section_6_epilogue.lean +++ b/analysis/Analysis/Section_6_epilogue.lean @@ -137,5 +137,5 @@ theorem Chapter6.Sequence.liminf_eq (a:ℕ → ℝ) : sorry /-- Identification of `rpow` and Mathlib exponentiation -/ -theorem Chapter6.Real.rpow_eq_rpow (x:ℝ) (α:ℝ) : rpow x α = x^α := by +theorem Chapter6.Real.rpow_eq_rpow {x:ℝ} (hx: x > 0) (α:ℝ) : rpow x α = x^α := by sorry