QuantumBlockEncoding/HermiteBernstein.lean

This definition gives the library's named construction or computation for “basis”. Evaluation of the exact degree-'d' Bernstein basis polynomial.

def basis (d r : ℕ) (t : ℝ) : ℝ := (bernsteinPolynomial ℝ d r).eval t

commit-pinned source · Verso Blueprint panel

Lean checks the proposition indexed as “basis eq”; the hypotheses and conclusion in the code panel fix its exact scope.

theorem basis_eq (d r : ℕ) (t : ℝ) :
    basis d r t = (d.choose r : ℝ) * t ^ r * (1 - t) ^ (d - r) := by

commit-pinned source · Verso Blueprint panel

Lean checks the proposition indexed as “basis nonneg”; the hypotheses and conclusion in the code panel fix its exact scope.

theorem basis_nonneg (d r : ℕ) (t : ℝ) (ht : t ∈ Set.Icc 0 1) :
    0 ≤ basis d r t := by

commit-pinned source · Verso Blueprint panel

Lean checks the proposition indexed as “basis flip”; the hypotheses and conclusion in the code panel fix its exact scope.

theorem basis_flip (d r : ℕ) (hr : r ≤ d) (t : ℝ) :
    basis d r (1 - t) = basis d (d - r) t := by

commit-pinned source · Verso Blueprint panel

This definition gives the library's named construction or computation for “source coefficient”. The coefficient of 't^i' in the source's positive truncated series.

def sourceCoefficient (k i : ℕ) : ℝ := PowerSeries.coeff i (coefficientSeries k)

commit-pinned source · Verso Blueprint panel

Lean checks the proposition indexed as “source coefficient eq”; the hypotheses and conclusion in the code panel fix its exact scope.

theorem sourceCoefficient_eq (k i : ℕ) :
    sourceCoefficient k i = ∑ m ∈ Finset.range (i + 1),
      (Nat.choose (k + i - m) k : ℝ) / (m.factorial : ℝ) :=
  coefficientSeries_coeff k i

commit-pinned source · Verso Blueprint panel

Lean checks the proposition indexed as “source coefficient nonneg”; the hypotheses and conclusion in the code panel fix its exact scope.

theorem sourceCoefficient_nonneg (k i : ℕ) : 0 ≤ sourceCoefficient k i :=
  coefficientSeries_coeff_nonneg k i

/-- Degree-elevation weight from source monomial `i` to basis index `i+j`. -/

commit-pinned source · Verso Blueprint panel

This definition gives the library's named construction or computation for “elevation weight”. Degree-elevation weight from source monomial 'i' to basis index 'i+j'.

def elevationWeight (k i j : ℕ) : ℝ :=
  ((k - i).choose j : ℝ) / ((2 * k + 1).choose (i + j) : ℝ)

commit-pinned source · Verso Blueprint panel

Lean checks the proposition indexed as “elevation weight nonneg”; the hypotheses and conclusion in the code panel fix its exact scope.

theorem elevationWeight_nonneg (k i j : ℕ) : 0 ≤ elevationWeight k i j :=
  div_nonneg (Nat.cast_nonneg _) (Nat.cast_nonneg _)

commit-pinned source · Verso Blueprint panel

Lean checks the proposition indexed as “elevation term”; the hypotheses and conclusion in the code panel fix its exact scope.

theorem elevation_term (k i j : ℕ) (hi : i ≤ k) (hj : j ≤ k - i) (t : ℝ) :
    elevationWeight k i j * basis (2 * k + 1) (i + j) t =
      t ^ i * (1 - t) ^ (k + 1) *
        ((k - i).choose j : ℝ) * t ^ j * (1 - t) ^ (k - i - j) := by

commit-pinned source · Verso Blueprint panel

Lean checks the proposition indexed as “elevation sum”; the hypotheses and conclusion in the code panel fix its exact scope. Exact degree elevation of one endpoint-factor monomial.

theorem elevation_sum (k i : ℕ) (hi : i ≤ k) (t : ℝ) :
    (∑ j ∈ Finset.range (k - i + 1),
      elevationWeight k i j * basis (2 * k + 1) (i + j) t) =
      t ^ i * (1 - t) ^ (k + 1) := by

commit-pinned source · Verso Blueprint panel

This definition gives the library's named construction or computation for “left coefficient”. Collected Bernstein coefficients for the source's left endpoint factor.

def leftCoefficient (k r : ℕ) : ℝ :=
  ∑ i ∈ Finset.range (k + 1), ∑ j ∈ Finset.range (k - i + 1),
    if r = i + j then sourceCoefficient k i * elevationWeight k i j else 0

