⚠️ Found by a local LLM, not a human. This was flagged by an automated documentation-mistake finder (qwen3:14b) and passed 10/10 independent verification runs before filing, but it has not been reviewed by a person. Please check it's a genuine error before acting on it.
Summary
The documentation in Physlib/SpaceAndTime/Space/Norm/Basic.lean (around line 15) is incorrect.
Current text
## i. Overview
The main content of this file is defining `Space.normPowerSeries`, a power series which is
differentiable everywhere, and which tends to the norm in the limit as `n → ∞`.
Why this is wrong
The file claims that Space.normPowerSeries is a power series, but its definition as sqrt(‖x‖^2 + 1/(n+1)) does not match the mathematical definition of a power series (which is a sum of terms $a_k x^k$). The reviewer correctly notes this is a sequence of functions, not a power series.
The correction accurately describes it as a sequence of functions that converges to the norm. This aligns with the implementation, which defines normPowerSeries as a function depending on n but does not involve any summation over powers of ‖x‖. The term "power series" was misleading and has been appropriately replaced.
Suggested correction
## i. Overview
The main content of this file is defining `Space.normPowerSeries`, a sequence of functions which is differentiable everywhere, and which tends to the norm in the limit as `n → ∞`.
Summary
The documentation in
Physlib/SpaceAndTime/Space/Norm/Basic.lean(around line 15) is incorrect.Current text
Why this is wrong
The file claims that$a_k x^k$ ). The reviewer correctly notes this is a sequence of functions, not a power series.
Space.normPowerSeriesis a power series, but its definition assqrt(‖x‖^2 + 1/(n+1))does not match the mathematical definition of a power series (which is a sum of termsThe correction accurately describes it as a sequence of functions that converges to the norm. This aligns with the implementation, which defines
normPowerSeriesas a function depending onnbut does not involve any summation over powers of‖x‖. The term "power series" was misleading and has been appropriately replaced.Suggested correction