10.17. QuantumBlockEncoding/HermiteSmoothness.lean🔗

12 explicit public declarations, in source order.

Definition10.17.1

uses 0used by 0✓L∃∀N

Plain-English reading. This definition gives the library's named construction or computation for “splice”. Join two real functions at a threshold, taking the right value at the threshold.

Formal status. Compiled declaration in the default ASPBE import surface; its kind and displayed Lean type determine how it may be used.

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

Technical source note. Join two real functions at a threshold, taking the right value at the threshold.

Declaration kind. def.

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

Lean code for Definition10.17.1●1 definition

defdefined in QuantumBlockEncoding/HermiteSmoothness.lean

complete

def QuantumBlockEncoding.HermiteSmoothness.splice (c : ℝ) (f g : ℝ → ℝ)
  (x : ℝ) : ℝ

def QuantumBlockEncoding.HermiteSmoothness.splice
  (c : ℝ) (f g : ℝ → ℝ) (x : ℝ) : ℝ

Join two real functions at a threshold, taking the right value at the threshold.

Theorem10.17.2

uses 0used by 0✓L∃∀N

Plain-English reading. Lean checks the proposition indexed as “has deriv at ite of eq”; the hypotheses and conclusion in the code panel fix its exact scope. Any selector preserves a common derivative when both branch values agree.

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. Any selector preserves a common derivative when both branch values agree.

Declaration kind. theorem.

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

Lean code for Theorem10.17.2●1 theorem

theoremdefined in QuantumBlockEncoding/HermiteSmoothness.lean

complete

theorem QuantumBlockEncoding.HermiteSmoothness.hasDerivAt_ite_of_eq
  (pred : ℝ → Prop) [DecidablePred pred] {f g : ℝ → ℝ} {d x : ℝ}
  (hf : HasDerivAt f d x) (hg : HasDerivAt g d x) (hv : f x = g x) :
  HasDerivAt (fun y => if pred y then f y else g y) d x

theorem QuantumBlockEncoding.HermiteSmoothness.hasDerivAt_ite_of_eq
  (pred : ℝ → Prop) [DecidablePred pred]
  {f g : ℝ → ℝ} {d x : ℝ}
  (hf : HasDerivAt f d x)
  (hg : HasDerivAt g d x)
  (hv : f x = g x) :
  HasDerivAt
    (fun y => if pred y then f y else g y)
    d x

Any selector preserves a common derivative when both branch values agree.

Theorem10.17.3

uses 0used by 0✓L∃∀N

Plain-English reading. Lean checks the proposition indexed as “has deriv at splice”; 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/HermiteSmoothness.lean:38. A commit-pinned external link is added by the publication build when the source exists at the published ref.

Lean code for Theorem10.17.3●1 theorem

theoremdefined in QuantumBlockEncoding/HermiteSmoothness.lean

complete

theorem QuantumBlockEncoding.HermiteSmoothness.hasDerivAt_splice (c : ℝ)
  (f g : ℝ → ℝ) (hf : Differentiable ℝ f) (hg : Differentiable ℝ g)
  (hv : f c = g c) (hd : deriv f c = deriv g c) (x : ℝ) :
  HasDerivAt (QuantumBlockEncoding.HermiteSmoothness.splice c f g)
    (QuantumBlockEncoding.HermiteSmoothness.splice c (deriv f) (deriv g)
      x)
    x

theorem QuantumBlockEncoding.HermiteSmoothness.hasDerivAt_splice
  (c : ℝ) (f g : ℝ → ℝ)
  (hf : Differentiable ℝ f)
  (hg : Differentiable ℝ g)
  (hv : f c = g c)
  (hd : deriv f c = deriv g c) (x : ℝ) :
  HasDerivAt
    (QuantumBlockEncoding.HermiteSmoothness.splice
      c f g)
    (QuantumBlockEncoding.HermiteSmoothness.splice
      c (deriv f) (deriv g) x)
    x

Theorem10.17.4

uses 0used by 0✓L∃∀N

