10.15. QuantumBlockEncoding/HermitePolynomialResources.lean🔗

1 explicit public declarations, in source order.

Theorem10.15.1

uses 0used by 0✓L∃∀N

Plain-English reading. Lean checks the proposition indexed as “exists polynomial resources”; the hypotheses and conclusion in the code panel fix its exact scope.

Formal status. Compiled theorem in the default ASPBE import surface; the displayed Lean signature is the authoritative claim.

Why it is in this chapter. Paper-facing backend models, source-specific Hermite constructions, and concrete State Preparation / Robin example artifacts.

Technical source note. The source declaration has no docstring. The reader cue above is generated from its kind and name and does not replace the Lean signature.

Declaration kind. theorem.

Source: QuantumBlockEncoding/HermitePolynomialResources.lean:11. A commit-pinned external link is added by the publication build when the source exists at the published ref.

Lean code for Theorem10.15.1●1 theorem

theoremdefined in QuantumBlockEncoding/HermitePolynomialResources.lean

complete

theorem QuantumBlockEncoding.HermitePolynomialPreparation.exists_polynomial_resources
  (k n : ℕ) (L : ℝ) (hL : 0 < L) :
  ∃ circuit,
    circuit.gateCount ≤ 48 * (n + 1) * (2 * k + 6) ^ 3 ∧
      circuit.resource.depth ≤ 48 * (n + 1) * (2 * k + 6) ^ 3 ∧
        circuit.resource.oracleCalls = 0 ∧
          QuantumBlockEncoding.evalPrimitiveCircuit circuit ∈
              Matrix.unitaryGroup
                (QuantumBlockEncoding.PrimitiveBasis
                  (n + 1 +
                    QuantumBlockEncoding.HermiteFiniteChain.bondQubits
                      k))
                ℂ ∧
            ∀ (x : QuantumBlockEncoding.PrimitiveBasis (n + 1))
              (b :
                QuantumBlockEncoding.PrimitiveBasis
                  (QuantumBlockEncoding.HermiteFiniteChain.bondQubits
                    k)),
              (QuantumBlockEncoding.evalPrimitiveCircuit circuit
                  (Fin.append x b) fun x => 0) =
                if b = fun x => 0 then
                  QuantumBlockEncoding.HermiteStatePreparation.normalizedAmplitude
                    k (n + 1) L
                    ((QuantumBlockEncoding.primitiveBasisLEEquiv
                        (n + 1))
                      x)
                else 0

theorem QuantumBlockEncoding.HermitePolynomialPreparation.exists_polynomial_resources
  (k n : ℕ) (L : ℝ) (hL : 0 < L) :
  ∃ circuit,
    circuit.gateCount ≤
        48 * (n + 1) * (2 * k + 6) ^ 3 ∧
      circuit.resource.depth ≤
          48 * (n + 1) * (2 * k + 6) ^ 3 ∧
        circuit.resource.oracleCalls = 0 ∧
          QuantumBlockEncoding.evalPrimitiveCircuit
                circuit ∈
              Matrix.unitaryGroup
                (QuantumBlockEncoding.PrimitiveBasis
                  (n + 1 +
                    QuantumBlockEncoding.HermiteFiniteChain.bondQubits
                      k))
                ℂ ∧
            ∀
              (x :
                QuantumBlockEncoding.PrimitiveBasis
                  (n + 1))
              (b :
                QuantumBlockEncoding.PrimitiveBasis
                  (QuantumBlockEncoding.HermiteFiniteChain.bondQubits
                    k)),
              (QuantumBlockEncoding.evalPrimitiveCircuit
                  circuit (Fin.append x b)
                  fun x => 0) =
                if b = fun x => 0 then
                  QuantumBlockEncoding.HermiteStatePreparation.normalizedAmplitude
                    k (n + 1) L
                    ((QuantumBlockEncoding.primitiveBasisLEEquiv
                        (n + 1))
                      x)
                else 0