commit-pinned source · Verso Blueprint panel

Lean checks the proposition indexed as “left coefficient eq”; the hypotheses and conclusion in the code panel fix its exact scope.

theorem leftCoefficient_eq (k r : ℕ) :
    leftCoefficient k r = ∑ i ∈ Finset.range (k + 1),
      if i ≤ r ∧ r ≤ k then sourceCoefficient k i *
        ((k - i).choose (r - i) : ℝ) / ((2 * k + 1).choose r : ℝ) else 0 := by

commit-pinned source · Verso Blueprint panel

Lean checks the proposition indexed as “left coefficient nonneg”; the hypotheses and conclusion in the code panel fix its exact scope.

theorem leftCoefficient_nonneg (k r : ℕ) : 0 ≤ leftCoefficient k r := by

commit-pinned source · Verso Blueprint panel

Lean checks the proposition indexed as “left coefficient eval”; the hypotheses and conclusion in the code panel fix its exact scope. The collected coefficients evaluate to the literal source endpoint factor.

theorem leftCoefficient_eval (k : ℕ) (t : ℝ) :
    (∑ r ∈ Finset.range (2 * k + 2), leftCoefficient k r * basis (2 * k + 1) r t) =
      (endpointFactor k).eval t := by

commit-pinned source · Verso Blueprint panel

This definition gives the library's named construction or computation for “source bernstein coefficient”. The actual positive Bernstein coefficient vector of the source polynomial.

def sourceBernsteinCoefficient (k r : ℕ) : ℝ :=
  Real.exp (-1) * leftCoefficient k r + leftCoefficient k (2 * k + 1 - r)

commit-pinned source · Verso Blueprint panel

Lean checks the proposition indexed as “source bernstein coefficient nonneg”; the hypotheses and conclusion in the code panel fix its exact scope.

theorem sourceBernsteinCoefficient_nonneg (k r : ℕ) :
    0 ≤ sourceBernsteinCoefficient k r :=
  add_nonneg (mul_nonneg (Real.exp_pos _).le (leftCoefficient_nonneg k r))
    (leftCoefficient_nonneg k _)

/-- Reflection of a coefficient vector corresponds exactly to `t ↦ 1-t`. -/

commit-pinned source · Verso Blueprint panel

Lean checks the proposition indexed as “reflected sum”; the hypotheses and conclusion in the code panel fix its exact scope. Reflection of a coefficient vector corresponds exactly to 't ↦ 1-t'.

theorem reflected_sum (d : ℕ) (c : ℕ → ℝ) (t : ℝ) :
    (∑ r ∈ Finset.range (d + 1), c (d - r) * basis d r t) =
      ∑ r ∈ Finset.range (d + 1), c r * basis d r (1 - t) := by

commit-pinned source · Verso Blueprint panel

Lean checks the proposition indexed as “source interpolant bernstein”; the hypotheses and conclusion in the code panel fix its exact scope. Exact source-to-Bernstein bridge, valid for every real coordinate, not merely on '[0,1]'.

theorem sourceInterpolant_bernstein (k : ℕ) (t : ℝ) :
    (∑ r ∈ Finset.range (2 * k + 2),
      sourceBernsteinCoefficient k r * basis (2 * k + 1) r t) =
      (sourceInterpolant k).eval (t - 1) := by

commit-pinned source · Verso Blueprint panel

This definition gives the library's named construction or computation for “coefficient shift”. Shift a coefficient row by one entry.

def coefficientShift : Module.End ℝ (ℕ → ℝ) where
  toFun c i := c (i + 1)
  map_add' _ _ := rfl
  map_smul' _ _ := rfl

commit-pinned source · Verso Blueprint panel

Lean checks the proposition indexed as “coefficient shift pow”; the hypotheses and conclusion in the code panel fix its exact scope.

theorem coefficientShift_pow (n i : ℕ) (c : ℕ → ℝ) :
    (coefficientShift ^ n) c i = c (i + n) := by

commit-pinned source · Verso Blueprint panel

This definition gives the library's named construction or computation for “casteljau step”. One exact de Casteljau update on an infinite coefficient row.

def casteljauStep (t : ℝ) : Module.End ℝ (ℕ → ℝ) :=
  t • coefficientShift + (1 - t) • 1

commit-pinned source · Verso Blueprint panel

Lean checks the proposition indexed as “casteljau step apply”; the hypotheses and conclusion in the code panel fix its exact scope.

theorem casteljauStep_apply (t : ℝ) (c : ℕ → ℝ) (i : ℕ) :
    casteljauStep t c i = (1 - t) * c i + t * c (i + 1) := by

commit-pinned source · Verso Blueprint panel