Plain-English reading. Lean checks the proposition indexed as “deriv splice”; 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/HermiteSmoothness.lean:56. A commit-pinned external link is added by the publication build when the source exists at the published ref.

Lean code for Theorem10.17.4●1 theorem

theoremdefined in QuantumBlockEncoding/HermiteSmoothness.lean

complete

theorem QuantumBlockEncoding.HermiteSmoothness.deriv_splice (c : ℝ)
  (f g : ℝ → ℝ) (hf : Differentiable ℝ f) (hg : Differentiable ℝ g)
  (hv : f c = g c) (hd : deriv f c = deriv g c) :
  deriv (QuantumBlockEncoding.HermiteSmoothness.splice c f g) =
    QuantumBlockEncoding.HermiteSmoothness.splice c (deriv f) (deriv g)

theorem QuantumBlockEncoding.HermiteSmoothness.deriv_splice
  (c : ℝ) (f g : ℝ → ℝ)
  (hf : Differentiable ℝ f)
  (hg : Differentiable ℝ g)
  (hv : f c = g c)
  (hd : deriv f c = deriv g c) :
  deriv
      (QuantumBlockEncoding.HermiteSmoothness.splice
        c f g) =
    QuantumBlockEncoding.HermiteSmoothness.splice
      c (deriv f) (deriv g)

Theorem10.17.5

uses 0used by 0✓L∃∀N

Plain-English reading. Lean checks the proposition indexed as “cont diff splice”; the hypotheses and conclusion in the code panel fix its exact scope. Two 'C^k' real functions glue to a 'C^k' function if their jets agree at the cut.

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. Two 'C^k' real functions glue to a 'C^k' function if their jets agree at the cut.

Declaration kind. theorem.

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

Lean code for Theorem10.17.5●1 theorem

theoremdefined in QuantumBlockEncoding/HermiteSmoothness.lean

complete

theorem QuantumBlockEncoding.HermiteSmoothness.contDiff_splice (k : ℕ) (c : ℝ)
  (f g : ℝ → ℝ) (hf : ContDiff ℝ (↑k) f) (hg : ContDiff ℝ (↑k) g)
  (hjet : ∀ j ≤ k, iteratedDeriv j f c = iteratedDeriv j g c) :
  ContDiff ℝ (↑k) (QuantumBlockEncoding.HermiteSmoothness.splice c f g)

theorem QuantumBlockEncoding.HermiteSmoothness.contDiff_splice
  (k : ℕ) (c : ℝ) (f g : ℝ → ℝ)
  (hf : ContDiff ℝ (↑k) f)
  (hg : ContDiff ℝ (↑k) g)
  (hjet :
    ∀ j ≤ k,
      iteratedDeriv j f c =
        iteratedDeriv j g c) :
  ContDiff ℝ (↑k)
    (QuantumBlockEncoding.HermiteSmoothness.splice
      c f g)

Two `C^k` real functions glue to a `C^k` function if their jets agree at the cut.

Theorem10.17.6

uses 0used by 0✓L∃∀N

Plain-English reading. Lean checks the proposition indexed as “iterated deriv exp”; 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/HermiteSmoothness.lean:92. A commit-pinned external link is added by the publication build when the source exists at the published ref.

Lean code for Theorem10.17.6●1 theorem

theoremdefined in QuantumBlockEncoding/HermiteSmoothness.lean

complete

theorem QuantumBlockEncoding.HermiteSmoothness.iteratedDeriv_exp (j : ℕ)
  (x : ℝ) : iteratedDeriv j Real.exp x = Real.exp x

theorem QuantumBlockEncoding.HermiteSmoothness.iteratedDeriv_exp
  (j : ℕ) (x : ℝ) :
  iteratedDeriv j Real.exp x = Real.exp x

Theorem10.17.7

uses 0used by 0✓L∃∀N

Plain-English reading. Lean checks the proposition indexed as “iterated deriv exp neg”; 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/HermiteSmoothness.lean:95. A commit-pinned external link is added by the publication build when the source exists at the published ref.

Lean code for Theorem10.17.7●1 theorem

