This definition gives the library's named construction or computation for “power sum closed”. A power sum with iteration bound depending on the degree, not sample count.
def powerSumClosed (count degree : ℕ) : ℚ :=
∑ i ∈ Finset.range (degree + 1),
_root_.bernoulli i * ((degree + 1).choose i) *
(count : ℚ) ^ (degree + 1 - i) / (degree + 1)
/-- Mathlib's exact Faulhaber theorem, exposed over the real target field. -/
commit-pinned source · Verso Blueprint panel
Lean checks the proposition indexed as “power sum closed eq”; the hypotheses and conclusion in the code panel fix its exact scope. Mathlib's exact Faulhaber theorem, exposed over the real target field.
theorem powerSumClosed_eq (count degree : ℕ) :
(powerSumClosed count degree : ℝ) =
∑ j ∈ Finset.range count, (j : ℝ) ^ degree := by
commit-pinned source · Verso Blueprint panel
This definition gives the library's named construction or computation for “affine squared”. Square the actual polynomial amplitude after an affine index substitution.
def affineSquared (p : ℝ[X]) (start step : ℝ) : ℝ[X] :=
(p.comp (C start + C step * X)) ^ 2
commit-pinned source · Verso Blueprint panel
Lean checks the proposition indexed as “affine squared eval”; the hypotheses and conclusion in the code panel fix its exact scope.
@[simp] theorem affineSquared_eval (p : ℝ[X]) (start step x : ℝ) :
(affineSquared p start step).eval x = (p.eval (start + step * x)) ^ 2 := by
commit-pinned source · Verso Blueprint panel
This definition gives the library's named construction or computation for “polynomial mass closed”. A supplied degree bound gives a fixed-size expression for discrete mass.
def polynomialMassClosed (p : ℝ[X]) (start step : ℝ) (count bound : ℕ) : ℝ :=
∑ r ∈ Finset.range (bound + 1),
(affineSquared p start step).coeff r * (powerSumClosed count r : ℝ)
/-- Exact arbitrary-count identity; no quadrature or continuum substitution. -/
commit-pinned source · Verso Blueprint panel
Lean checks the proposition indexed as “polynomial mass closed eq”; the hypotheses and conclusion in the code panel fix its exact scope. Exact arbitrary-count identity; no quadrature or continuum substitution.
theorem polynomialMassClosed_eq (p : ℝ[X]) (start step : ℝ) (count bound : ℕ)
(h : (affineSquared p start step).natDegree ≤ bound) :
polynomialMassClosed p start step count bound =
∑ j ∈ Finset.range count, (p.eval (start + step * j)) ^ 2 := by
commit-pinned source · Verso Blueprint panel
Lean checks the proposition indexed as “affine squared degree”; the hypotheses and conclusion in the code panel fix its exact scope.
theorem affineSquared_degree (p : ℝ[X]) (start step : ℝ) :
(affineSquared p start step).natDegree ≤ 2 * p.natDegree := by
commit-pinned source · Verso Blueprint panel
Lean checks the proposition indexed as “hermite affine squared degree”; the hypotheses and conclusion in the code panel fix its exact scope. At most '4*k+3' coefficient terms suffice for every affine progression.
theorem hermite_affineSquared_degree (k : ℕ) (start step : ℝ) :
(affineSquared (HermitePolynomial.sourceInterpolant k) start step).natDegree ≤
4 * k + 2 := by
commit-pinned source · Verso Blueprint panel
Lean checks the proposition indexed as “hermite polynomial mass”; the hypotheses and conclusion in the code panel fix its exact scope. The exact discrete squared mass of the polynomial branch, at arbitrary width.
theorem hermite_polynomial_mass (k count : ℕ) (start step : ℝ) :
polynomialMassClosed (HermitePolynomial.sourceInterpolant k) start step count
(4 * k + 2) =
∑ j ∈ Finset.range count,
((HermitePolynomial.sourceInterpolant k).eval (start + step * j)) ^ 2 :=
polynomialMassClosed_eq _ _ _ _ _ (hermite_affineSquared_degree k start step)
/-- Explicit finite exponential mass, including the zero-step corner case. -/
commit-pinned source · Verso Blueprint panel
This definition gives the library's named construction or computation for “exponential mass closed”. Explicit finite exponential mass, including the zero-step corner case.
def exponentialMassClosed (start step : ℝ) (count : ℕ) : ℝ :=
if step = 0 then (count : ℝ) * Real.exp (2 * start)
else Real.exp (2 * start) *
((Real.exp (2 * step)) ^ count - 1) / (Real.exp (2 * step) - 1)
/-- Exact geometric mass of squared exponential amplitudes. -/
commit-pinned source · Verso Blueprint panel
Lean checks the proposition indexed as “exponential mass closed eq”; the hypotheses and conclusion in the code panel fix its exact scope. Exact geometric mass of squared exponential amplitudes.
theorem exponentialMassClosed_eq (start step : ℝ) (count : ℕ) :
exponentialMassClosed start step count =
∑ j ∈ Finset.range count, (Real.exp (start + step * j)) ^ 2 := by
commit-pinned source · Verso Blueprint panel
Lean checks the proposition indexed as “right exponential mass”; the hypotheses and conclusion in the code panel fix its exact scope. The positive exponential branch uses the same formula with negated grid.
theorem right_exponential_mass (start step : ℝ) (count : ℕ) :
exponentialMassClosed (-start) (-step) count =
∑ j ∈ Finset.range count, (Real.exp (-(start + step * j))) ^ 2 := by
commit-pinned source · Verso Blueprint panel
Lean checks the proposition indexed as “smooth initial middle mass”; the hypotheses and conclusion in the code panel fix its exact scope. On the middle branch the formula is the frozen 'smoothInitial' mass.
theorem smoothInitial_middle_mass (k count : ℕ) (start step : ℝ)
(h : ∀ j ∈ Finset.range count, start + step * j ∈ Set.Icc (-1) 0) :
polynomialMassClosed (HermitePolynomial.sourceInterpolant k) start step count
(4 * k + 2) =
∑ j ∈ Finset.range count,
(HermitePolynomial.smoothInitial k (start + step * j)) ^ 2 := by
commit-pinned source · Verso Blueprint panel
Lean checks the proposition indexed as “smooth initial left mass”; the hypotheses and conclusion in the code panel fix its exact scope. The left-tail formula concerns the function amplitude, not its square root.
theorem smoothInitial_left_mass (k count : ℕ) (start step : ℝ)
(h : ∀ j ∈ Finset.range count, start + step * j < -1) :
exponentialMassClosed start step count =
∑ j ∈ Finset.range count,
(HermitePolynomial.smoothInitial k (start + step * j)) ^ 2 := by
commit-pinned source · Verso Blueprint panel
Lean checks the proposition indexed as “smooth initial right mass”; the hypotheses and conclusion in the code panel fix its exact scope. The right-tail formula is equally a statement about the exact frozen target.
theorem smoothInitial_right_mass (k count : ℕ) (start step : ℝ)
(h : ∀ j ∈ Finset.range count, 0 < start + step * j) :
exponentialMassClosed (-start) (-step) count =
∑ j ∈ Finset.range count,
(HermitePolynomial.smoothInitial k (start + step * j)) ^ 2 := by
commit-pinned source · Verso Blueprint panel
Lean checks the proposition indexed as “smooth initial zero”; the hypotheses and conclusion in the code panel fix its exact scope. The splice passes through amplitude one, independently of smoothing order.
theorem smoothInitial_zero (k : ℕ) : HermitePolynomial.smoothInitial k 0 = 1 := by
commit-pinned source · Verso Blueprint panel
This definition gives the library's named construction or computation for “central index”. The central sample in a nonempty qubit register, in the frozen LE indexing.
def centralIndex (n : ℕ) : Fin (gridSize (n + 1)) :=
⟨2 ^ n, by
change 2 ^ n < 2 ^ (n + 1)
rw [pow_succ]
have h : 0 < 2 ^ n := pow_pos (by decide) n
omega⟩
commit-pinned source · Verso Blueprint panel
Lean checks the proposition indexed as “grid point central”; the hypotheses and conclusion in the code panel fix its exact scope.
theorem gridPoint_central (n : ℕ) (L : ℝ) :
HermiteStatePreparation.gridPoint (n + 1) L (centralIndex n) = 0 := by
commit-pinned source · Verso Blueprint panel
Lean checks the proposition indexed as “sampled mass ge one”; the hypotheses and conclusion in the code panel fix its exact scope. A width-uniform conditioning anchor: the unnormalized squared norm is at least one.
theorem sampled_mass_ge_one (k n : ℕ) (L : ℝ) :
1 ≤ ∑ j : Fin (gridSize (n + 1)),
(HermiteStatePreparation.sampledAmplitude k (n + 1) L j) ^ 2 := by
commit-pinned source · Verso Blueprint panel