QuantumBlockEncoding/HermiteSmoothness.lean

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.

def splice (c : ℝ) (f g : ℝ → ℝ) (x : ℝ) : ℝ := if x < c then f x else g x

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

commit-pinned source · Verso Blueprint panel

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.

theorem 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 := by

commit-pinned source · Verso Blueprint panel

Lean checks the proposition indexed as “has deriv at splice”; the hypotheses and conclusion in the code panel fix its exact scope.

theorem 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 (splice c f g) (splice c (deriv f) (deriv g) x) x := by

commit-pinned source · Verso Blueprint panel

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

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

commit-pinned source · Verso Blueprint panel

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.

theorem 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 (splice c f g) := by

commit-pinned source · Verso Blueprint panel

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

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

commit-pinned source · Verso Blueprint panel

Lean checks the proposition indexed as “iterated deriv exp neg”; the hypotheses and conclusion in the code panel fix its exact scope.

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

commit-pinned source · Verso Blueprint panel

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.

theorem contDiff_right_splice (k : ℕ) :
    ContDiff ℝ k
      (splice 0 (fun p => (sourceInterpolant k).eval p) (fun p => Real.exp (-p))) := by

commit-pinned source · Verso Blueprint panel

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.

theorem right_splice_eventuallyEq (k : ℕ) :
    splice 0 (fun p => (sourceInterpolant k).eval p) (fun p => Real.exp (-p))
      =ᶠ[𝓝 (-1)] (fun p => (sourceInterpolant k).eval p) := by

commit-pinned source · Verso Blueprint panel

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.

theorem contDiff_double_splice (k : ℕ) :
    ContDiff ℝ k
      (splice (-1) Real.exp
        (splice 0 (fun p => (sourceInterpolant k).eval p) (fun p => Real.exp (-p)))) := by

commit-pinned source · Verso Blueprint panel

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.

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

commit-pinned source · Verso Blueprint panel

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'.

theorem smoothInitial_contDiff (k : ℕ) : ContDiff ℝ k (smoothInitial k) := by

commit-pinned source · Verso Blueprint panel