6.5 Series kernels and finite-data certificates
Coefficient majorants bound both the kernel approximation error and the operator error. For the exponential kernel, these bounds give a residual certificate from finite data.
Reference details: Joint weights for kernel monomials and related results
For a monomial \(p(x,y)=cx^iy^j\), define
This weight is nonnegative for \(R,S\ge 0\) and bounds \(|p(x,y)|\) when \(|x|\le R\), \(|y|\le S\). If \(S\ge 1\), it also bounds \(|cx^i j y^{j-1}|\), with the derivative zero when \(j=0\). Its ordered operator is \(cH^iJ^j\). For \(R\ge \| H\| \), \(S\ge \| J\| \), its operator norm is at most \(w_{R,S}(i,j,c)\).
Lean Formalisation
theorem MvPolynomial.eval_volterraSeriesTerm (i j : ℕ) (c : ℝ) (z : Fin 2 → ℝ) :
(MvPolynomial.eval z) (MvPolynomial.volterraSeriesTerm i j c) = c * z 0 ^ i * z 1 ^ jLean proof
/-- Physical evaluation of a kernel-series monomial. -/
theorem eval_volterraSeriesTerm (i j : ℕ) (c : ℝ) (z : Fin 2 → ℝ) :
eval z (volterraSeriesTerm i j c) = c*z 0^i*z 1^j := by
have he : volterraSeriesTerm i j c = C c * X 0^i * X 1^j := by
simp [volterraSeriesTerm, X_pow_eq_monomial, C_mul_monomial, monomial_mul_monomial]
rw [he]
simpFor real \(R,S\), put \(B_{R,S}=\{ (x,y)\in \mathbb R^2:|x|\le R,\ |y|\le S\} \). This set is empty if either radius is negative.
Lean Formalisation
def MvPolynomial.volterraSeriesBox (R S : ℝ) : Set (Fin 2 → ℝ)Lean definition
def volterraSeriesBox (R S : ℝ) : Set (Fin 2 → ℝ) :=
{z | |z 0| ≤ R ∧ |z 1| ≤ S}Every \(B_{R,S}\) is closed.
Lean Formalisation
theorem MvPolynomial.isClosed_volterraSeriesBox (R S : ℝ) : IsClosed (MvPolynomial.volterraSeriesBox R S)Lean proof
theorem isClosed_volterraSeriesBox (R S : ℝ) : IsClosed (volterraSeriesBox R S) := by
exact (isClosed_le (show Continuous (fun z : Fin 2 → ℝ ↦ |z 0|) by fun_prop)
continuous_const).inter
(isClosed_le (show Continuous (fun z : Fin 2 → ℝ ↦ |z 1|) by fun_prop) continuous_const)Fix exponent sequences \(i_n,j_n\in \mathbb N\) and a point \(z=(x,y)\in \mathbb R^2\). A kernel-series input at \(z\) is a real coefficient sequence \(c_n\) for which \(\sum _n |c_nx^{i_n}y^{j_n}|{\lt}\infty \). Convergence is required at the selected point; no common rectangle is required to define the series at \(z\).
Lean Formalisation
def MvPolynomial.VolterraSeriesKernelInput (i j : ℕ → ℕ) (z : Fin 2 → ℝ) : TypeLean definition
def VolterraSeriesKernelInput (i j : ℕ → ℕ) (z : Fin 2 → ℝ) :=
{c : ℕ → ℝ // Summable (fun n ↦ c n * z 0 ^ i n * z 1 ^ j n)}If \(R,S\ge 0\) and \(\sum _n w_{R,S}(i_n,j_n,c_n){\lt}\infty \), the scalar series \(\sum _n c_n x^{i_n}y^{j_n}\) converges absolutely at every \((x,y)\in B_{R,S}\). If \(R,S\ge 1\), this convergence holds at every point of the physical triangle \(\Delta \).
Lean Formalisation
def MvPolynomial.VolterraSeriesKernelInput.ofWeight (i j : ℕ → ℕ) (c : ℕ → ℝ) {R S : ℝ} (hR : 0 ≤ R) (hS : 0 ≤ S)
(hw : Summable fun n => MvPolynomial.volterraSeriesWeight R S (i n) (j n) (c n))
(z : ↑(MvPolynomial.volterraSeriesBox R S)) : MvPolynomial.VolterraSeriesKernelInput i j ↑zLean definition
def VolterraSeriesKernelInput.ofWeight (i j : ℕ → ℕ) (c : ℕ → ℝ) {R S : ℝ}
(hR : 0 ≤ R) (hS : 0 ≤ S)
(hw : Summable (fun n ↦ volterraSeriesWeight R S (i n) (j n) (c n)))
(z : volterraSeriesBox R S) : VolterraSeriesKernelInput i j z :=
⟨c, hw.of_norm_bounded (fun n ↦ by
simpa only [eval_volterraSeriesTerm] using
norm_eval_volterraSeriesTerm_le hR hS (i n) (j n) (c n) z
z.property.1 z.property.2)⟩For a kernel-series input at \(z=(x,y)\), define \(K(z)=\sum _{n\ge 0}c_nx^{i_n}y^{j_n}\), the sum of its absolutely convergent series.
Lean Formalisation
def MvPolynomial.volterraSeriesKernel (i j : ℕ → ℕ) {z : Fin 2 → ℝ} (d : MvPolynomial.VolterraSeriesKernelInput i j z) : ℝLean definition
def volterraSeriesKernel (i j : ℕ → ℕ) {z : Fin 2 → ℝ} (d : VolterraSeriesKernelInput i j z) : ℝ :=
∑' n, d.val n * z 0 ^ i n * z 1 ^ j nAt every point \((x,y)\) where the monomial series is absolutely convergent, its kernel value is its sum:
Lean Formalisation
theorem MvPolynomial.hasSum_volterraSeriesKernel (i j : ℕ → ℕ) {z : Fin 2 → ℝ}
(d : MvPolynomial.VolterraSeriesKernelInput i j z) :
HasSum (fun n => ↑d n * z 0 ^ i n * z 1 ^ j n) (MvPolynomial.volterraSeriesKernel i j d)Lean proof
theorem hasSum_volterraSeriesKernel (i j : ℕ → ℕ) {z : Fin 2 → ℝ} (d : VolterraSeriesKernelInput i j z) :
HasSum (fun n ↦ d.val n * z 0 ^ i n * z 1 ^ j n) (volterraSeriesKernel i j d) :=
d.property.hasSumIf \(R,S\ge 0\) and the joint weights are summable, the function \(K:B_{R,S}\to \mathbb R\) is continuous.
Lean Formalisation
theorem MvPolynomial.continuous_volterraSeriesKernel_box (i j : ℕ → ℕ) (c : ℕ → ℝ) {R S : ℝ} (hR : 0 ≤ R) (hS : 0 ≤ S)
(hw : Summable fun n => MvPolynomial.volterraSeriesWeight R S (i n) (j n) (c n)) :
Continuous fun z =>
MvPolynomial.volterraSeriesKernel i j (MvPolynomial.VolterraSeriesKernelInput.ofWeight i j c hR hS hw z)Lean proof
theorem continuous_volterraSeriesKernel_box (i j : ℕ → ℕ) (c : ℕ → ℝ) {R S : ℝ}
(hR : 0 ≤ R) (hS : 0 ≤ S)
(hw : Summable (fun n ↦ volterraSeriesWeight R S (i n) (j n) (c n))) :
Continuous (fun z : volterraSeriesBox R S ↦ volterraSeriesKernel i j (VolterraSeriesKernelInput.ofWeight i j c hR hS hw z)) := by
simp only [volterraSeriesKernel, VolterraSeriesKernelInput.ofWeight]
refine continuous_tsum (fun n ↦ ?_) hw (fun n z ↦ ?_)
· have h0 : Continuous (fun z : volterraSeriesBox R S ↦ (z : Fin 2 → ℝ) 0) :=
(continuous_apply 0).comp continuous_subtype_val
have h1 : Continuous (fun z : volterraSeriesBox R S ↦ (z : Fin 2 → ℝ) 1) :=
(continuous_apply 1).comp continuous_subtype_val
exact ((h0.pow (i n)).const_mul (c n)).mul (h1.pow (j n))
· simpa only [eval_volterraSeriesTerm] using
norm_eval_volterraSeriesTerm_le hR hS (i n) (j n) (c n) z
z.property.1 z.property.2For nonnegative radii and a summable joint majorant, a kernel-series extension is a continuous function \(F:\mathbb R^2\to \mathbb R\) such that \(F(z)=K(z)\) for every \(z\in B_{R,S}\). Outside the rectangle, \(F\) is an extension and is not asserted to be a series value.
Lean Formalisation
def MvPolynomial.VolterraSeriesKernelExtension (i j : ℕ → ℕ) (c : ℕ → ℝ) {R S : ℝ} (hR : 0 ≤ R) (hS : 0 ≤ S)
(hw : Summable fun n => MvPolynomial.volterraSeriesWeight R S (i n) (j n) (c n)) : TypeLean definition
/-- A genuine continuous extension of the series on its closed convergence volterraSeriesBox. -/
def VolterraSeriesKernelExtension (i j : ℕ → ℕ) (c : ℕ → ℝ) {R S : ℝ}
(hR : 0 ≤ R) (hS : 0 ≤ S)
(hw : Summable (fun n ↦ volterraSeriesWeight R S (i n) (j n) (c n))) :=
{K : C((Fin 2 → ℝ), ℝ) // ∀ z : volterraSeriesBox R S,
K z = volterraSeriesKernel i j (VolterraSeriesKernelInput.ofWeight i j c hR hS hw z)}Every kernel series with nonnegative radii and a summable joint majorant admits a continuous extension to \(\mathbb R^2\) agreeing on \(B_{R,S}\).
Lean Formalisation
theorem MvPolynomial.nonempty_volterraSeriesKernelExtension (i j : ℕ → ℕ) (c : ℕ → ℝ) {R S : ℝ} (hR : 0 ≤ R) (hS : 0 ≤ S)
(hw : Summable fun n => MvPolynomial.volterraSeriesWeight R S (i n) (j n) (c n)) :
Nonempty (MvPolynomial.VolterraSeriesKernelExtension i j c hR hS hw)Lean proof
theorem nonempty_volterraSeriesKernelExtension (i j : ℕ → ℕ) (c : ℕ → ℝ) {R S : ℝ}
(hR : 0 ≤ R) (hS : 0 ≤ S)
(hw : Summable (fun n ↦ volterraSeriesWeight R S (i n) (j n) (c n))) :
Nonempty (VolterraSeriesKernelExtension i j c hR hS hw) := by
obtain ⟨K,hK⟩ := exists_continuous_volterraSeriesKernel_extension i j c hR hS hw
exact ⟨⟨K,hK⟩⟩For exponent sequences \(i_n,j_n\in \mathbb N\), an operator-series input is a real coefficient sequence \(c_n\) for which the ordered operator family \(A_{c_nx^{i_n}y^{j_n}}\) is unconditionally summable in the Banach space of bounded operators on real \(\ell ^2\).
Lean Formalisation
def MvPolynomial.VolterraSeriesOperatorInput (i j : ℕ → ℕ) : TypeLean definition
/-- Coefficients for which the ordered Volterra operator series converges. -/
def VolterraSeriesOperatorInput :=
{c : ℕ → ℝ // Summable (fun n ↦
volterraPreconditionedL2 (volterraSeriesTerm (i n) (j n) (c n)))}If \(R\ge \| H\| \), \(S\ge \| J\| \), and \((w_{R,S}(i_n,j_n,c_n))_{n\ge 0}\) is summable, then the ordered operator series \(\sum _n c_nH^{i_n}J^{j_n}\) is summable in the Banach space of bounded operators.
Lean Formalisation
def MvPolynomial.VolterraSeriesOperatorInput.ofWeight (i j : ℕ → ℕ) (c : ℕ → ℝ) {R S : ℝ}
(hw : Summable fun n => MvPolynomial.volterraSeriesWeight R S (i n) (j n) (c n))
(hRH : ‖Polynomial.reflectedJacobiOneZeroL2‖ ≤ R) (hSJ : ‖Polynomial.shiftedJacobiOneZeroL2‖ ≤ S) :
MvPolynomial.VolterraSeriesOperatorInput i jLean definition
/-- A summable joint coefficient majorant supplies a convergent operator input. -/
def VolterraSeriesOperatorInput.ofWeight {R S : ℝ}
(hw : Summable (fun n ↦ volterraSeriesWeight R S (i n) (j n) (c n)))
(hRH : ‖reflectedJacobiOneZeroL2‖ ≤ R) (hSJ : ‖shiftedJacobiOneZeroL2‖ ≤ S) :
VolterraSeriesOperatorInput i j :=
⟨c, hw.of_norm_bounded (fun n ↦
norm_volterraPreconditionedL2_seriesTerm_le hRH hSJ (i n) (j n) (c n))⟩For a convergent operator-series input, define the unconditional sum \(A=\sum _{n\ge 0}A_{c_nx^{i_n}y^{j_n}}\) in the space of bounded operators on real \(\ell ^2\).
Lean Formalisation
def MvPolynomial.volterraSeriesOperator (i j : ℕ → ℕ) (d : MvPolynomial.VolterraSeriesOperatorInput i j) :
↥(lp (fun x => ℝ) 2) →L[ℝ] ↥(lp (fun x => ℝ) 2)Lean definition
/-- The convergent ordered operator series associated to the kernel expansion. -/
def volterraSeriesOperator (d : VolterraSeriesOperatorInput i j) :
lp (fun _ : ℕ ↦ ℝ) 2 →L[ℝ] lp (fun _ : ℕ ↦ ℝ) 2 :=
∑' n, volterraPreconditionedL2 (volterraSeriesTerm (i n) (j n) (d.val n))On the domain where \(\sum _n c_nH^{i_n}J^{j_n}\) is unconditionally summable in the Banach space of bounded operators, the ordered Volterra series operator \(A\) is its sum:
Lean Formalisation
theorem MvPolynomial.hasSum_volterraSeriesOperator (i j : ℕ → ℕ) (d : MvPolynomial.VolterraSeriesOperatorInput i j) :
HasSum (fun n => (MvPolynomial.volterraSeriesTerm (i n) (j n) (↑d n)).volterraPreconditionedL2)
(MvPolynomial.volterraSeriesOperator i j d)Lean proof
/-- The ordered operator series has the specified classical sum. -/
theorem hasSum_volterraSeriesOperator (d : VolterraSeriesOperatorInput i j) :
HasSum (fun n ↦ volterraPreconditionedL2 (volterraSeriesTerm (i n) (j n) (d.val n)))
(volterraSeriesOperator i j d) :=
d.property.hasSumFor exponent sequences \(i_n,j_n\in \mathbb N\) and real radii \(R,S\), a Volterra tail input is a real coefficient sequence \(c_n\) for which the real family \(w_n=w_{R,S}(i_n,j_n,c_n)\) is absolutely summable. No positivity of the radii is needed to specify this convergence domain.
Lean Formalisation
def MvPolynomial.VolterraSeriesTailInput (i j : ℕ → ℕ) (R S : ℝ) : TypeLean definition
/-- Coefficients whose joint Volterra majorant is summable. -/
def VolterraSeriesTailInput (R S : ℝ) :=
{c : ℕ → ℝ // Summable (fun n ↦ volterraSeriesWeight R S (i n) (j n) (c n))}Let \(w_n=w_{R,S}(i_n,j_n,c_n)\) be the joint coefficient weights. If \((w_n)_{n\ge 0}\) is summable, then for every \(N\ge 0\) the shifted family \((w_{n+N})_{n\ge 0}\) is summable.
Lean Formalisation
theorem MvPolynomial.VolterraSeriesTailInput.summable_tail (i j : ℕ → ℕ) {R S : ℝ}
(d : MvPolynomial.VolterraSeriesTailInput i j R S) (N : ℕ) :
Summable fun n => MvPolynomial.volterraSeriesWeight R S (i (n + N)) (j (n + N)) (↑d (n + N))Lean proof
/-- The shared tail input has a summable tail at each finite cutoff. -/
theorem VolterraSeriesTailInput.summable_tail {R S : ℝ}
(d : VolterraSeriesTailInput i j R S) (N : ℕ) :
Summable (fun n ↦ volterraSeriesWeight R S (i (n+N)) (j (n+N)) (d.val (n+N))) :=
(summable_nat_add_iff N).mpr d.propertyFor a Volterra tail input, define the convergent coefficient tail by \(E_N=\sum _{n\ge 0}w_{n+N}\).
Lean Formalisation
def MvPolynomial.volterraSeriesTail (i j : ℕ → ℕ) {R S : ℝ} (d : MvPolynomial.VolterraSeriesTailInput i j R S) (N : ℕ) : ℝLean definition
/-- A convergent coefficient majorant tail shared by physical and operator errors. -/
def volterraSeriesTail {R S : ℝ} (d : VolterraSeriesTailInput i j R S) (N : ℕ) : ℝ :=
∑' n, volterraSeriesWeight R S (i (n+N)) (j (n+N)) (d.val (n+N))The shifted family \((w_{n+N})_{n\ge 0}\) has sum \(E_N\), and \(E_N\to 0\). If \(R,S\ge 1\), then \(E_N\ge 0\) for every \(N\).
Lean Formalisation
theorem MvPolynomial.hasSum_volterraSeriesTail (i j : ℕ → ℕ) {R S : ℝ} (d : MvPolynomial.VolterraSeriesTailInput i j R S)
(N : ℕ) :
HasSum (fun n => MvPolynomial.volterraSeriesWeight R S (i (n + N)) (j (n + N)) (↑d (n + N)))
(MvPolynomial.volterraSeriesTail i j d N)Lean proof
/-- The coefficient tail is the sum of its defining convergent series. -/
theorem hasSum_volterraSeriesTail {R S : ℝ} (d : VolterraSeriesTailInput i j R S) (N : ℕ) :
HasSum (fun n ↦ volterraSeriesWeight R S (i (n+N)) (j (n+N)) (d.val (n+N)))
(volterraSeriesTail i j d N) :=
(VolterraSeriesTailInput.summable_tail i j d N).hasSumLet \(i_n,j_n\in \mathbb N\), \(c_n\in \mathbb R\), and assume \(R,S\ge 1\) and \(\sum _nw_n{\lt}\infty \), where \(w_n=w_{R,S}(i_n,j_n,c_n)\). Put \(p_n(x,y)=c_nx^{i_n}y^{j_n}\) and \(P_N=\sum _{n{\lt}N}p_n\). On \(B_{R,S}\) use the classical kernel sum \(K\) from Definition 6.5.6. For the coefficient tail \(E_N\) from Definition 6.5.17, we have \(E_N\ge 0\), \(E_N\to 0\), and \(K\) is continuous on \(\Delta \), with \(|P_N-K|\le E_N\) uniformly there. If additionally \(R\ge \| H\| \), \(S\ge \| J\| \), the operator-series input is convergent. Writing \(A=\sum _n A_{p_n}\), we have \(\| A_{P_N}-A\| \le E_N\) and \(A_{P_N}\to A\) in operator norm. The enumeration is arbitrary; a bivariate power series is obtained by enumerating its exponent pairs. No injectivity of the enumeration is needed.
Lean Formalisation
theorem MvPolynomial.norm_volterraSeriesPartial_sub_kernel_le (i j : ℕ → ℕ) (c : ℕ → ℝ) {R S : ℝ} (hR : 1 ≤ R) (hS : 1 ≤ S)
(hw : Summable fun n => MvPolynomial.volterraSeriesWeight R S (i n) (j n) (c n)) (N : ℕ)
(z : ↑Real.volterraTriangle) :
‖(MvPolynomial.eval ↑z) (MvPolynomial.volterraSeriesPartial i j c N) -
MvPolynomial.volterraSeriesKernel i j (MvPolynomial.VolterraSeriesKernelInput.ofTriangle i j c hR hS hw z)‖ ≤
MvPolynomial.volterraSeriesTail i j ⟨c, hw⟩ NLean proof
/-- Uniform physical truncation error is bounded by the coefficient tail. -/
theorem norm_volterraSeriesPartial_sub_kernel_le (N : ℕ)
(z : Real.volterraTriangle) :
‖eval (z : Fin 2 → ℝ) (volterraSeriesPartial i j c N) -
volterraSeriesKernel i j (VolterraSeriesKernelInput.ofTriangle i j c hR hS hw z)‖ ≤
volterraSeriesTail i j ⟨c, hw⟩ N := by
have hz := z.property
have hb (n : ℕ) : ‖eval (z : Fin 2 → ℝ) (volterraSeriesTerm (i n) (j n) (c n))‖ ≤
volterraSeriesWeight R S (i n) (j n) (c n) :=
norm_eval_volterraSeriesTerm_le (zero_le_one.trans hR) (zero_le_one.trans hS) _ _ _ _
(by rw [abs_of_nonneg hz.1.1]; exact hz.1.2.trans hR)
(by rw [abs_of_nonneg hz.2.1]; exact (hz.2.2.trans hz.1.2).trans hS)
simpa only [volterraSeriesPartial, map_sum, eval_volterraSeriesTerm, volterraSeriesKernel,
VolterraSeriesKernelInput.ofTriangle, VolterraSeriesKernelInput.ofWeight,
volterraSeriesTail] using series_tail_bound _ hw hb NUnder the preceding summability condition, assume \(R\ge 1\) and \(S{\gt}1\). For \(|x|\le R\), \(|y|{\lt}S\), the kernel is differentiable in its inner variable and
The summand is zero when \(j_n=0\); when \(j_n{\gt}0\), its exponent is nonnegative. On \(\Delta \), \(|\partial _yK|\le W:=\sum _n w_n\) and every slice on \([0,x]\) is absolutely continuous. These local derivative and row statements hold for every continuous extension agreeing on \(B_{R,S}\); the derivative of the domain-valued kernel is independent of the chosen extension. If \(K(x,x)\ne 0\) throughout \([0,1]\), there exists \(C\in \mathbb R\) such that \(|\partial _yK(x,y)|\le C|K(x,x)|\) on \(\Delta \).
Lean Formalisation
theorem MvPolynomial.hasDerivAt_volterraSeriesKernel (i j : ℕ → ℕ) (c : ℕ → ℝ) {R S : ℝ} (hR : 1 ≤ R) (hS : 1 < S)
(hw : Summable fun n => MvPolynomial.volterraSeriesWeight R S (i n) (j n) (c n)) (x : { x // |x| ≤ R })
(y : ↑(Set.Ioo (-S) S)) :
HasDerivAtOnOpen { carrier := Set.Ioo (-S) S, is_open' := ⋯ }
(fun t =>
MvPolynomial.volterraSeriesKernel i j
(MvPolynomial.VolterraSeriesKernelInput.ofWeight i j c ⋯ ⋯ hw ⟨![↑x, ↑t], ⋯⟩))
(∑' (n : ℕ), c n * ↑x ^ i n * (↑(j n) * ↑y ^ (j n - 1))) yLean proof
/-- The series derivative exists intrinsically on its open inner domain. -/
theorem hasDerivAt_volterraSeriesKernel (x : {x : ℝ // |x| ≤ R}) (y : Ioo (-S) S) :
HasDerivAtOnOpen ⟨Ioo (-S) S, isOpen_Ioo⟩
(fun t ↦ volterraSeriesKernel i j (VolterraSeriesKernelInput.ofWeight i j c
(zero_le_one.trans hR) (zero_le_one.trans hS.le) hw
⟨![(x : ℝ),(t : ℝ)], x.property, abs_le.mpr ⟨t.property.1.le,t.property.2.le⟩⟩))
(∑' n, c n*(x : ℝ)^(i n)*((j n : ℝ)*(y : ℝ)^(j n-1))) y := by
obtain ⟨F⟩ := nonempty_volterraSeriesKernelExtension i j c
(zero_le_one.trans hR) (zero_le_one.trans hS.le) hw
refine ⟨fun t ↦ F.val ![(x : ℝ),t], ?_,
hasDerivAt_volterraSeriesKernel_extension i j c hR hS hw F x.property
(abs_lt.mpr y.property)⟩
intro t
exact F.property ⟨![(x : ℝ),(t : ℝ)], x.property,
abs_le.mpr ⟨t.property.1.le,t.property.2.le⟩⟩Suppose \(R\ge \max (1,\| H\| )\), \(S{\gt}1\), \(S\ge \| J\| \), \(\sum _nw_n{\lt}\infty \), and \(K(x,x)\ne 0\) on \([0,1]\). Then \(A\) is invertible and its padded leading sections \(S_N(A)=I-P_N^{\ell ^2}+P_N^{\ell ^2}AP_N^{\ell ^2}\) have a uniform eventual inverse bound. For raw data \(g_N\to g\),
Here the kernel truncation \(P_N\) and coordinate projection \(P_N^{\ell ^2}\) are different objects. More generally, at any invertible section \(B=S_N(A_{P_L})\), for arbitrary \(u,g\in \ell ^2\),
The error estimate itself only requires the summability, operator-radius bounds and invertibility of that section.
Lean Formalisation
theorem MvPolynomial.isUnit_and_stable_volterraSeriesOperator (i j : ℕ → ℕ) (c : ℕ → ℝ) {R S : ℝ} (hR : 1 ≤ R) (hS : 1 < S)
(hRH : ‖Polynomial.reflectedJacobiOneZeroL2‖ ≤ R) (hSJ : ‖Polynomial.shiftedJacobiOneZeroL2‖ ≤ S)
(hw : Summable fun n => MvPolynomial.volterraSeriesWeight R S (i n) (j n) (c n))
(hd :
∀ (x : ↑(Set.Icc 0 1)),
MvPolynomial.volterraSeriesKernel i j
(MvPolynomial.VolterraSeriesKernelInput.ofTriangle i j c hR ⋯ hw ⟨![↑x, ↑x], ⋯⟩) ≠
0) :
IsUnit
(MvPolynomial.volterraSeriesOperator i j (MvPolynomial.VolterraSeriesOperatorInput.ofWeight i j c hw hRH hSJ)) ∧
∃ B,
0 ≤ B ∧
∀ᶠ (N : ℕ) in Filter.atTop,
IsUnit
((lp.initialL2Projection N).coerciveFiniteSection
(MvPolynomial.volterraSeriesOperator i j
(MvPolynomial.VolterraSeriesOperatorInput.ofWeight i j c hw hRH hSJ))) ∧
‖Ring.inverse
((lp.initialL2Projection N).coerciveFiniteSection
(MvPolynomial.volterraSeriesOperator i j
(MvPolynomial.VolterraSeriesOperatorInput.ofWeight i j c hw hRH hSJ)))‖ ≤
BLean proof
/-- The joint coefficient criterion and a nonzero diagonal imply invertibility and stable sections. -/
theorem isUnit_and_stable_volterraSeriesOperator :
IsUnit (volterraSeriesOperator i j (VolterraSeriesOperatorInput.ofWeight i j c hw hRH hSJ)) ∧ ∃ B : ℝ, 0 ≤ B ∧ ∀ᶠ N in atTop,
IsUnit (coerciveFiniteSection (lp.initialL2Projection N) (volterraSeriesOperator i j (VolterraSeriesOperatorInput.ofWeight i j c hw hRH hSJ))) ∧
‖Ring.inverse (coerciveFiniteSection (lp.initialL2Projection N)
(volterraSeriesOperator i j (VolterraSeriesOperatorInput.ofWeight i j c hw hRH hSJ)))‖ ≤ B := by
obtain ⟨E⟩ := nonempty_volterraSeriesKernelExtension i j c
(zero_le_one.trans hR) (zero_le_one.trans hS.le) hw
have hdE (x : Icc (0 : ℝ) 1) : E.val ![(x : ℝ),(x : ℝ)] ≠ 0 := by
rw [extension_eq_triangle i j c hR hS hw E
⟨![(x : ℝ),(x : ℝ)], x.property, x.property.1, le_rfl⟩]
exact hd x
obtain ⟨C,hC⟩ := exists_volterraSeriesKernel_relative_derivative_bound i j c hR hS hw E hdE
have herr (N : ℕ) (z : Fin 2 → ℝ) (hz : z ∈ Real.volterraTriangle) :
‖eval z (volterraSeriesPartial i j c N) - E.val z‖ ≤
volterraSeriesTail i j ⟨c,hw⟩ N := by
rw [extension_eq_triangle i j c hR hS hw E ⟨z,hz⟩]
exact norm_volterraSeriesPartial_sub_kernel_le i j c hR hS.le hw N ⟨z,hz⟩
exact Real.isUnit_and_stable_continuousVolterra
E.val.continuous.continuousOn
(fun x hx ↦ absolutelyContinuousOnInterval_volterraSeriesKernel i j c hR hS hw E ⟨x,hx⟩)
(fun x hx ↦ by
obtain ⟨g⟩ := IntegrableDerivative.nonempty_of_absolutelyContinuous
(absolutelyContinuousOnInterval_volterraSeriesKernel i j c hR hS hw E ⟨x,hx⟩)
refine ⟨g, ?_⟩
filter_upwards [g.hasDerivAt, MeasureTheory.ae_restrict_mem measurableSet_uIcc] with y hy hmem
rw [← hy.deriv]
exact hC ⟨x,hx⟩ ⟨y,by simpa only [uIcc_of_le hx.1] using hmem⟩) (fun x hx ↦ hdE ⟨x,hx⟩)
(volterraSeriesPartial i j c) (volterraSeriesTail_nonneg i j c hR hS.le hw)
herr
(tendsto_volterraSeriesTail i j c hw) _ (tendsto_volterraSeriesPartial_operator i j c hw hRH hSJ)The inverse norm and solution tail remain explicit; no numerical certificate for them is asserted.
Reference details: The exponential kernel satisfies the coefficient criterion
For any real \(\lambda \), enumerate \((i_n,j_n)=\operatorname {unpair}(n)\) and set
The series \(\sum _n c_n x^{i_n}y^{j_n}\) converges absolutely for every \((x,y)\in \mathbb {R}^2\). The classical kernel value equals \(e^{\lambda (x-y)}\) for all real \(x,y\). For every \(R,S\ge 0\), its joint weights are summable. The pairing enumerates all exponent pairs.
Lean Formalisation
theorem MvPolynomial.summable_volterraExponentialWeight (lam : ℝ) {R S : ℝ} (hR : 0 ≤ R) (hS : 0 ≤ S) :
Summable fun n =>
MvPolynomial.volterraSeriesWeight R S (Nat.unpair n).1 (Nat.unpair n).2
(MvPolynomial.volterraExponentialCoefficient lam n)Lean proof
/-- The exponential coefficient weights are summable for arbitrary nonnegative radii. -/
theorem summable_volterraExponentialWeight (lam : ℝ) {R S : ℝ} (hR : 0 ≤ R) (hS : 0 ≤ S) :
Summable (fun n ↦ volterraSeriesWeight R S (Nat.unpair n).1 (Nat.unpair n).2
(volterraExponentialCoefficient lam n)) := by
have hs := (Real.summable_pow_div_factorial (|lam| *R)).mul_of_nonneg
(Real.summable_pow_div_factorial (2*|lam| *S)) (fun n ↦ by positivity) (fun n ↦ by positivity)
have hp : Summable (fun n ↦ ((|lam| *R)^(Nat.unpair n).1 / ((Nat.unpair n).1.factorial : ℝ))*
((2*|lam| *S)^(Nat.unpair n).2 / ((Nat.unpair n).2.factorial : ℝ))) :=
by simpa only [Function.comp_def,Nat.pairEquiv_symm_apply] using
(Nat.pairEquiv.symm.summable_iff.mpr hs)
apply hp.of_nonneg_of_le
(fun n ↦ volterraSeriesWeight_nonneg hR hS _ _ _) (fun n ↦ ?_)
have hn : ((Nat.unpair n).2 : ℝ)+1 ≤ (2 : ℝ)^(Nat.unpair n).2 := by
exact_mod_cast Nat.succ_le_of_lt (Nat.lt_two_pow_self (n := (Nat.unpair n).2))
have hcast (k : ℕ) : |(k : ℝ)| = (k : ℝ) := abs_of_nonneg (Nat.cast_nonneg k)
have hc : volterraSeriesWeight R S (Nat.unpair n).1 (Nat.unpair n).2
(volterraExponentialCoefficient lam n) =
((|lam| *R)^(Nat.unpair n).1 / ((Nat.unpair n).1.factorial : ℝ))*
((|lam| *S)^(Nat.unpair n).2 / ((Nat.unpair n).2.factorial : ℝ))*((Nat.unpair n).2+1) := by
simp only [volterraSeriesWeight,volterraExponentialCoefficient,abs_div,abs_mul,
abs_pow,abs_neg,hcast,mul_pow]
ring
rw [hc]
have hb := mul_le_mul_of_nonneg_left hn
(show 0 ≤ ((|lam| *R)^(Nat.unpair n).1 / ((Nat.unpair n).1.factorial : ℝ))*
((|lam| *S)^(Nat.unpair n).2 / ((Nat.unpair n).2.factorial : ℝ)) by positivity)
convert hb using 1
simp only [mul_pow]
ringLet \(K_\lambda (x,y)=e^{\lambda (x-y)}\), for any \(\lambda \in \mathbb R\), and let \(P_N\) be its paired polynomial series truncations and \(A_\lambda \) the ordered operator series. The physical bound is \(|K_\lambda |\le e^{|\lambda |}\) on \(\Delta \); its truncation error is bounded by the coefficient tail for every \(R,S\ge 1\). The diagonal is identically one. The operator \(A_\lambda \) is invertible, its leading sections have a uniform eventual inverse bound, and for \(g_N\to g\) in raw \(\ell ^2\),
The exact integral realization satisfies \(SD A_\lambda =B_{K_\lambda }S\). Consequently, the limiting coefficient solution satisfies the genuine weighted integral equation
Reflection and endpoint averaging are those of \(B_K\), and \(S\) is synthesis from raw coefficients.
Lean Formalisation
theorem MvPolynomial.norm_volterraExponentialPartial_sub_le (lam : ℝ) {R S : ℝ} (hR : 1 ≤ R) (hS : 1 ≤ S) (N : ℕ)
(z : Fin 2 → ℝ) (hz : z ∈ Real.volterraTriangle) :
‖(MvPolynomial.eval z) (MvPolynomial.volterraExponentialPartial lam N) - Real.exp (lam * (z 0 - z 1))‖ ≤
MvPolynomial.volterraSeriesTail (fun n => (Nat.unpair n).1) (fun n => (Nat.unpair n).2)
⟨MvPolynomial.volterraExponentialCoefficient lam, ⋯⟩ NLean proof
/-- Explicit coefficient-tail control of the physical exponential-kernel approximation. -/
theorem norm_volterraExponentialPartial_sub_le (lam : ℝ) {R S : ℝ}
(hR : 1 ≤ R) (hS : 1 ≤ S) (N : ℕ) (z : Fin 2 → ℝ) (hz : z ∈ Real.volterraTriangle) :
‖eval z (volterraExponentialPartial lam N)-Real.exp (lam*(z 0-z 1))‖ ≤
volterraSeriesTail a b ⟨volterraExponentialCoefficient lam,
summable_volterraExponentialWeight lam (zero_le_one.trans hR) (zero_le_one.trans hS)⟩ N := by
have h := norm_volterraSeriesPartial_sub_kernel_le a b (volterraExponentialCoefficient lam) hR hS
(summable_volterraExponentialWeight lam (zero_le_one.trans hR) (zero_le_one.trans hS)) N ⟨z,hz⟩
have he := volterraSeriesKernel_exponential lam z
simp only [volterraSeriesKernel, VolterraSeriesKernelInput.ofTriangle,
VolterraSeriesKernelInput.ofExponential, VolterraSeriesKernelInput.ofWeight] at h he
simpa only [volterraExponentialPartial, he] using hFor every real \(\lambda \), the raw coefficient operator factors in the stated order:
No commutation of \(H\) and \(J\) is assumed. In particular, with \(C_\lambda =\exp (|\lambda |(\| H\| +\| J\| ))\),
Lean Formalisation
theorem MvPolynomial.volterraExponentialOperator_eq (lam : ℝ) :
MvPolynomial.volterraExponentialOperator lam =
NormedSpace.exp (lam • Polynomial.reflectedJacobiOneZeroL2) *
NormedSpace.exp (-lam • Polynomial.shiftedJacobiOneZeroL2)Lean proof
/-- The exponential kernel gives an ordered product of operator exponentials. -/
theorem volterraExponentialOperator_eq (lam : ℝ) :
volterraExponentialOperator lam =
NormedSpace.exp (lam • H) * NormedSpace.exp ((-lam) • J) := by
have hp (x : ℝ) (A : E →L[ℝ] E) (n : ℕ) : (x • A)^n = x^n • A^n := by
induction n with
| zero => simp
| succ n ih =>
rw [pow_succ,ih,pow_succ,pow_succ]
apply ContinuousLinearMap.ext
intro v
simp only [mul_apply_eq_comp,smul_apply,
map_smul,smul_smul,mul_comm]
have hm (x y : ℝ) (A B : E →L[ℝ] E) :
(x • A)*(y • B) = (x*y) • (A*B) := by
apply ContinuousLinearMap.ext
intro v
simp only [mul_apply_eq_comp,smul_apply,
map_smul,smul_smul,mul_comm]
unfold volterraExponentialOperator volterraSeriesOperator VolterraSeriesOperatorInput.ofWeight
simp_rw [volterraPreconditionedL2_seriesTerm]
have he (n : ℕ) : volterraExponentialCoefficient lam n •
(H^(Nat.unpair n).1 * J^(Nat.unpair n).2) =
(((Nat.unpair n).1.factorial : ℝ)⁻¹ • (lam • H)^(Nat.unpair n).1) *
(((Nat.unpair n).2.factorial : ℝ)⁻¹ • ((-lam) • J)^(Nat.unpair n).2) := by
simp only [volterraExponentialCoefficient,hp,hm,smul_smul,div_eq_mul_inv]
congr 1
ring
simp_rw [he]
have hr := Nat.pairEquiv.symm.tsum_eq (fun k : ℕ × ℕ ↦
((k.1.factorial : ℝ)⁻¹ • (lam • H)^k.1) *
((k.2.factorial : ℝ)⁻¹ • ((-lam) • J)^k.2))
simp only [Nat.pairEquiv_symm_apply] at hr
rw [hr, ← tsum_mul_tsum_of_summable_norm
(NormedSpace.norm_expSeries_summable' (𝕂 := ℝ) (lam • H))
(NormedSpace.norm_expSeries_summable' (𝕂 := ℝ) ((-lam) • J))]
rw [NormedSpace.exp_eq_tsum ℝ]This is a bound for the full inverse; it does not assert the same constant for finite-section inverses.
For \(R,S\ge 0\), the total joint coefficient weight of the exponential series satisfies
For \(0{\lt}q\le 1\) and natural numbers \(m,N\) with \(m^2\le N\), its tail satisfies
Consequently, on the physical triangle,
For \(R\ge \| H\| \), \(S\ge \| J\| \), the raw operator error satisfies
For fixed \(q{\lt}1\) these are geometric bounds in \(m\); \(N\) is the number of paired terms, not a total-degree cutoff. Choosing \(q=1/2\) gives entirely explicit bounds without an infinite tail sum.
Lean Formalisation
theorem MvPolynomial.tsum_volterraExponentialWeight_le (lam : ℝ) {R S : ℝ} (hR : 0 ≤ R) (hS : 0 ≤ S) :
∑' (n : ℕ),
MvPolynomial.volterraSeriesWeight R S ((fun n => (Nat.unpair n).1) n) ((fun n => (Nat.unpair n).2) n)
(MvPolynomial.volterraExponentialCoefficient lam n) ≤
Real.exp (|lam| * R + 2 * |lam| * S)Lean proof
/-- A closed-form bound for the total joint coefficient majorant. -/
theorem tsum_volterraExponentialWeight_le (lam : ℝ) {R S : ℝ} (hR : 0 ≤ R) (hS : 0 ≤ S) :
(∑' n, volterraSeriesWeight R S (a n) (b n) (volterraExponentialCoefficient lam n)) ≤
Real.exp (|lam| *R+2*|lam| *S) := by
let f (k : ℕ × ℕ) := ((|lam| *R)^k.1/(k.1.factorial : ℝ))*
((2*|lam| *S)^k.2/(k.2.factorial : ℝ))
have hs := (Real.summable_pow_div_factorial (|lam| *R)).mul_of_nonneg
(Real.summable_pow_div_factorial (2*|lam| *S)) (fun n ↦ by positivity) (fun n ↦ by positivity)
have hp : Summable (fun n ↦ f (Nat.unpair n)) := by
simpa only [Function.comp_def,Nat.pairEquiv_symm_apply] using
(Nat.pairEquiv.symm.summable_iff.mpr hs)
apply (Summable.tsum_le_tsum (weight_bound lam hR hS)
(summable_volterraExponentialWeight lam hR hS) hp).trans_eq
have hr := Nat.pairEquiv.symm.tsum_eq f
simp only [Nat.pairEquiv_symm_apply] at hr
rw [hr]
have hnorm (x : ℝ) : Summable (fun n : ℕ ↦ ‖x^n/(n.factorial : ℝ)‖) := by
simpa only [norm_div,norm_pow,Real.norm_natCast] using Real.summable_pow_div_factorial ‖x‖
rw [show f = (fun k : ℕ × ℕ ↦ ((|lam| *R)^k.1/(k.1.factorial : ℝ))*
((2*|lam| *S)^k.2/(k.2.factorial : ℝ))) from rfl,
← tsum_mul_tsum_of_summable_norm (hnorm _) (hnorm _)]
have he (x : ℝ) : (∑' n : ℕ, x^n/(n.factorial : ℝ)) = Real.exp x := by
rw [Real.exp_eq_exp_ℝ,NormedSpace.exp_eq_tsum_div]
rw [he,he,Real.exp_add]Reference details: Numerical bounds for the raw Jacobi factors and related results
For the constant tridiagonal part \(T\), raw shifted Jacobi multiplication \(J\), and reflected preconditioned factor \(H\),
Lean Formalisation
theorem Polynomial.norm_shiftedJacobiToeplitzPart_le : ‖Polynomial.shiftedJacobiToeplitzPart‖ ≤ 1Lean proof
/-- The common constant tridiagonal part has norm at most one. -/
theorem norm_shiftedJacobiToeplitzPart_le : ‖shiftedJacobiToeplitzPart‖ ≤ 1 := by
have h := norm_add_le ((1/2 : ℝ) • (1 : E →L[ℝ] E)) ((1/4 : ℝ) • (F+B))
have hsum := (norm_add_le F B).trans (add_le_add forward_bound backward_bound)
have hid : ‖(1 : E →L[ℝ] E)‖ ≤ 1 := ContinuousLinearMap.norm_id_le
simp only [norm_smul,Real.norm_eq_abs] at h
norm_num only at h
unfold shiftedJacobiToeplitzPart
nlinarithThese are conservative bounds in the raw coefficient \(\ell ^2\) norm.
Let \(K\) be a polynomial kernel of total degree \(d_K\) (zero for the zero kernel), and let \(c,d\) be finite raw coefficient vectors supported below \(N,M\), respectively. Write \(b_i=(\mathcal V_Kc)_i\) for the Proriol assembled coefficients before the endpoint factor. The raw preconditioned action is
It vanishes for \(i\ge N+d_K\). Thus the residual \(r=d-A_Kc\) vanishes for \(i\ge Q:=\max (M,N+d_K)\), and its full norm is exactly
For input \(v\in \mathbb {R}^N\), each of the first \(N+d_K\) raw output rows is the corresponding row of the rectangular Proriol section multiplied by \((-1)^i(i+1)\). The residual sum includes rows beyond the retained square system; those rows cannot generally be discarded.
Lean Formalisation
theorem lp.norm_finsuppL2_eq_sqrt_sum (c : ℕ →₀ ℝ) (N : ℕ) (hc : ∀ n ∈ c.support, n < N) :
‖lp.finsuppL2 c‖ = √(∑ n ∈ Finset.range N, c n ^ 2)Lean proof
/-- A finitely supported raw coefficient norm is an ordinary finite Euclidean norm. -/
theorem norm_finsuppL2_eq_sqrt_sum (c : ℕ →₀ ℝ) (N : ℕ)
(hc : ∀ n ∈ c.support, n < N) :
‖finsuppL2 c‖ = Real.sqrt (∑ n ∈ Finset.range N, (c n)^2) := by
apply norm_eq_finite_sum
intro n hn
exact Finsupp.notMem_support_iff.mp (fun h ↦ (Nat.not_lt_of_ge hn) (hc n h))For every real \(\lambda \),
For any raw vectors \(g,d,v\), bounded operator \(B\), and error bounds \(\| g-d\| \le \delta \), \(\| B-A_\lambda \| \le \varepsilon \),
In particular, for the paired kernel truncation \(P_L\), \(0{\lt}q\le 1\), and \(m^2\le L\), one may take
For finite input coefficients \(c\) supported below \(N\) and finite data \(d\) supported below \(M\), put \(Q=\max (M,N+\operatorname {totalDegree}P_L)\) and \(b_i=(\mathcal V_{P_L}c)_i\). Given \(\| g-d\| \le \delta \), the certificate is
Finite vectors are embedded by zero extension. The candidate need not satisfy its retained equations exactly.
Lean Formalisation
theorem MvPolynomial.norm_inverse_volterraExponentialOperator_le_numeric (lam : ℝ) :
‖Ring.inverse (MvPolynomial.volterraExponentialOperator lam)‖ ≤ Real.exp (5 * |lam|)Lean proof
/-- A numerical full-inverse bound, valid for every real exponential parameter. -/
theorem norm_inverse_volterraExponentialOperator_le_numeric (lam : ℝ) :
‖Ring.inverse (volterraExponentialOperator lam)‖ ≤ Real.exp (5*|lam|) := by
apply (norm_inverse_volterraExponentialOperator_le lam).trans
apply Real.exp_le_exp.mpr
have h := add_le_add norm_reflectedJacobiOneZeroL2_le norm_shiftedJacobiOneZeroL2_le
nlinarith [abs_nonneg lam]The data-tail bound is supplied explicitly; no finite-section inverse bound or floating-point rounding model is assumed.
Volterra operators through the triangle: see Theorems 6.1.15, 6.1.24, 6.1.30, 6.1.36, 6.1.38, 6.1.44, 6.1.54, 6.4.3, 6.4.4, 6.4.24, 6.4.30, 6.4.32, 6.5.21, 6.5.23, 6.5.24, 6.5.25 and 6.5.28.