Structured Preparation
Exercise SP-112
local source supported. Current content-bound mathematical second pass accepted. No new Lean verification is claimed for this NL view.
Assumptions and conventions
- samples use the exact grid x_j = start + step*j; the right tail reuses the same formula with negated start and step
Question
On the exponential tail of the target, the sampled amplitude at x_j = start + step*j is exp(x_j), and the discrete squared mass over count samples is E = sum_{j=0}^{count-1} exp(x_j)^2. Give the exact closed form for E, and treat the boundary case step = 0 explicitly. Explain precisely why the generic geometric-series formula exp(2 start) * ((exp(2 step))^count - 1) / (exp(2 step) - 1) is well defined exactly when step is nonzero, what it degenerates to as the ratio approaches 1, and what the correct value is when step = 0.
Hint: mathematical route
The exponential-tail discrete squared mass is a geometric sum whose closed form requires an explicit step=0 branch where the common ratio is one, with both branches agreeing in the limit.
- Each squared exponential sample factors as exp(2 start) times (exp(2 step))^j, a geometric term.
- For step != 0 the ratio exp(2 step) != 1 by injectivity of exp, so the geometric-sum formula applies with nonzero denominator.
- For step = 0 the ratio is 1 and the sum is count*exp(2 start); the branches agree in the limit, giving a total continuous definition.
Reference solution
Rewrite each squared term: exp(x_j)^2 = exp(2 x_j) = exp(2 start + 2 step j) = exp(2 start) * (exp(2 step))^j. So E = exp(2 start) * sum_{j=0}^{count-1} q^j with common ratio q = exp(2 step). Generic case (step != 0): since exp is injective and 2 step != 0, we have exp(2 step) != 1, so the ratio q != 1 and the finite geometric sum has the closed form sum_{j=0}^{count-1} q^j = (q^count - 1)/(q - 1). Hence E = exp(2 start) * ((exp(2 step))^count - 1)/(exp(2 step) - 1). The denominator exp(2 step) - 1 is nonzero exactly because step != 0, which is what makes the division well defined. Boundary case (step = 0): then q = exp(0) = 1 and every term equals exp(2 start), so the sum is count copies: E = count * exp(2 start). The generic formula is undefined here (its denominator is 0), so a separate branch is mandatory; this is not a removable notational nuisance but a genuine 0/0 at step = 0. The two branches agree in the limit: as step -> 0 the generic expression tends to exp(2 start) * count by L'Hopital/the limit of (q^count-1)/(q-1) at q=1, matching the step=0 value, so the piecewise definition is continuous across the boundary. A single formula without the case split would either divide by zero at step = 0 or silently return a wrong value, so the explicit boundary branch is required for a total, correct definition.
Assessment rubric
- Rewrites exp(x_j)^2 = exp(2 start)*(exp(2 step))^j, exhibiting a geometric series with ratio exp(2 step). (1 weight)
- Gives the generic closed form and argues the ratio exp(2 step) != 1 (hence denominator nonzero) exactly when step != 0, by injectivity of exp. (1 weight)
- Handles step=0 as a separate branch E = count*exp(2 start), noting the generic formula is a genuine 0/0 there. (1 weight)
- Explains the two branches agree in the step->0 limit, so the piecewise definition is continuous and total. (1 weight)
Graph-grounded prerequisites
These are support/source anchors, not an automatically extracted theorem-dependency proof.
Lean view and evidence boundary
No aligned Lean view has been admitted for this native core in this textbook checkpoint. This is not a claim that the underlying mathematics lacks a formal proof. Contributions must preserve this exact target contract and split.
Sources and provenance
- QuantumBlockEncoding/HermiteIntervalMass.lean
lines 89-116: exponentialMassClosed start step count = if step = 0 then count * exp(2*start) else exp(2*start) * ((exp(2*step))^count - 1)/(exp(2*step)-1); exponentialMassClosed_eq : = sum_{j in range count} (exp(start+step*j))^2; proof needs exp(2*step) != 1 derived from step != 0 via exp_injective, then geom_sum_eq
Source SHA-256:ff87cc69d0527cb1a7001a7bae4b916cf0a2c2b8bd1e6ba017511c3be27bc69f· MIT (repository LICENSE)
Contract: 7cd9b2ef7659382e6980272b94b9108f3a13582583829cb18dcd449b35343b95
Item digest: f461f617f938693f5dd6590f3941706aa04c057bf24d4f52eda14c0641aecfab
Graph snapshot: qcb-snapshot-ffa644f0da3031a1ce754b9a
Authored support steps: 3. This is not measured graph distance or model difficulty.