This definition gives the library's named construction or computation for “jet polynomial”. The truncated Taylor polynomial with the prescribed ordinary derivatives.
def jetPolynomial (a : ℝ) (k : ℕ) (v : ℕ → ℝ) : ℝ[X] :=
taylor (-a) (∑ j ∈ Finset.range (k + 1), monomial j (v j / (j.factorial : ℝ)))
/-- Convert Taylor coefficients to ordinary iterated derivatives. -/
commit-pinned source · Verso Blueprint panel
Lean checks the proposition indexed as “eval iterate derivative”; the hypotheses and conclusion in the code panel fix its exact scope. Convert Taylor coefficients to ordinary iterated derivatives.
theorem eval_iterate_derivative (p : ℝ[X]) (a : ℝ) (j : ℕ) :
(derivative^[j] p).eval a = (j.factorial : ℝ) * (taylor a p).coeff j := by
commit-pinned source · Verso Blueprint panel
Lean checks the proposition indexed as “jet polynomial jet”; the hypotheses and conclusion in the code panel fix its exact scope. Every requested jet is realized by its local Taylor polynomial.
theorem jetPolynomial_jet (a : ℝ) (k j : ℕ) (v : ℕ → ℝ) (hj : j ≤ k) :
(derivative^[j] (jetPolynomial a k v)).eval a = v j := by
commit-pinned source · Verso Blueprint panel
Lean checks the proposition indexed as “jet eq of pow dvd sub”; the hypotheses and conclusion in the code panel fix its exact scope. A high-multiplicity zero preserves all derivatives below the multiplicity.
theorem jet_eq_of_pow_dvd_sub (p q : ℝ[X]) (a : ℝ) (k j : ℕ)
(hj : j ≤ k) (h : (X - C a) ^ (k + 1) ∣ p - q) :
(derivative^[j] p).eval a = (derivative^[j] q).eval a := by
commit-pinned source · Verso Blueprint panel
This definition gives the library's named construction or computation for “bezout normalizer”. The inverse constant that normalizes the extended-gcd identity.
def bezoutNormalizer (A B : ℝ[X]) : ℝ[X] :=
C ((EuclideanDomain.gcd A B).coeff 0)⁻¹
commit-pinned source · Verso Blueprint panel
Lean checks the proposition indexed as “bezout normalizer gcd”; the hypotheses and conclusion in the code panel fix its exact scope.
theorem bezoutNormalizer_gcd (A B : ℝ[X]) (h : IsCoprime A B) :
bezoutNormalizer A B * EuclideanDomain.gcd A B = 1 := by
commit-pinned source · Verso Blueprint panel
This definition gives the library's named construction or computation for “two point interpolant”. An explicit Chinese-remainder interpolant, using extended Euclid.
def twoPointInterpolant (A B u v : ℝ[X]) : ℝ[X] :=
(bezoutNormalizer A B *
(B * EuclideanDomain.gcdB A B * u + A * EuclideanDomain.gcdA A B * v)) %
(A * B)
commit-pinned source · Verso Blueprint panel
Lean checks the proposition indexed as “two point interpolant left”; the hypotheses and conclusion in the code panel fix its exact scope.
theorem twoPointInterpolant_left (A B u v : ℝ[X]) (h : IsCoprime A B) :
A ∣ twoPointInterpolant A B u v - u := by
commit-pinned source · Verso Blueprint panel
Lean checks the proposition indexed as “two point interpolant right”; the hypotheses and conclusion in the code panel fix its exact scope.
theorem twoPointInterpolant_right (A B u v : ℝ[X]) (h : IsCoprime A B) :
B ∣ twoPointInterpolant A B u v - v := by
commit-pinned source · Verso Blueprint panel
This definition gives the library's named construction or computation for “left modulus”. The multiplicity polynomial for the endpoint '-1'.
def leftModulus (k : ℕ) : ℝ[X] := (X - C (-1)) ^ (k + 1)
/-- The multiplicity polynomial for the endpoint `0`. -/
commit-pinned source · Verso Blueprint panel
This definition gives the library's named construction or computation for “right modulus”. The multiplicity polynomial for the endpoint '0'.
def rightModulus (k : ℕ) : ℝ[X] := (X - C 0) ^ (k + 1)
commit-pinned source · Verso Blueprint panel
Lean checks the proposition indexed as “endpoint moduli coprime”; the hypotheses and conclusion in the code panel fix its exact scope.
theorem endpointModuli_coprime (k : ℕ) : IsCoprime (leftModulus k) (rightModulus k) := by
commit-pinned source · Verso Blueprint panel
This definition gives the library's named construction or computation for “interpolant”. The degree-bounded polynomial joining the jets of 'exp p' and 'exp (-p)'.
def interpolant (k : ℕ) : ℝ[X] :=
twoPointInterpolant (leftModulus k) (rightModulus k)
(jetPolynomial (-1) k (fun _ => Real.exp (-1)))
(jetPolynomial 0 k (fun j => (-1 : ℝ) ^ j))
/-- All derivatives through order `k` at `-1` equal `exp (-1)`. -/
commit-pinned source · Verso Blueprint panel
Lean checks the proposition indexed as “interpolant left jet”; the hypotheses and conclusion in the code panel fix its exact scope. All derivatives through order 'k' at '-1' equal 'exp (-1)'.
theorem interpolant_left_jet (k j : ℕ) (hj : j ≤ k) :
(derivative^[j] (interpolant k)).eval (-1) = Real.exp (-1) := by
commit-pinned source · Verso Blueprint panel
Lean checks the proposition indexed as “interpolant right jet”; the hypotheses and conclusion in the code panel fix its exact scope. All derivatives through order 'k' at '0' equal '(-1)^j'.
theorem interpolant_right_jet (k j : ℕ) (hj : j ≤ k) :
(derivative^[j] (interpolant k)).eval 0 = (-1 : ℝ) ^ j := by
commit-pinned source · Verso Blueprint panel
Lean checks the proposition indexed as “interpolant degree”; the hypotheses and conclusion in the code panel fix its exact scope. The construction has the minimal Hermite degree bound.
theorem interpolant_degree (k : ℕ) : (interpolant k).natDegree ≤ 2 * k + 1 := by
commit-pinned source · Verso Blueprint panel
This definition gives the library's named construction or computation for “coefficient series”. The generating series whose first 'k+1' coefficients are the source's 'a_{k,r}'.
def coefficientSeries (k : ℕ) : PowerSeries ℝ :=
PowerSeries.exp ℝ * (PowerSeries.invOneSubPow ℝ (k + 1)).val
/-- The exact polynomial `A_k`, implemented as a finite Taylor truncation. -/
commit-pinned source · Verso Blueprint panel
This definition gives the library's named construction or computation for “coefficient polynomial”. The exact polynomial 'A_k', implemented as a finite Taylor truncation.
def coefficientPolynomial (k : ℕ) : ℝ[X] :=
PowerSeries.trunc (k + 1) (coefficientSeries k)
/-- One endpoint cardinal factor in the symmetric closed-form Hermite formula. -/
commit-pinned source · Verso Blueprint panel
This definition gives the library's named construction or computation for “endpoint factor”. One endpoint cardinal factor in the symmetric closed-form Hermite formula.
def endpointFactor (k : ℕ) : ℝ[X] := (1 - X) ^ (k + 1) * coefficientPolynomial k
/-- The source closed form, in the coordinate `t = p + 1`. -/
commit-pinned source · Verso Blueprint panel
This definition gives the library's named construction or computation for “source interpolant”. The source closed form, in the coordinate 't = p + 1'.
def sourceInterpolant (k : ℕ) : ℝ[X] :=
taylor 1 (C (Real.exp (-1)) * endpointFactor k +
(endpointFactor k).comp (1 - X))
commit-pinned source · Verso Blueprint panel
Lean checks the proposition indexed as “coefficient series coeff”; the hypotheses and conclusion in the code panel fix its exact scope.
theorem coefficientSeries_coeff (k r : ℕ) :
PowerSeries.coeff r (coefficientSeries k) =
∑ m ∈ Finset.range (r + 1), (Nat.choose (k + r - m) k : ℝ) /
(m.factorial : ℝ) := by
commit-pinned source · Verso Blueprint panel
Lean checks the proposition indexed as “coefficient series coeff nonneg”; the hypotheses and conclusion in the code panel fix its exact scope.
theorem coefficientSeries_coeff_nonneg (k r : ℕ) :
0 ≤ PowerSeries.coeff r (coefficientSeries k) := by
commit-pinned source · Verso Blueprint panel
Lean checks the proposition indexed as “coefficient series coeff zero”; the hypotheses and conclusion in the code panel fix its exact scope.
@[simp] theorem coefficientSeries_coeff_zero (k : ℕ) :
PowerSeries.coeff 0 (coefficientSeries k) = 1 := by
commit-pinned source · Verso Blueprint panel
Lean checks the proposition indexed as “endpoint factor series trunc”; the hypotheses and conclusion in the code panel fix its exact scope.
theorem endpointFactor_series_trunc (k : ℕ) :
PowerSeries.trunc (k + 1) (endpointFactor k : PowerSeries ℝ) =
PowerSeries.trunc (k + 1) (PowerSeries.exp ℝ) := by
commit-pinned source · Verso Blueprint panel
Lean checks the proposition indexed as “endpoint factor coeff”; the hypotheses and conclusion in the code panel fix its exact scope.
theorem endpointFactor_coeff (k j : ℕ) (hj : j ≤ k) :
(endpointFactor k).coeff j = 1 / (j.factorial : ℝ) := by
commit-pinned source · Verso Blueprint panel
Lean checks the proposition indexed as “endpoint factor zero jet”; the hypotheses and conclusion in the code panel fix its exact scope.
theorem endpointFactor_zero_jet (k j : ℕ) (hj : j ≤ k) :
(derivative^[j] (endpointFactor k)).eval 0 = 1 := by
commit-pinned source · Verso Blueprint panel
Lean checks the proposition indexed as “endpoint factor one jet”; the hypotheses and conclusion in the code panel fix its exact scope.
theorem endpointFactor_one_jet (k j : ℕ) (hj : j ≤ k) :
(derivative^[j] (endpointFactor k)).eval 1 = 0 := by
commit-pinned source · Verso Blueprint panel
Lean checks the proposition indexed as “source interpolant left jet”; the hypotheses and conclusion in the code panel fix its exact scope.
theorem sourceInterpolant_left_jet (k j : ℕ) (hj : j ≤ k) :
(derivative^[j] (sourceInterpolant k)).eval (-1) = Real.exp (-1) := by
commit-pinned source · Verso Blueprint panel
Lean checks the proposition indexed as “source interpolant right jet”; the hypotheses and conclusion in the code panel fix its exact scope.
theorem sourceInterpolant_right_jet (k j : ℕ) (hj : j ≤ k) :
(derivative^[j] (sourceInterpolant k)).eval 0 = (-1 : ℝ) ^ j := by
commit-pinned source · Verso Blueprint panel
Lean checks the proposition indexed as “coefficient polynomial pos”; the hypotheses and conclusion in the code panel fix its exact scope.
theorem coefficientPolynomial_pos (k : ℕ) (t : ℝ) (ht : 0 ≤ t) :
0 < (coefficientPolynomial k).eval t := by
commit-pinned source · Verso Blueprint panel
Lean checks the proposition indexed as “source interpolant pos”; the hypotheses and conclusion in the code panel fix its exact scope.
theorem sourceInterpolant_pos (k : ℕ) (p : ℝ) (hp : p ∈ Set.Icc (-1) 0) :
0 < (sourceInterpolant k).eval p := by
commit-pinned source · Verso Blueprint panel
Lean checks the proposition indexed as “coefficient polynomial eval”; the hypotheses and conclusion in the code panel fix its exact scope. The coefficient polynomial is exactly the finite sum in the closed form.
theorem coefficientPolynomial_eval (k : ℕ) (t : ℝ) :
(coefficientPolynomial k).eval t =
∑ r ∈ Finset.range (k + 1),
(∑ m ∈ Finset.range (r + 1), (Nat.choose (k + r - m) k : ℝ) /
(m.factorial : ℝ)) * t ^ r := by
commit-pinned source · Verso Blueprint panel
Lean checks the proposition indexed as “source interpolant eval”; the hypotheses and conclusion in the code panel fix its exact scope. Source formula with the coordinate convention 't = p + 1' made explicit.
theorem sourceInterpolant_eval (k : ℕ) (p : ℝ) :
(sourceInterpolant k).eval p =
Real.exp (-1) * (1 - (p + 1)) ^ (k + 1) *
(coefficientPolynomial k).eval (p + 1) +
(p + 1) ^ (k + 1) * (coefficientPolynomial k).eval (1 - (p + 1)) := by
commit-pinned source · Verso Blueprint panel
Lean checks the proposition indexed as “coefficient polynomial degree”; the hypotheses and conclusion in the code panel fix its exact scope.
theorem coefficientPolynomial_degree (k : ℕ) : (coefficientPolynomial k).natDegree ≤ k :=
Nat.le_of_lt_succ (PowerSeries.natDegree_trunc_lt (coefficientSeries k) k)
commit-pinned source · Verso Blueprint panel
Lean checks the proposition indexed as “endpoint factor degree”; the hypotheses and conclusion in the code panel fix its exact scope.
theorem endpointFactor_degree (k : ℕ) : (endpointFactor k).natDegree ≤ 2 * k + 1 := by
commit-pinned source · Verso Blueprint panel
Lean checks the proposition indexed as “source interpolant degree”; the hypotheses and conclusion in the code panel fix its exact scope. The source closed form has degree at most '2k+1'.
theorem sourceInterpolant_degree (k : ℕ) : (sourceInterpolant k).natDegree ≤ 2 * k + 1 := by
commit-pinned source · Verso Blueprint panel
Lean checks the proposition indexed as “iterated deriv polynomial”; the hypotheses and conclusion in the code panel fix its exact scope. Algebraic and analytic repeated differentiation agree for real polynomials.
theorem iteratedDeriv_polynomial (p : ℝ[X]) (j : ℕ) (x : ℝ) :
iteratedDeriv j (fun y => p.eval y) x = (derivative^[j] p).eval x := by
commit-pinned source · Verso Blueprint panel
Lean checks the proposition indexed as “source interpolant left iterated deriv”; the hypotheses and conclusion in the code panel fix its exact scope.
theorem sourceInterpolant_left_iteratedDeriv (k j : ℕ) (hj : j ≤ k) :
iteratedDeriv j (fun p => (sourceInterpolant k).eval p) (-1) = Real.exp (-1) := by
commit-pinned source · Verso Blueprint panel
Lean checks the proposition indexed as “source interpolant right iterated deriv”; the hypotheses and conclusion in the code panel fix its exact scope.
theorem sourceInterpolant_right_iteratedDeriv (k j : ℕ) (hj : j ≤ k) :
iteratedDeriv j (fun p => (sourceInterpolant k).eval p) 0 = (-1 : ℝ) ^ j := by
commit-pinned source · Verso Blueprint panel
This definition gives the library's named construction or computation for “smooth initial”. The literal piecewise initial datum: left exponential, Hermite bridge, right exponential.
def smoothInitial (k : ℕ) (p : ℝ) : ℝ :=
if p < -1 then Real.exp p else
if p ≤ 0 then (sourceInterpolant k).eval p else Real.exp (-p)
commit-pinned source · Verso Blueprint panel
Lean checks the proposition indexed as “smooth initial left”; the hypotheses and conclusion in the code panel fix its exact scope.
theorem smoothInitial_left (k : ℕ) (p : ℝ) (hp : p < -1) :
smoothInitial k p = Real.exp p := by simp [smoothInitial, hp]
commit-pinned source · Verso Blueprint panel
Lean checks the proposition indexed as “smooth initial middle”; the hypotheses and conclusion in the code panel fix its exact scope.
theorem smoothInitial_middle (k : ℕ) (p : ℝ) (hp : p ∈ Set.Icc (-1) 0) :
smoothInitial k p = (sourceInterpolant k).eval p := by
commit-pinned source · Verso Blueprint panel
Lean checks the proposition indexed as “smooth initial right”; the hypotheses and conclusion in the code panel fix its exact scope.
theorem smoothInitial_right (k : ℕ) (p : ℝ) (hp : 0 < p) :
smoothInitial k p = Real.exp (-p) := by
commit-pinned source · Verso Blueprint panel
Lean checks the proposition indexed as “smooth initial pos”; the hypotheses and conclusion in the code panel fix its exact scope. Strict positivity holds globally and makes every finite sampled norm nonzero.
theorem smoothInitial_pos (k : ℕ) (p : ℝ) : 0 < smoothInitial k p := by
commit-pinned source · Verso Blueprint panel
Lean checks the proposition indexed as “pow dvd sub of jet eq”; the hypotheses and conclusion in the code panel fix its exact scope. Agreement of a finite jet is equivalent to divisibility by the endpoint multiplicity.
theorem pow_dvd_sub_of_jet_eq (p q : ℝ[X]) (a : ℝ) (k : ℕ)
(h : ∀ j ≤ k, (derivative^[j] p).eval a = (derivative^[j] q).eval a) :
(X - C a) ^ (k + 1) ∣ p - q := by
commit-pinned source · Verso Blueprint panel
Lean checks the proposition indexed as “source interpolant unique”; the hypotheses and conclusion in the code panel fix its exact scope. There is only one degree-bounded polynomial with the source endpoint jets.
theorem sourceInterpolant_unique (k : ℕ) (p : ℝ[X]) (hp : p.natDegree ≤ 2 * k + 1)
(hl : ∀ j ≤ k, (derivative^[j] p).eval (-1) = Real.exp (-1))
(hr : ∀ j ≤ k, (derivative^[j] p).eval 0 = (-1 : ℝ) ^ j) :
p = sourceInterpolant k := by
commit-pinned source · Verso Blueprint panel
Lean checks the proposition indexed as “interpolant eq source interpolant”; the hypotheses and conclusion in the code panel fix its exact scope. The Euclidean-algorithm construction and the positive source formula agree exactly.
theorem interpolant_eq_sourceInterpolant (k : ℕ) : interpolant k = sourceInterpolant k :=
sourceInterpolant_unique k (interpolant k) (interpolant_degree k)
(interpolant_left_jet k) (interpolant_right_jet k)
commit-pinned source · Verso Blueprint panel