This definition gives the library's named construction or computation for “casteljau”. Repeated rows of the exact de Casteljau triangle.

def casteljau (d : ℕ) (c : ℕ → ℝ) (t : ℝ) (i : ℕ) : ℝ :=
  (casteljauStep t ^ d) c i

commit-pinned source · Verso Blueprint panel

Lean checks the proposition indexed as “casteljau eq sum”; the hypotheses and conclusion in the code panel fix its exact scope.

theorem casteljau_eq_sum (d : ℕ) (c : ℕ → ℝ) (t : ℝ) (i : ℕ) :
    casteljau d c t i = ∑ j ∈ Finset.range (d + 1), c (i + j) * basis d j t := by

commit-pinned source · Verso Blueprint panel

This definition gives the library's named construction or computation for “left restriction”. Left edge of the de Casteljau triangle: coefficients on '[0,u]'.

def leftRestriction (u : ℝ) (c : ℕ → ℝ) (i : ℕ) : ℝ := casteljau i c u 0

commit-pinned source · Verso Blueprint panel

Lean checks the proposition indexed as “casteljau step mul parameter”; the hypotheses and conclusion in the code panel fix its exact scope.

theorem casteljauStep_mul_parameter (u t : ℝ) :
    casteljauStep (u * t) = (1 - t) • (1 : Module.End ℝ (ℕ → ℝ)) +
      t • casteljauStep u := by

commit-pinned source · Verso Blueprint panel

Lean checks the proposition indexed as “left restriction step”; the hypotheses and conclusion in the code panel fix its exact scope.

theorem leftRestriction_step (u t : ℝ) (c : ℕ → ℝ) :
    leftRestriction u (casteljauStep (u * t) c) =
      casteljauStep t (leftRestriction u c) := by

commit-pinned source · Verso Blueprint panel

Lean checks the proposition indexed as “casteljau left restriction”; the hypotheses and conclusion in the code panel fix its exact scope. The left subdivision evaluates the original polynomial at 'u*t'.

theorem casteljau_leftRestriction (d : ℕ) (c : ℕ → ℝ) (u t : ℝ) :
    casteljau d (leftRestriction u c) t 0 = casteljau d c (u * t) 0 := by

commit-pinned source · Verso Blueprint panel

Lean checks the proposition indexed as “left restriction eval”; the hypotheses and conclusion in the code panel fix its exact scope. Exact coefficient-level semantics of left de Casteljau subdivision.

theorem leftRestriction_eval (d : ℕ) (c : ℕ → ℝ) (u t : ℝ) :
    (∑ r ∈ Finset.range (d + 1), leftRestriction u c r * basis d r t) =
      ∑ r ∈ Finset.range (d + 1), c r * basis d r (u * t) := by

commit-pinned source · Verso Blueprint panel

This definition gives the library's named construction or computation for “right restriction”. Right edge of the de Casteljau triangle, equivalently reflected left subdivision.

def rightRestriction (d : ℕ) (u : ℝ) (c : ℕ → ℝ) (i : ℕ) : ℝ :=
  leftRestriction (1 - u) (fun r => c (d - r)) (d - i)

commit-pinned source · Verso Blueprint panel

Lean checks the proposition indexed as “right restriction eq casteljau”; the hypotheses and conclusion in the code panel fix its exact scope.

theorem rightRestriction_eq_casteljau (d i : ℕ) (hi : i ≤ d) (u : ℝ) (c : ℕ → ℝ) :
    rightRestriction d u c i = casteljau (d - i) c u i := by

commit-pinned source · Verso Blueprint panel

Lean checks the proposition indexed as “right restriction eval”; the hypotheses and conclusion in the code panel fix its exact scope.

theorem rightRestriction_eval (d : ℕ) (c : ℕ → ℝ) (u t : ℝ) :
    (∑ r ∈ Finset.range (d + 1), rightRestriction d u c r * basis d r t) =
      ∑ r ∈ Finset.range (d + 1), c r * basis d r (u + (1 - u) * t) := by

commit-pinned source · Verso Blueprint panel

This definition gives the library's named construction or computation for “restrict coefficients”. The candidate's two successive subdivisions restricting to '[u,v]'.

def restrictCoefficients (d : ℕ) (u v : ℝ) (c : ℕ → ℝ) : ℕ → ℝ :=
  leftRestriction ((v - u) / (1 - u)) (rightRestriction d u c)

/-- Exact affine restriction; no floating-point quantities occur. -/

commit-pinned source · Verso Blueprint panel

Lean checks the proposition indexed as “restrict coefficients eval”; the hypotheses and conclusion in the code panel fix its exact scope. Exact affine restriction; no floating-point quantities occur.