theoremdefined in QuantumBlockEncoding/HermiteSmoothness.lean

complete

theorem QuantumBlockEncoding.HermiteSmoothness.iteratedDeriv_exp_neg (j : ℕ)
  (x : ℝ) :
  iteratedDeriv j (fun y => Real.exp (-y)) x = (-1) ^ j * Real.exp (-x)

theorem QuantumBlockEncoding.HermiteSmoothness.iteratedDeriv_exp_neg
  (j : ℕ) (x : ℝ) :
  iteratedDeriv j (fun y => Real.exp (-y))
      x =
    (-1) ^ j * Real.exp (-x)

Theorem10.17.8

uses 0used by 0✓L∃∀N

Plain-English reading. Lean checks the proposition indexed as “cont diff right splice”; the hypotheses and conclusion in the code panel fix its exact scope. First join: the source polynomial and right exponential meet smoothly at zero.

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. First join: the source polynomial and right exponential meet smoothly at zero.

Declaration kind. theorem.

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

Lean code for Theorem10.17.8●1 theorem

theoremdefined in QuantumBlockEncoding/HermiteSmoothness.lean

complete

theorem QuantumBlockEncoding.HermiteSmoothness.contDiff_right_splice (k : ℕ) :
  ContDiff ℝ (↑k)
    (QuantumBlockEncoding.HermiteSmoothness.splice 0
      (fun p =>
        Polynomial.eval p
          (QuantumBlockEncoding.HermitePolynomial.sourceInterpolant k))
      fun p => Real.exp (-p))

theorem QuantumBlockEncoding.HermiteSmoothness.contDiff_right_splice
  (k : ℕ) :
  ContDiff ℝ (↑k)
    (QuantumBlockEncoding.HermiteSmoothness.splice
      0
      (fun p =>
        Polynomial.eval p
          (QuantumBlockEncoding.HermitePolynomial.sourceInterpolant
            k))
      fun p => Real.exp (-p))

First join: the source polynomial and right exponential meet smoothly at zero.

Theorem10.17.9

uses 0used by 0✓L∃∀N

Plain-English reading. Lean checks the proposition indexed as “right splice eventually eq”; the hypotheses and conclusion in the code panel fix its exact scope. The right splice coincides with the polynomial on a neighborhood of the left junction.

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 right splice coincides with the polynomial on a neighborhood of the left junction.

Declaration kind. theorem.

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

Lean code for Theorem10.17.9●1 theorem

theoremdefined in QuantumBlockEncoding/HermiteSmoothness.lean

complete

theorem QuantumBlockEncoding.HermiteSmoothness.right_splice_eventuallyEq
  (k : ℕ) :
  (QuantumBlockEncoding.HermiteSmoothness.splice 0
      (fun p =>
        Polynomial.eval p
          (QuantumBlockEncoding.HermitePolynomial.sourceInterpolant k))
      fun p => Real.exp (-p)) =ᶠ[nhds (-1)]
    fun p =>
    Polynomial.eval p
      (QuantumBlockEncoding.HermitePolynomial.sourceInterpolant k)

theorem QuantumBlockEncoding.HermiteSmoothness.right_splice_eventuallyEq
  (k : ℕ) :
  (QuantumBlockEncoding.HermiteSmoothness.splice
      0
      (fun p =>
        Polynomial.eval p
          (QuantumBlockEncoding.HermitePolynomial.sourceInterpolant
            k))
      fun p =>
      Real.exp (-p)) =ᶠ[nhds (-1)]
    fun p =>
    Polynomial.eval p
      (QuantumBlockEncoding.HermitePolynomial.sourceInterpolant
        k)

The right splice coincides with the polynomial on a neighborhood of the left junction.

Theorem10.17.10

uses 0used by 0✓L∃∀N

Plain-English reading. Lean checks the proposition indexed as “cont diff double splice”; the hypotheses and conclusion in the code panel fix its exact scope. Two applications of the reusable gluing theorem close both source junctions.

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. Two applications of the reusable gluing theorem close both source junctions.

Declaration kind. theorem.

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

Lean code for Theorem10.17.10●1 theorem

theoremdefined in QuantumBlockEncoding/HermiteSmoothness.lean

complete

theorem QuantumBlockEncoding.HermiteSmoothness.contDiff_double_splice (k : ℕ) :
  ContDiff ℝ (↑k)
    (QuantumBlockEncoding.HermiteSmoothness.splice (-1) Real.exp
      (QuantumBlockEncoding.HermiteSmoothness.splice 0
        (fun p =>
          Polynomial.eval p
            (QuantumBlockEncoding.HermitePolynomial.sourceInterpolant
              k))
        fun p => Real.exp (-p)))

theorem QuantumBlockEncoding.HermiteSmoothness.contDiff_double_splice
  (k : ℕ) :
  ContDiff ℝ (↑k)
    (QuantumBlockEncoding.HermiteSmoothness.splice
      (-1) Real.exp
      (QuantumBlockEncoding.HermiteSmoothness.splice
        0
        (fun p =>
          Polynomial.eval p
            (QuantumBlockEncoding.HermitePolynomial.sourceInterpolant
              k))
        fun p => Real.exp (-p)))

Two applications of the reusable gluing theorem close both source junctions.

Theorem10.17.11

uses 0used by 0✓L∃∀N

Plain-English reading. Lean checks the proposition indexed as “smooth initial eq double splice”; the hypotheses and conclusion in the code panel fix its exact scope. The original '≤ 0' middle-branch convention equals the smooth double splice exactly.

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 original '≤ 0' middle-branch convention equals the smooth double splice exactly.

Declaration kind. theorem.

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

Lean code for Theorem10.17.11●1 theorem

theoremdefined in QuantumBlockEncoding/HermiteSmoothness.lean

complete

theorem QuantumBlockEncoding.HermiteSmoothness.smoothInitial_eq_double_splice
  (k : ℕ) :
  QuantumBlockEncoding.HermitePolynomial.smoothInitial k =
    QuantumBlockEncoding.HermiteSmoothness.splice (-1) Real.exp
      (QuantumBlockEncoding.HermiteSmoothness.splice 0
        (fun p =>
          Polynomial.eval p
            (QuantumBlockEncoding.HermitePolynomial.sourceInterpolant
              k))
        fun p => Real.exp (-p))

theorem QuantumBlockEncoding.HermiteSmoothness.smoothInitial_eq_double_splice
  (k : ℕ) :
  QuantumBlockEncoding.HermitePolynomial.smoothInitial
      k =
    QuantumBlockEncoding.HermiteSmoothness.splice
      (-1) Real.exp
      (QuantumBlockEncoding.HermiteSmoothness.splice
        0
        (fun p =>
          Polynomial.eval p
            (QuantumBlockEncoding.HermitePolynomial.sourceInterpolant
              k))
        fun p => Real.exp (-p))

The original `≤ 0` middle-branch convention equals the smooth double splice exactly.

Theorem10.17.12

uses 0used by 0✓L∃∀N

Plain-English reading. Lean checks the proposition indexed as “smooth initial cont diff”; the hypotheses and conclusion in the code panel fix its exact scope. The literal source initial datum is globally 'C^k', for every natural order 'k'.

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 literal source initial datum is globally 'C^k', for every natural order 'k'.

Declaration kind. theorem.

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

Lean code for Theorem10.17.12●1 theorem

theoremdefined in QuantumBlockEncoding/HermiteSmoothness.lean

complete

theorem QuantumBlockEncoding.HermiteSmoothness.smoothInitial_contDiff (k : ℕ) :
  ContDiff ℝ (↑k)
    (QuantumBlockEncoding.HermitePolynomial.smoothInitial k)

theorem QuantumBlockEncoding.HermiteSmoothness.smoothInitial_contDiff
  (k : ℕ) :
  ContDiff ℝ (↑k)
    (QuantumBlockEncoding.HermitePolynomial.smoothInitial
      k)

The literal source initial datum is globally `C^k`, for every natural order `k`.