theorem restrictCoefficients_eval (d : ℕ) (c : ℕ → ℝ) (u v t : ℝ) (hu : u ≠ 1) :
    (∑ r ∈ Finset.range (d + 1), restrictCoefficients d u v c r * basis d r t) =
      ∑ r ∈ Finset.range (d + 1), c r * basis d r (u + (v - u) * t) := by

commit-pinned source · Verso Blueprint panel

Lean checks the proposition indexed as “basis sum”; the hypotheses and conclusion in the code panel fix its exact scope.

theorem basis_sum (d : ℕ) (t : ℝ) :
    (∑ r ∈ Finset.range (d + 1), basis d r t) = 1 := by

commit-pinned source · Verso Blueprint panel

Lean checks the proposition indexed as “bernstein sum bounds”; the hypotheses and conclusion in the code panel fix its exact scope. Bernstein evaluation lies in any common interval containing its coefficients.

theorem bernstein_sum_bounds (d : ℕ) (c : ℕ → ℝ) (t lo hi : ℝ)
    (ht : t ∈ Set.Icc 0 1) (hc : ∀ r ≤ d, c r ∈ Set.Icc lo hi) :
    (∑ r ∈ Finset.range (d + 1), c r * basis d r t) ∈ Set.Icc lo hi := by

commit-pinned source · Verso Blueprint panel

Lean checks the proposition indexed as “left restriction bounds”; the hypotheses and conclusion in the code panel fix its exact scope.

theorem leftRestriction_bounds (d : ℕ) (c : ℕ → ℝ) (u lo hi : ℝ)
    (hu : u ∈ Set.Icc 0 1) (hc : ∀ r ≤ d, c r ∈ Set.Icc lo hi)
    (i : ℕ) (hi' : i ≤ d) : leftRestriction u c i ∈ Set.Icc lo hi := by

commit-pinned source · Verso Blueprint panel

Lean checks the proposition indexed as “right restriction bounds”; the hypotheses and conclusion in the code panel fix its exact scope.

theorem rightRestriction_bounds (d : ℕ) (c : ℕ → ℝ) (u lo hi : ℝ)
    (hu : u ∈ Set.Icc 0 1) (hc : ∀ r ≤ d, c r ∈ Set.Icc lo hi)
    (i : ℕ) : rightRestriction d u c i ∈ Set.Icc lo hi := by

commit-pinned source · Verso Blueprint panel

Lean checks the proposition indexed as “restrict coefficients bounds”; the hypotheses and conclusion in the code panel fix its exact scope. Every restricted coefficient remains in the original coefficient bounds.

theorem restrictCoefficients_bounds (d : ℕ) (c : ℕ → ℝ) (u v lo hi : ℝ)
    (hu : 0 ≤ u) (huv : u < v) (hv : v ≤ 1)
    (hc : ∀ r ≤ d, c r ∈ Set.Icc lo hi) (i : ℕ) (hi' : i ≤ d) :
    restrictCoefficients d u v c i ∈ Set.Icc lo hi := by

commit-pinned source · Verso Blueprint panel

Lean checks the proposition indexed as “basis half”; the hypotheses and conclusion in the code panel fix its exact scope.

theorem basis_half (d r : ℕ) (hr : r ≤ d) :
    basis d r (1 / 2) = (d.choose r : ℝ) / 2 ^ d := by

commit-pinned source · Verso Blueprint panel

Lean checks the proposition indexed as “left restriction half”; the hypotheses and conclusion in the code panel fix its exact scope. The lower half-interval subdivision row is the candidate's binomial row.

theorem leftRestriction_half (c : ℕ → ℝ) (i : ℕ) :
    leftRestriction (1 / 2) c i =
      ∑ j ∈ Finset.range (i + 1), c j * (i.choose j : ℝ) / 2 ^ i := by

commit-pinned source · Verso Blueprint panel

Lean checks the proposition indexed as “right restriction half”; the hypotheses and conclusion in the code panel fix its exact scope. The upper half-interval subdivision row, with 'j' the offset from row 'i'.

theorem rightRestriction_half (d i : ℕ) (hi : i ≤ d) (c : ℕ → ℝ) :
    rightRestriction d (1 / 2) c i =
      ∑ j ∈ Finset.range (d - i + 1),
        c (i + j) * ((d - i).choose j : ℝ) / 2 ^ (d - i) := by

commit-pinned source · Verso Blueprint panel

Lean checks the proposition indexed as “source interpolant restricted”; the hypotheses and conclusion in the code panel fix its exact scope. The complete exact source/restriction bridge needed by Bernstein injection.

theorem sourceInterpolant_restricted (k : ℕ) (u v t : ℝ) (hu : u ≠ 1) :
    (∑ r ∈ Finset.range (2 * k + 2),
      restrictCoefficients (2 * k + 1) u v (sourceBernsteinCoefficient k) r *
        basis (2 * k + 1) r t) =
      (sourceInterpolant k).eval (u + (v - u) * t - 1) := by

commit-pinned source · Verso Blueprint panel

This definition gives the library's named construction or computation for “half subdivision”. Exact coefficient update for one binary digit; 'false' is the lower child.

def halfSubdivision (d : ℕ) (bit : Bool) (c : ℕ → ℝ) : ℕ → ℝ :=
  if bit then rightRestriction d (1 / 2) c else leftRestriction (1 / 2) c

/-- The local coordinate of one binary child. -/

commit-pinned source · Verso Blueprint panel

This definition gives the library's named construction or computation for “child coordinate”. The local coordinate of one binary child.

def childCoordinate (bit : Bool) (t : ℝ) : ℝ :=
  if bit then (1 + t) / 2 else t / 2

commit-pinned source · Verso Blueprint panel

Lean checks the proposition indexed as “half subdivision eval”; the hypotheses and conclusion in the code panel fix its exact scope.

theorem halfSubdivision_eval (d : ℕ) (c : ℕ → ℝ) (bit : Bool) (t : ℝ) :
    (∑ r ∈ Finset.range (d + 1), halfSubdivision d bit c r * basis d r t) =
      ∑ r ∈ Finset.range (d + 1), c r * basis d r (childCoordinate bit t) := by

commit-pinned source · Verso Blueprint panel

This definition gives the library's named construction or computation for “subdivision path”. Successive binary subdivisions in MSB-first order.

def subdivisionPath (d : ℕ) (c : ℕ → ℝ) : List Bool → (ℕ → ℝ)
  | [] => c
  | bit :: bits => subdivisionPath d (halfSubdivision d bit c) bits

/-- Composition of the same MSB-first binary-child coordinate maps. -/

commit-pinned source · Verso Blueprint panel

This definition gives the library's named construction or computation for “path coordinate”. Composition of the same MSB-first binary-child coordinate maps.

def pathCoordinate : List Bool → ℝ → ℝ
  | [], t => t
  | bit :: bits, t => childCoordinate bit (pathCoordinate bits t)

/-- The shared Bernstein state is exact after any finite bit prefix. -/

commit-pinned source · Verso Blueprint panel

Lean checks the proposition indexed as “subdivision path eval”; the hypotheses and conclusion in the code panel fix its exact scope. The shared Bernstein state is exact after any finite bit prefix.

theorem subdivisionPath_eval (d : ℕ) (c : ℕ → ℝ) (bits : List Bool) (t : ℝ) :
    (∑ r ∈ Finset.range (d + 1), subdivisionPath d c bits r * basis d r t) =
      ∑ r ∈ Finset.range (d + 1), c r * basis d r (pathCoordinate bits t) := by

commit-pinned source · Verso Blueprint panel

Lean checks the proposition indexed as “bernstein eval zero”; the hypotheses and conclusion in the code panel fix its exact scope.

theorem bernstein_eval_zero (d : ℕ) (c : ℕ → ℝ) :
    (∑ r ∈ Finset.range (d + 1), c r * basis d r 0) = c 0 := by

commit-pinned source · Verso Blueprint panel

Lean checks the proposition indexed as “subdivision path readout”; the hypotheses and conclusion in the code panel fix its exact scope. The zeroth coefficient after the last digit is the value at the represented left endpoint.

theorem subdivisionPath_readout (d : ℕ) (c : ℕ → ℝ) (bits : List Bool) :
    subdivisionPath d c bits 0 =
      ∑ r ∈ Finset.range (d + 1), c r * basis d r (pathCoordinate bits 0) := by

commit-pinned source · Verso Blueprint panel

Lean checks the proposition indexed as “source interpolant subdivision readout”; the hypotheses and conclusion in the code panel fix its exact scope. Source-correct readout from a restricted Bernstein injection followed by any finite MSB-first suffix.

theorem sourceInterpolant_subdivision_readout (k : ℕ) (u v : ℝ) (hu : u ≠ 1)
    (bits : List Bool) :
    subdivisionPath (2 * k + 1)
      (restrictCoefficients (2 * k + 1) u v (sourceBernsteinCoefficient k)) bits 0 =
      (sourceInterpolant k).eval (u + (v - u) * pathCoordinate bits 0 - 1) := by

commit-pinned source · Verso Blueprint panel