LeanFun RevOLVER

6.1 Volterra operators and second-kind equations

Proriol polynomials on the triangle represent Volterra kernels. We first compute their action on coefficients, then construct operators on function spaces and prove convergence of finite solves. The coordinate spaces and assumptions are stated in each solve theorem.

Let \(D_{n,k}\) denote our DLMF-normalized unweighted Proriol polynomial on \(0{\lt}y{\lt}x{\lt}1\), and put \(Q_{n,k}(x,y)=(-1)^{n-k}D_{n,k}(1-x,y)\). This is precisely the normalization of [GO20] on \(0{\lt}y{\lt}1-x\):

\[ Q_{n,k}(x,(1-x)z)=\widetilde P_{n-k}^{(2k+1,0)}(x) (1-x)^k\widetilde P_k^{(0,0)}(z). \]

The linear marginal \(I_yf(x)=\int _0^{1-x}f(x,y)\, dy\) satisfies

\[ I_yQ_{n,k}(x)= \begin{cases} (1-x)\widetilde P_n^{(1,0)}(x),& k=0,\\ 0,& k{\gt}0.\end{cases} \]

Consequently, for every finite expansion,

\[ I_y\! \left(\sum _{n{\lt}N}\sum _{k=0}^n c_{n,k}Q_{n,k}\right)(x) =(1-x)\sum _{n{\lt}N}c_{n,0}\widetilde P_n^{(1,0)}(x). \]

The endpoint factor remains explicit; these identities include \(x=1\) and hold for all real \(x\) with oriented interval integrals.

References: [GO20, Section 3.1]; [Gut22, Section 2.3].

Lean Formalisation
theorem Polynomial.eval_shiftedJacobi_one_sub (α β x : ℝ) (n : ℕ) :
  Polynomial.eval (1 - x) (Polynomial.shiftedJacobi α β n) =
    (-1) ^ n * Polynomial.eval x (Polynomial.shiftedJacobi β α n)
Lean proof
/-- Shifted Jacobi reflection, with the parameter swap (DLMF Table 18.6.1). -/
theorem eval_shiftedJacobi_one_sub (α β x : ℝ) (n : ℕ) :
    (shiftedJacobi α β n).eval (1-x) =
      (-1 : ℝ)^n * (shiftedJacobi β α n).eval x := by
  simp only [eval_shiftedJacobi]
  rw [show 2*(1-x)-1 = -(2*x-1) by ring, eval_jacobi_neg]
source

For a polynomial kernel \(K(x,y)\) and polynomial input \(u\), let \(E_yu(x,y)=u(y)\) and \(\mathcal RK(x,y)=K(1-x,y)\). Then extension, multiplication by the reflected kernel, marginal integration, and output reflection give exactly

\[ [I_y((\mathcal RK)E_yu)](1-x) =\int _0^x K(x,y)u(y)\, dy. \]

This assembly is linear in the input and in the kernel. The formula holds for all real \(x\), including the collapsed interval at zero.

Reference: [GO20, Sections 3.1–3.2].

Lean Formalisation
theorem MvPolynomial.eval_triangleExtendY (u : Polynomial ℝ) (x y : ℝ) :
  (MvPolynomial.eval ![x, y]) (MvPolynomial.triangleExtendY u) = Polynomial.eval y u
Lean proof
/-- Inner extension evaluates as `u(y)` at every point. -/
theorem eval_triangleExtendY (u : ℝ[X]) (x y : ℝ) :
    eval (![x,y] : Fin 2 → ℝ) (triangleExtendY u) = u.eval y := by
  change eval (![x,y] : Fin 2 → ℝ) (u.eval₂ C (X 1)) = _
  simp [eval_eval₂_C_X]
source

The bounded integral operator and its polynomial coefficient realization are given in Theorems 6.1.28 and 6.1.30.

Reference details: Finite Proriol marginal coefficient operator and related results

On finitely supported coefficients indexed by \((n,k)\) with \(0\le k\le n\), the normalized Proriol marginal coefficient operator has entries

\[ Q_{j,(n,k)}=\begin{cases} 1,& k=0\text{ and }j=n,\\ 0,& \text{otherwise}.\end{cases} \]

Synthesize its output in \(\widetilde P_n^{(1,0)}\) and multiply by \(1-X\). The resulting univariate polynomial agrees pointwise with the analytic marginal of the synthesized triangle polynomial. Each matrix column has at most one nonzero; no infinite series or infinite matrix multiplication is used.

References: [GO20, Section 3.1]; [Gut22, equation (2.7)].

Lean Formalisation
theorem MvPolynomial.proriolMarginalCoefficients_single (i : (n : ℕ) × Fin (n + 1)) (a : ℝ) :
  MvPolynomial.proriolMarginalCoefficients (Finsupp.single i a) = if i.snd = 0 then Finsupp.single i.fst a else 0
Lean proof
/-- Each column has at most one nonzero, in its own total degree. -/
theorem proriolMarginalCoefficients_single (i : Σ n : ℕ, Fin (n+1)) (a : ℝ) :
    proriolMarginalCoefficients (Finsupp.single i a) =
      if i.2 = 0 then Finsupp.single i.1 a else 0 := by
  classical
  simp [proriolMarginalCoefficients, Finsupp.linearCombination_single, smul_ite]
source
Theorem 6.1.4 Jacobi lowering of the second parameter
✓ 🤖
#

Over every commutative \(\mathbb {Q}\)-algebra, for \(n\ge 0\),

\[ (X+1)(P_n^{(\alpha ,\beta )})'+\beta P_n^{(\alpha ,\beta )} =(n+\beta )P_n^{(\alpha +1,\beta -1)}. \]

No parameter factors are divided out, so exceptional parameters are included.

Lean Formalisation
theorem Polynomial.jacobi_lower_beta.{u_1} {R : Type u_1} [CommRing R] [Algebra ℚ R] (α β : R) (n : ℕ) :
  (Polynomial.X + 1) * Polynomial.derivative (Polynomial.jacobi α β n) + Polynomial.C β * Polynomial.jacobi α β n =
    Polynomial.C (↑n + β) * Polynomial.jacobi (α + 1) (β - 1) n
Lean proof
/-- Lowering the second parameter by a first-order differential operator. -/
theorem jacobi_lower_beta (α β : R) (n : ℕ) :
    (X+1) * derivative (jacobi α β n) + C β * jacobi α β n =
      C ((n : R)+β) * jacobi (α+1) (β-1) n := by
  let : HasUniqueDiv R := HasUniqueDiv.of_module_rat R
  let r (α β : R) (n : ℕ) :=
    (X+1) * derivative (jacobi α β n) + C β * jacobi α β n -
      C ((n : R)+β) * jacobi (α+1) (β-1) n
  have hz (α β : R) (n : ℕ) : (r α β n).eval (-1) = 0 := by
    have hp := congrArg (fun p : R[X] ↦ p.eval β)
      ((ascPochhammer_succ_left R n).symm.trans (ascPochhammer_succ_right R n))
    simp only [eval_mul, eval_X, eval_comp, eval_add, eval_one,
      eval_natCast] at hp
    dsimp [r]
    simp only [eval_sub, eval_add, eval_mul, eval_X, eval_one, eval_C,
      neg_add_cancel, zero_mul, zero_add, eval_jacobi_neg_one]
    simp only [sub_add_cancel]
    linear_combination ((-1 : R)^n * algebraMap ℚ R ((n.factorial : ℚ)⁻¹)) * hp
  have hr : ∀ n : ℕ, ∀ α β : R, r α β n = 0 := by
    intro n
    induction n with
    | zero => intro α β; simp [r]
    | succ n ih =>
      intro α β
      have hd : derivative (r α β (n+1)) = 0 := by
        have hi := ih (α+1) (β+1)
        dsimp only [r] at hi ⊢
        simp only [derivative_sub, derivative_add, derivative_mul, derivative_X,
          derivative_one, add_zero, one_mul, derivative_C, zero_mul, zero_add,
          derivative_jacobi_succ]
        simp only [show β-1+1=β by ring, show β+1-1=β by ring] at *
        simp only [Nat.cast_add, Nat.cast_one, map_add, map_sub, map_mul,
          map_natCast, map_one, map_ofNat] at hi ⊢
        linear_combination (C (algebraMap ℚ R (1/2)) * ((n : R[X])+C α+C β+2)) * hi
      have hc := eq_C_of_derivative_eq_zero hd
      have he := congrArg (fun p : R[X] ↦ p.eval (-1)) hc
      rw [hz, eval_C] at he
      rw [hc, ← he, C_0]
  exact sub_eq_zero.mp (hr n α β)
source

Derived from the Jacobi derivative formula [DLMF, 18.9.15] and endpoint symmetry.

For every \(n\ge 0\) and real \(x\),

\[ \int _0^x\widetilde P_n^{(1,0)}(y)\, dy =\frac{x}{n+1}\widetilde P_n^{(0,1)}(x). \]

Consequently extension in \(y\) followed by the simplex marginal satisfies

\[ I_yE_y\widetilde P_n^{(1,0)}(x) =(1-x)\frac{(-1)^n}{n+1}\widetilde P_n^{(1,0)}(x). \]

With the endpoint factor kept outside the coefficient operator, the diagonal is \(D_{nn}=(-1)^n/(n+1)\). This coefficient formula is proved for every finitely supported input, with exact agreement with the analytic marginal. It includes \(n=0\) and the collapsed integration intervals.

References: [GO20, Section 3.1]; [Gut22, Section 2.3], with the displayed one-based diagonal converted to zero-based indexing.

Lean Formalisation
theorem Polynomial.hasDerivAt_mul_shiftedJacobi_zero_one (n : ℕ) (x : ℝ) :
  HasDerivAt (fun t => t * Polynomial.eval t (Polynomial.shiftedJacobi 0 1 n))
    ((↑n + 1) * Polynomial.eval x (Polynomial.shiftedJacobi 1 0 n)) x
Lean proof
/-- The endpoint-vanishing primitive underlying the Volterra Jacobi diagonal. -/
theorem hasDerivAt_mul_shiftedJacobi_zero_one (n : ℕ) (x : ℝ) :
    HasDerivAt (fun t ↦ t * (shiftedJacobi 0 1 n).eval t)
      (((n : ℝ)+1) * (shiftedJacobi 1 0 n).eval x) x := by
  have ha : HasDerivAt (fun t : ℝ ↦ 2*t-1) 2 x := by
    convert ((hasDerivAt_id x).const_mul 2).sub_const 1 using 1 <;> simp
  have hd := (hasDerivAt_id x).mul (((jacobi (0 : ℝ) 1 n).hasDerivAt (2*x-1)).comp x ha)
  have hi := congrArg (fun p : ℝ[X] ↦ p.eval (2*x-1)) (jacobi_lower_beta 0 1 n)
  norm_num only [zero_add, sub_self, eval_add, eval_mul, eval_C, eval_X, eval_one] at hi
  convert hd using 1
  · ext t
    simp [eval_shiftedJacobi]
  · simp only [eval_shiftedJacobi, Function.comp_apply, id_eq]
    linear_combination -hi
source

For every polynomial \(p\) of degree at most \(N\), construct finitely supported coordinates \(E_Np\) in the signed, reflected Volterra Proriol basis \(Q_{n,k}\). They satisfy

\[ \sum _{n,k}(E_Np)_{n,k}Q_{n,k}(x,y)=p(y),\qquad (E_Np)_{n,k}=0\quad (n{\gt}N). \]

The synthesis identity is a polynomial identity, hence holds for all real \(x,y\). The coordinates are unique, independent of any admissible cutoff \(N\), and additive and homogeneous in \(p\). Applying the existing marginal coefficient operator, including its endpoint factor, gives exactly \(\int _0^{1-x}p(y)\, dy\).

Reference: [GO20, Section 3.1].

Lean Formalisation
theorem MvPolynomial.proriolVolterraSynthesis_transport (N : ℕ) (c : { d // (d.sum fun x e => e) ≤ N } →₀ ℝ) :
  MvPolynomial.proriolVolterraSynthesis ((MvPolynomial.proriolVolterraCoordinateTransport N) c) =
    MvPolynomial.triangleReflect
      ((Finsupp.linearCombination ℝ fun d => MvPolynomial.proriol 0 0 0 (↑d 0 + ↑d 1) (↑d 1)) c)
Lean proof
/-- Transport followed by synthesis is reflection of the original synthesis. -/
theorem proriolVolterraSynthesis_transport (N : ℕ)
    (c : {d : Fin 2 →₀ ℕ // d.sum (fun _ e ↦ e) ≤ N} →₀ ℝ) :
    proriolVolterraSynthesis (proriolVolterraCoordinateTransport N c) =
      triangleReflect (Finsupp.linearCombination ℝ
        (fun d : {d : Fin 2 →₀ ℕ // d.sum (fun _ e ↦ e) ≤ N} ↦
          proriol 0 0 0 (d.1 0+d.1 1) (d.1 1)) c) := by
  classical
  induction c using Finsupp.induction_linear with
  | zero => simp
  | add c d hc hd => simp [hc, hd]
  | single d a =>
    rw [proriolVolterraCoordinateTransport, Finsupp.linearCombination_single,
      map_smul, proriolVolterraSynthesis, Finsupp.linearCombination_single,
      Finsupp.linearCombination_single]
    simp only [Nat.add_sub_cancel, smul_smul, map_smul]
    have hs : (-1 : ℝ)^(d.1 0) * (-1 : ℝ)^(d.1 0) = 1 := by
      rw [← mul_pow]; simp
    rw [hs, mul_one]
source

Explicit rational entries for shifted Jacobi inputs and their sharper total-degree-block support are given in Theorems 6.1.12 and 6.1.11.

The construction uses the finite orthogonal-basis coordinate map.

Let \(e^{(n)}\) be the actual Proriol extension coordinates of \(\widetilde P_n^{(1,0)}\). For every \(n,m\ge 0\),

\[ e^{(n)}_{m,0}= \begin{cases} (-1)^n/(n+1),& m=n,\\ 0,& m\ne n.\end{cases} \]

The complete first two columns are

\[ e^{(0)}=\delta _{(0,0)},\qquad e^{(1)}=-\tfrac 12\delta _{(1,0)}+\tfrac 32\delta _{(1,1)}. \]

Here \(\delta _{(n,k)}\) is the coordinate unit vector in the signed, reflected Volterra Proriol basis. These are equalities of the full finitely supported vectors; all unlisted entries in the two initial columns vanish.

Reference: [GO20, Section 3.1]; [Gut22, Section 2.3].

Lean Formalisation
theorem MvPolynomial.proriolMarginalCoefficients_apply (c : (n : ℕ) × Fin (n + 1) →₀ ℝ) (n : ℕ) :
  (MvPolynomial.proriolMarginalCoefficients c) n = c ⟨n, 0⟩
Lean proof
/-- Marginal selection is exactly restriction to inner degree zero. -/
theorem proriolMarginalCoefficients_apply (c : (Σ n : ℕ, Fin (n+1)) →₀ ℝ) (n : ℕ) :
    proriolMarginalCoefficients c n = c ⟨n, 0⟩ := by
  classical
  induction c using Finsupp.induction_linear with
  | zero => simp
  | add c d hc hd => simp [hc, hd]
  | single i a =>
    rw [proriolMarginalCoefficients_single]
    by_cases hi : i.2 = 0
    · by_cases hn : i.1 = n
      · have he : i = ⟨n, 0⟩ := Sigma.ext hn
          ((Fin.heq_ext_iff (congrArg (fun t : ℕ ↦ t+1) hn)).mpr (by simp only [hi, Fin.val_zero]))
        rw [he]
        simp
      · have he : (⟨n, 0⟩ : Σ n : ℕ, Fin (n+1)) ≠ i :=
          fun h ↦ hn (congrArg Sigma.fst h).symm
        simp [hi, Finsupp.single_eq_of_ne (Ne.symm hn), Finsupp.single_eq_of_ne he]
    · have hn : (⟨n, 0⟩ : Σ n : ℕ, Fin (n+1)) ≠ i := by
        intro he
        subst i
        exact hi rfl
      simp [hi, Finsupp.single_eq_of_ne hn]
source

The formula for arbitrary positive inner degree is not asserted here.

For a polynomial \(q(x,y)=\sum _{a,b}q_{ab}x^ay^b\), define the finite sum

\[ \mathcal M(q)=\sum _{a,b}\frac{q_{ab}}{(b+1)(a+b+2)}. \]

Then \(\mathcal M(q)=\int _0^1\int _0^x q(x,y)\, dy\, dx\). Consequently polynomial pairings and squared norms in the unweighted DLMF triangle are \(\mathcal M(pq)\) and \(\mathcal M(p^2)\). For every degree cutoff \(N\), coordinates of a polynomial of total degree at most \(N\) in the canonical unweighted Proriol basis with parameters \((0,0,0)\) are the corresponding moment quotient, and the squared-norm denominators of the basis members are strictly positive. Reference: [DLMF, 18.37.8] at zero weight parameters.

Lean Formalisation
theorem MvPolynomial.integral_monomial_proriolMeasure_zero (d : Fin 2 →₀ ℕ) (a : ℝ) :
  ∫ (v : Fin 2 → ℝ), (MvPolynomial.eval v) ((MvPolynomial.monomial d) a) ∂MvPolynomial.proriolMeasure 0 0 0 =
    a / ((↑(d 1) + 1) * (↑(d 0) + ↑(d 1) + 2))
Lean proof
/-- Exact integration of a monomial on the unweighted DLMF triangle. -/
theorem integral_monomial_proriolMeasure_zero (d : Fin 2 →₀ ℕ) (a : ℝ) :
    (∫ v, eval v (monomial d a) ∂proriolMeasure 0 0 0) =
      a / (((d 1 : ℝ)+1)*((d 0 : ℝ)+d 1+2)) := by
  rw [integral_proriolMeasure_density (by norm_num) (by norm_num) (by norm_num)]
  simp only [Real.rpow_zero, one_mul, eval_monomial]
  have he (x y : ℝ) : d.prod (fun i n ↦ (![x,y] : Fin 2 → ℝ) i ^ n) =
      x^(d 0)*y^(d 1) := by
    rw [Finsupp.prod_fintype]
    · simp
    · simp
  simp_rw [he, ← mul_assoc]
  have heq (x : Set.Ioo (0 : ℝ) 1) :
      (∫ y : Set.Ioo (0 : ℝ) (x : ℝ), a*(x : ℝ)^(d 0)*(y : ℝ)^(d 1)) =
      ∫ y in (0 : ℝ)..(x : ℝ), a*(x : ℝ)^(d 0)*y^(d 1) := by
    rw [integral_subtype measurableSet_Ioo (fun y : ℝ ↦ a*(x : ℝ)^(d 0)*y^(d 1)),
      restrict_Ioo_eq_restrict_Ioc, intervalIntegral.integral_of_le x.property.1.le]
  simp_rw [heq]
  rw [integral_subtype measurableSet_Ioo
    (fun x : ℝ ↦ ∫ y in (0 : ℝ)..x, a*x^(d 0)*y^(d 1)),
    restrict_Ioo_eq_restrict_Ioc,
    ← intervalIntegral.integral_of_le (by norm_num : (0 : ℝ) ≤ 1)]
  simp_rw [intervalIntegral.integral_const_mul, integral_pow]
  simp only [zero_pow (Nat.succ_ne_zero _), sub_zero]
  calc
    _ = a / ((d 1 : ℝ)+1) * ∫ x in (0 : ℝ)..1, x^(d 0+d 1+1) := by
      rw [← intervalIntegral.integral_const_mul]
      apply intervalIntegral.integral_congr
      intro x _
      simp only [pow_add, pow_one]
      ring
    _ = _ := by
      rw [integral_pow]
      simp only [one_pow, zero_pow (Nat.succ_ne_zero _), sub_zero, Nat.cast_add, Nat.cast_one, div_eq_mul_inv, mul_inv_rev]
      ring
source
Theorem 6.1.9 Elementary unweighted Proriol norms
✓ 🤖

For \(\beta {\gt}-1\), the Jacobi norm with first parameter zero is

\[ \int _{-1}^1(1+x)^\beta \bigl(P_n^{(0,\beta )}(x)\bigr)^2\, dx =\frac{2^{\beta +1}}{2n+\beta +1}. \]

Writing \(P_{m+k,k}\) for the unweighted DLMF Proriol polynomial, for all \(m,k\ge 0\),

\[ \mathcal M(P_{m+k,k}^2)=\frac1{2(m+k+1)(2k+1)}. \]

Reference: [DLMF, Table 18.3.1 and 18.37.8].

Lean Formalisation
theorem Polynomial.integral_sq_jacobi_zero_left {β : ℝ} (hβ : -1 < β) (n : ℕ) :
  ∫ (x : ℝ), Polynomial.eval x (Polynomial.jacobi 0 β n) ^ 2 ∂Polynomial.jacobiMeasure 0 β =
    2 ^ (β + 1) / (2 * ↑n + β + 1)
Lean proof
/-- Jacobi norms with first parameter zero need no Gamma factors. -/
theorem integral_sq_jacobi_zero_left {β : ℝ} (hβ : -1 < β) (n : ℕ) :
    (∫ x, (jacobi 0 β n).eval x ^ 2 ∂jacobiMeasure 0 β) =
      (2 : ℝ)^(β+1)/(2*n+β+1) := by
  cases n with
  | zero =>
    rw [integral_sq_jacobi_zero (by norm_num) hβ]
    simp only [GammaOn, GammaPoint.ofPos, zero_add, Nat.cast_zero, mul_zero, Gamma_one, mul_one]
    rw [show β+2 = (β+1)+1 by ring, Gamma_add_one (by linarith : β+1 ≠ 0)]
    have hg : Gamma (β+1) ≠ 0 := (Gamma_pos_of_pos (by linarith)).ne'
    field_simp
  | succ n =>
    rw [integral_sq_jacobi_succ (by norm_num) hβ]
    simp only [GammaOn, GammaPoint.ofPos, zero_add, add_zero]
    rw [show (n : ℝ)+2 = (n+1 : ℕ)+1 by push_cast; ring, Gamma_nat_eq_factorial]
    have hg : Gamma ((n : ℝ)+β+2) ≠ 0 :=
      (Gamma_pos_of_pos (by have := Nat.cast_nonneg (α := ℝ) n; linarith)).ne'
    have hf : ((n+1).factorial : ℝ) ≠ 0 := Nat.cast_ne_zero.mpr (Nat.factorial_ne_zero _)
    have hd : 2*(n : ℝ)+β+3 ≠ 0 := by have := Nat.cast_nonneg (α := ℝ) n; linarith
    simp only [Nat.cast_succ]
    field_simp
    ring
source

Let \(p\) have degree at most \(N\), and let \(e=E_Np\) be its actual extension coordinates in the signed, reflected Volterra basis. For \(m+k\le N\),

\[ e_{m+k,k}=(-1)^m\frac{\mathcal M(p(y)P_{m+k,k}(x,y))}{\mathcal M(P_{m+k,k}^2)} =(-1)^m\, 2(m+k+1)(2k+1)\, \mathcal M(p(y)P_{m+k,k}(x,y)). \]

Here \(P\) is the unreflected DLMF basis and \(\mathcal M\) is the explicit finite coefficient sum above. Entries above the cutoff vanish by the existing extension theorem. Thus every entry is expressed using finite polynomial arithmetic, with no integral or abstract basis-coordinate operation on the right-hand side.

Reference: [GO20, Section 3.1], with orthogonal projection in the normalization of [DLMF, 18.37.8].

Lean Formalisation
theorem MvPolynomial.proriolVolterraCoordinateTransport_apply (N : ℕ) (c : { d // (d.sum fun x e => e) ≤ N } →₀ ℝ)
  (d : { d // (d.sum fun x e => e) ≤ N }) :
  ((MvPolynomial.proriolVolterraCoordinateTransport N) c) ⟨↑d 0 + ↑d 1, ⟨↑d 1, ⋯⟩⟩ = (-1) ^ ↑d 0 * c d
Lean proof
/-- Entrywise effect of the signed coordinate transport. -/
theorem proriolVolterraCoordinateTransport_apply (N : ℕ)
    (c : {d : Fin 2 →₀ ℕ // d.sum (fun _ e ↦ e) ≤ N} →₀ ℝ)
    (d : {d : Fin 2 →₀ ℕ // d.sum (fun _ e ↦ e) ≤ N}) :
    proriolVolterraCoordinateTransport N c ⟨d.1 0+d.1 1, ⟨d.1 1, by omega⟩⟩ =
      (-1 : ℝ)^(d.1 0) * c d := by
  classical
  induction c using Finsupp.induction_linear with
  | zero => simp
  | add c e hc he => simp [hc, he, mul_add]
  | single e a =>
    rw [proriolVolterraCoordinateTransport, Finsupp.linearCombination_single]
    simp only [Finsupp.smul_apply, smul_eq_mul]
    by_cases he : e = d
    · rw [he]
      simp [mul_comm]
    · have hn : (⟨d.1 0+d.1 1, ⟨d.1 1, by omega⟩⟩ : Σ n : ℕ, Fin (n+1)) ≠
          ⟨e.1 0+e.1 1, ⟨e.1 1, by omega⟩⟩ := by
        intro h
        exact he (Subtype.ext (diskIndex_injective h)).symm
      rw [Finsupp.single_eq_of_ne hn, Finsupp.single_eq_of_ne (Ne.symm he)]
      simp
source

The explicit shifted-Jacobi formula and its support are Theorems 6.1.12 and 6.1.11.

The inner-coordinate extension of \(P_n^{(1,0)}(2y-1)\) is orthogonal, for unnormalized area measure on \(0{\lt}y{\lt}x{\lt}1\), to every polynomial of total degree less than \(n\). Consequently its Proriol extension coordinates vanish in every total-degree block except \(n\). Reference: [GO20, Section 3.1].

Lean Formalisation
theorem Polynomial.integral_mul_shiftedJacobi_one_zero_eq_zero {n : ℕ} (q : Polynomial ℝ) (hq : q.natDegree < n) :
  ∫ (y : ℝ) in 0..1, (1 - y) * Polynomial.eval y q * Polynomial.eval y (Polynomial.shiftedJacobi 1 0 n) = 0
Lean proof
/-- Orthogonality for shifted `(1,0)` modes with the unnormalized density. -/
theorem integral_mul_shiftedJacobi_one_zero_eq_zero {n : ℕ} (q : ℝ[X])
    (hq : q.natDegree < n) :
    (∫ y in (0 : ℝ)..1, (1-y)*q.eval y*(shiftedJacobi 1 0 n).eval y) = 0 := by
  have h := (isOrthogonal_shiftedJacobiSequence (by norm_num : (-1 : ℝ) < 1)
    (by norm_num : (-1 : ℝ) < 0)).integralInner_eq_zero_of_degree_lt
      (hasFiniteMoments_unitJacobiMeasure (by norm_num) (by norm_num))
      (degree_le_natDegree.trans_lt (by exact_mod_cast hq))
  change integralInner (unitJacobiMeasure 1 0) (IntegrablePair.of (unitJacobiMeasure 1 0) q (shiftedJacobi 1 0 n) (h := (hasFiniteMoments_unitJacobiMeasure (by norm_num) (by norm_num)).integrable_mul _ _)) = 0 at h
  let g : IntegrableInput (unitJacobiMeasure 1 0) := ⟨fun x ↦ q.eval x * (shiftedJacobi 1 0 n).eval x, (hasFiniteMoments_unitJacobiMeasure (by norm_num) (by norm_num)).integrable_mul _ _⟩
  have hg : Measurable g.val := by dsimp [g]; fun_prop
  have hd : (∫ x, g.val x ∂unitJacobiMeasure 1 0) = 4 *
      ∫ x in (0 : ℝ)..1, (1-x) * g.val x := by
    rw [integral_unitJacobiMeasure_subtype 1 0 g hg]
    simp only [unitJacobiWeight_apply, add_zero, Real.rpow_one, Real.rpow_zero,
      mul_one, mul_assoc]
    norm_num only [one_add_one_eq_two, Real.rpow_two]
    rw [integral_const_mul, integral_subtype measurableSet_Ioo (fun x : ℝ ↦ (1-x)*g.val x),
      restrict_Ioo_eq_restrict_Ioc,
      ← intervalIntegral.integral_of_le (by norm_num : (0 : ℝ) ≤ 1)]
  dsimp only [g] at hd
  rw [integralInner, hd] at h
  have he : (∫ y in (0 : ℝ)..1, (1-y)*(q.eval y*(shiftedJacobi 1 0 n).eval y)) = 0 := by
    nlinarith [h]
  simpa only [mul_assoc] using he
source

In the signed reflected Volterra convention, every extension column is

\[ E_{(m,k),n}=\begin{cases} (-1)^{n-k}\dfrac {2k+1}{n+1},& m=n,\\ 0,& m\ne n. \end{cases} \]

These are the actual previously defined coordinates, including the constant and linear columns. More generally, for \(\deg q\le n\), \(\int _0^1P_n^{(1,0)}(2y-1)q(y)\, dy=q(1)/(n+1)\). Reference: [GO20, Section 3.1].

Lean Formalisation
theorem Polynomial.integral_shiftedJacobi_one_zero_mul (n : ℕ) (q : Polynomial ℝ) (hq : q.natDegree ≤ n) :
  ∫ (y : ℝ) in 0..1, Polynomial.eval y (Polynomial.shiftedJacobi 1 0 n) * Polynomial.eval y q =
    Polynomial.eval 1 q / (↑n + 1)
Lean proof
/-- Endpoint reproduction by a shifted `(1,0)` Jacobi mode. -/
theorem integral_shiftedJacobi_one_zero_mul (n : ℕ) (q : ℝ[X]) (hq : q.natDegree ≤ n) :
    (∫ y in (0 : ℝ)..1, (shiftedJacobi 1 0 n).eval y*q.eval y) =
      q.eval 1/((n : ℝ)+1) := by
  have hi : (∫ y in (0 : ℝ)..1, (shiftedJacobi 1 0 n).eval y) = 1/((n : ℝ)+1) := by
    rw [integral_shiftedJacobi_one_zero, eval_shiftedJacobi_zero_left_one, one_mul]
  by_cases hn : n = 0
  · subst n
    have hq0 : q.natDegree = 0 := Nat.eq_zero_of_le_zero hq
    rw [eq_C_of_natDegree_eq_zero hq0]
    simp only [eval_C, intervalIntegral.integral_mul_const, hi]
    ring
  let r := q /ₘ (X-C (1 : ℝ))
  have hr : r.natDegree < n := by
    dsimp only [r]
    rw [natDegree_divByMonic _ (monic_X_sub_C _), natDegree_X_sub_C]
    omega
  have he (y : ℝ) : q.eval 1+(y-1)*r.eval y = q.eval y := by
    have h := congrArg (fun p : ℝ[X] ↦ p.eval y) (modByMonic_add_div q (X-C (1 : ℝ)))
    simpa only [modByMonic_X_sub_C_eq_C_eval, eval_add, eval_mul, eval_sub, eval_C, eval_X] using h
  calc
    _ = q.eval 1*(∫ y in (0 : ℝ)..1, (shiftedJacobi 1 0 n).eval y) -
        ∫ y in (0 : ℝ)..1, (1-y)*r.eval y*(shiftedJacobi 1 0 n).eval y := by
      rw [← intervalIntegral.integral_const_mul,
        ← intervalIntegral.integral_sub (by apply Continuous.intervalIntegrable; fun_prop)
          (by apply Continuous.intervalIntegrable; fun_prop)]
      apply intervalIntegral.integral_congr
      intro y _
      dsimp only
      linear_combination -(shiftedJacobi 1 0 n).eval y*he y
    _ = _ := by
      rw [integral_mul_shiftedJacobi_one_zero_eq_zero r hr, hi, sub_zero]
      ring
source

Let \(S\) be synthesis in the signed reflected Proriol basis \(Q_{n,k}\). For finite shifted Jacobi \((1,0)\) coefficients \(c\), set

\[ Ec=S^{-1}\! \left(\sum _n c_nP_n^{(1,0)}(2y-1)\right),\qquad M_Kb=S^{-1}\bigl(K(1-x,y)Sb\bigr),\qquad B_K=DM_KE, \]

where \(b\) is a finite triangular coefficient vector and \(D\) selects inner index zero. The \(n\)th column of \(E\) is the coordinate vector of \(P_n^{(1,0)}(2y-1)\). The endpoint factor and output reflection are kept outside \(B_K\). Reference: [GO20, Sections 3.1–3.2].

Lean Formalisation
theorem MvPolynomial.proriolVolterraSynthesis_surjective : Function.Surjective ⇑MvPolynomial.proriolVolterraSynthesis
Lean proof
/-- Every polynomial has finite signed reflected Proriol coordinates. -/
theorem proriolVolterraSynthesis_surjective : Function.Surjective proriolVolterraSynthesis := by
  intro p
  let q := triangleReflect p
  let N := q.totalDegree
  let b := proriolDegreeBasis (by norm_num : (-1 : ℝ) < 0)
    (by norm_num : (-1 : ℝ) < 0) (by norm_num : (-1 : ℝ) < 0) N
  let v : restrictTotalDegree (Fin 2) ℝ N :=
    ⟨q, (mem_restrictTotalDegree (Fin 2) N q).mpr le_rfl⟩
  refine ⟨proriolVolterraCoordinateTransport N (b.repr v), ?_⟩
  rw [proriolVolterraSynthesis_transport]
  have h := congrArg (fun t : restrictTotalDegree (Fin 2) ℝ N ↦
    (t : MvPolynomial (Fin 2) ℝ)) (b.linearCombination_repr v)
  have hf : (fun d ↦ (b d : MvPolynomial (Fin 2) ℝ)) =
      (fun d : {d : Fin 2 →₀ ℕ // d.sum (fun _ e ↦ e) ≤ N} ↦
        proriol 0 0 0 (d.1 0+d.1 1) (d.1 1)) := by
    funext d
    exact proriolDegreeBasis_apply _ _ _ N d
  change (↑((b.repr v).sum (fun i a ↦ a • b i)) : MvPolynomial (Fin 2) ℝ) = q at h
  simp only [Finsupp.sum, Submodule.coe_sum, Submodule.coe_smul] at h
  rw [← hf, Finsupp.linearCombination_apply]
  simp only [Finsupp.sum]
  rw [h]
  exact triangleReflect_involutive p
source
Theorem 6.1.14 Algebraic properties of Volterra coefficient assembly
✓ 🤖

Synthesis \(S\) is a linear equivalence between finitely supported triangular coefficients and bivariate polynomials. The kernel map \(K\mapsto M_K\) is an algebra homomorphism on finitely supported vectors.

Lean Formalisation
theorem MvPolynomial.proriolVolterraSynthesis_surjective : Function.Surjective ⇑MvPolynomial.proriolVolterraSynthesis
Lean proof
/-- Every polynomial has finite signed reflected Proriol coordinates. -/
theorem proriolVolterraSynthesis_surjective : Function.Surjective proriolVolterraSynthesis := by
  intro p
  let q := triangleReflect p
  let N := q.totalDegree
  let b := proriolDegreeBasis (by norm_num : (-1 : ℝ) < 0)
    (by norm_num : (-1 : ℝ) < 0) (by norm_num : (-1 : ℝ) < 0) N
  let v : restrictTotalDegree (Fin 2) ℝ N :=
    ⟨q, (mem_restrictTotalDegree (Fin 2) N q).mpr le_rfl⟩
  refine ⟨proriolVolterraCoordinateTransport N (b.repr v), ?_⟩
  rw [proriolVolterraSynthesis_transport]
  have h := congrArg (fun t : restrictTotalDegree (Fin 2) ℝ N ↦
    (t : MvPolynomial (Fin 2) ℝ)) (b.linearCombination_repr v)
  have hf : (fun d ↦ (b d : MvPolynomial (Fin 2) ℝ)) =
      (fun d : {d : Fin 2 →₀ ℕ // d.sum (fun _ e ↦ e) ≤ N} ↦
        proriol 0 0 0 (d.1 0+d.1 1) (d.1 1)) := by
    funext d
    exact proriolDegreeBasis_apply _ _ _ N d
  change (↑((b.repr v).sum (fun i a ↦ a • b i)) : MvPolynomial (Fin 2) ℝ) = q at h
  simp only [Finsupp.sum, Submodule.coe_sum, Submodule.coe_smul] at h
  rw [← hf, Finsupp.linearCombination_apply]
  simp only [Finsupp.sum]
  rw [h]
  exact triangleReflect_involutive p
source
Reference details: Exact finite Volterra coefficient action

For every real bivariate polynomial kernel \(K\), finite coefficient vector \(c\), and real \(x\), writing \(u(y)=\sum _n c_nP_n^{(1,0)}(2y-1)\),

\[ x\sum _m(B_Kc)_m P_m^{(1,0)}(1-2x)=\int _0^x K(x,y)u(y)\, dy. \]

The integral is oriented when \(x{\lt}0\). Kernel multiplication reconstructs exactly \(K(1-x,y)Sc\). For \(K=1\), \(B_K\) is the existing diagonal with entries \((-1)^n/(n+1)\), including degree zero. Reference: [GO20, Sections 3.1–3.2].

Lean Formalisation
theorem MvPolynomial.proriolVolterraSynthesis_kernelMap (K : MvPolynomial (Fin 2) ℝ) (c : (n : ℕ) × Fin (n + 1) →₀ ℝ) :
  MvPolynomial.proriolVolterraSynthesis ((MvPolynomial.proriolKernelMap K) c) =
    MvPolynomial.triangleReflect K * MvPolynomial.proriolVolterraSynthesis c
Lean proof
/-- Kernel multiplication reconstructs the reflected polynomial product exactly. -/
theorem proriolVolterraSynthesis_kernelMap (K : MvPolynomial (Fin 2) ℝ)
    (c : (Σ n : ℕ, Fin (n+1)) →₀ ℝ) :
    proriolVolterraSynthesis (proriolKernelMap K c) =
      triangleReflect K * proriolVolterraSynthesis c := by
  change proriolVolterraEquiv (proriolVolterraEquiv.symm _) = _
  exact proriolVolterraEquiv.apply_symm_apply _
source

Let \(d=\operatorname {totalDegree}K\), with \(d=0\) for the zero kernel. The degree blocks of \(M_K\) vanish when \(|m-n|{\gt}d\), and the core Volterra matrix satisfies \((B_K)_{mn}=0\) under the same condition. These bounds precede the explicit endpoint factor and reflection. Inputs supported in \(0\le n{\lt}N\) produce coefficients supported in \(0\le m{\lt}N+d\). The corresponding \((N+d)\times N\) section has exactly the full operator’s action on the retained rows and loses no output coefficients. Reference: [GO20, Sections 3.1–3.2].

Lean Formalisation
theorem MvPolynomial.triangleReflect_proriolVolterraSynthesis_single (i : (n : ℕ) × Fin (n + 1)) (a : ℝ) :
  MvPolynomial.triangleReflect (MvPolynomial.proriolVolterraSynthesis (Finsupp.single i a)) =
    (a * (-1) ^ (i.fst - ↑i.snd)) • MvPolynomial.proriol 0 0 0 i.fst ↑i.snd
Lean proof
/-- Reflection removes the simplex coordinate change from each synthesis column. -/
theorem triangleReflect_proriolVolterraSynthesis_single
    (i : Σ n : ℕ, Fin (n+1)) (a : ℝ) :
    triangleReflect (proriolVolterraSynthesis (Finsupp.single i a)) =
      (a * (-1 : ℝ)^(i.1-i.2.val)) • proriol 0 0 0 i.1 i.2 := by
  simp only [proriolVolterraSynthesis, Finsupp.linearCombination_single, map_smul,
    smul_smul]
  rw [triangleReflect_involutive]
source

No same-size truncation of intermediate multiplication operators is asserted.

For \(p\in \mathbb {R}[t]\), polynomial functional calculus obeys \(M_{p(K)}=p(M_K)\), and the two coordinate operators commute. Suppose bivariate polynomials satisfy \(p_{k+2}=a_kp_{k+1}+b_kp_k\). Applying the backward Clenshaw recurrence to \(M_{a_k},M_{b_k},M_{c_k}\) with initial operators \(M_{p_0},M_{p_1}\) computes \(M_{\sum _{k{\lt}N}c_kp_k}\) exactly. Placing it between \(E\) and \(D\) gives \(B_{\sum _{k{\lt}N}c_kp_k}\). This permits polynomial-valued coefficients and nested coordinate expansions. The identity is on finitely supported vectors; no floating-point stability or finite-section recurrence is claimed. References: [Cle55]; [GO20, Sections 3.1–3.2].

Lean Formalisation
theorem MvPolynomial.proriolKernelMap_aeval (K : MvPolynomial (Fin 2) ℝ) (p : Polynomial ℝ) :
  MvPolynomial.proriolKernelMap ((Polynomial.aeval K) p) = (Polynomial.aeval (MvPolynomial.proriolKernelMap K)) p
Lean proof
/-- Polynomial functional calculus commutes with the kernel operator map.
In particular this applies to either coordinate and to nested kernel expansions. -/
theorem proriolKernelMap_aeval (K : MvPolynomial (Fin 2) ℝ) (p : ℝ[X]) :
    proriolKernelMap (Polynomial.aeval K p) =
      Polynomial.aeval (proriolKernelMap K) p := by
  exact (Polynomial.aeval_algHom_apply proriolKernelMap K p).symm
source
Definition 6.1.18 The physical Volterra triangle
✓ 🤖
#

The physical Volterra triangle is \(\Delta =\{ (x,y)\in \mathbb R^2:0\le y\le x\le 1\} \).

Lean Formalisation
def Real.volterraTriangle : Set (Fin 2 → ℝ)
Lean definition
/-- The physical triangle for Volterra integration on the unit interval. -/
def volterraTriangle : Set (Fin 2 → ℝ) :=
  {z | z 0 ∈ Icc 0 1 ∧ z 1 ∈ Icc 0 (z 0)}
source
Formal details: Integrable Volterra row pairs and related results
Definition 6.1.19 Integrable Volterra row pairs
✓ 🤖
#

For \(x\in \mathbb R\), put \(J_x=(\min (0,x),\max (0,x))\). A Volterra input at \(x\) consists of two real-valued functions \(k,f\) on \(J_x\) whose product is Lebesgue integrable there. Neither factor is required to be separately integrable, and no endpoint values are part of the input.

Lean Formalisation
inductive Real.VolterraIntegralInput (x : ℝ) : Type
Lean definition
/-- A pair of classical rows with an integrable product on the open integration interval. -/
structure VolterraIntegralInput (x : ℝ) where
  kernel : Ioo (min 0 x) (max 0 x) → ℝ
  input : Ioo (min 0 x) (max 0 x) → ℝ
  integrable : Integrable (fun y ↦ kernel y * input y)
    ((volume : Measure ℝ).comap Subtype.val)
source

Let \(J_x=(\min (0,x),\max (0,x))\). If \(y\mapsto K(x,y)f(y)\) is integrable between \(0\) and \(x\), its restrictions to \(J_x\) define an integrable Volterra row. The product is integrable in each of the following cases:

  • \(K\) is continuous on \(\Delta \), \(f\) is continuous on \([0,1]\), and \(x\in [0,1]\);

  • \(K\) is a polynomial kernel, \(f\) is locally integrable on \(\mathbb {R}\), and \(x\in \mathbb {R}\);

  • \(K\) is continuous on \(\Delta \), \(x\in [0,1]\), and \(f\) is integrable on \([0,x]\);

  • \(K\) is a polynomial kernel, \(f\) is integrable on \([0,b]\), and \(x\in [0,b]\);

  • the slice \(K(x,\cdot )\) is absolutely continuous between \(0\) and \(x\), and \(f\) is integrable on that interval.

Lean Formalisation
theorem Real.intervalIntegrable_volterra {K : (Fin 2 → ℝ) → ℝ} {f : ℝ → ℝ} (hK : ContinuousOn K Real.volterraTriangle)
  (hf : ContinuousOn f (Set.Icc 0 1)) {x : ℝ} (hx : x ∈ Set.Icc 0 1) :
  IntervalIntegrable (fun y => K ![x, y] * f y) MeasureTheory.volume 0 x
Lean proof
/-- Continuous triangle kernels and continuous inputs give integrable slices. -/
theorem intervalIntegrable_volterra {K : (Fin 2 → ℝ) → ℝ} {f : ℝ → ℝ}
    (hK : ContinuousOn K volterraTriangle) (hf : ContinuousOn f (Icc 0 1))
    {x : ℝ} (hx : x ∈ Icc 0 1) :
    IntervalIntegrable (fun y ↦ K ![x,y] * f y) volume 0 x := by
  apply ContinuousOn.intervalIntegrable_of_Icc (by exact hx.1)
  apply ContinuousOn.mul
  · apply hK.comp (by fun_prop : ContinuousOn (fun y : ℝ ↦ ![x,y]) (Icc 0 x))
    intro y hy
    exact ⟨hx, hy⟩
  · exact hf.mono (Icc_subset_Icc le_rfl hx.2)
source
Definition 6.1.21 Classical Volterra integration
✓ 🤖
#

For an integrable row pair \((k,f)\) at \(x\), define its oriented value by

\[ V(k,f;x)= \begin{cases} \displaystyle \int _{J_x} k(y)f(y)\, dy,& x\ge 0,\\ \displaystyle -\int _{J_x} k(y)f(y)\, dy,& x{\lt}0. \end{cases} \]

For the row \(k(y)=K(x,y)\) this is denoted \(V_Kf(x)\). The integral exists by the input’s product-integrability condition.

Lean Formalisation
def Real.volterraIntegral {x : ℝ} (d : x.VolterraIntegralInput) : ℝ
Lean definition
/-- The classical oriented integral of an integrable kernel-input row pair. -/
def volterraIntegral {x : ℝ} (d : VolterraIntegralInput x) : ℝ :=
  if 0 ≤ x then ∫ y, d.kernel y * d.input y ∂(volume : Measure ℝ).comap Subtype.val else -(∫ y, d.kernel y * d.input y ∂(volume : Measure ℝ).comap Subtype.val)
source
Reference details: Orientation and the zero-length row and related results
Theorem 6.1.22 Orientation and the zero-length row
✓ 🤖

For a row with \(K(x,\cdot )f\) integrable on \(J_x=(\min (0,x),\max (0,x))\),

\[ V_Kf(x)= \begin{cases} \displaystyle \int _{J_x}K(x,y)f(y)\, dy,& x\ge 0,\\ \displaystyle -\int _{J_x}K(x,y)f(y)\, dy,& x{\lt}0. \end{cases} \]

In particular \(V_Kf(0)=0\); no endpoint values of the factors are used.

Lean Formalisation
theorem Real.volterraIntegral_of_nonneg {x : ℝ} (hx : 0 ≤ x) (d : x.VolterraIntegralInput) :
  Real.volterraIntegral d =
    ∫ (y : { x_1 // x_1 ∈ Set.Ioo (min 0 x) (max 0 x) }),
      d.kernel y * d.input y ∂MeasureTheory.Measure.comap Subtype.val MeasureTheory.volume
Lean proof
/-- Nonnegative endpoints give the integral over the open row interval. -/
theorem volterraIntegral_of_nonneg {x : ℝ} (hx : 0 ≤ x) (d : VolterraIntegralInput x) :
    volterraIntegral d =
      ∫ y, d.kernel y * d.input y ∂(volume : Measure ℝ).comap Subtype.val :=
  ite_eq_left hx
source
Theorem 6.1.23 Volterra kernel and input stability
✓ 🤖

Let \(K,L\) be continuous on \(\Delta \) and \(f,g\) continuous on \([0,1]\). Their Volterra integrands are integrable for each \(x\in [0,1]\). Suppose \(M,F,\delta ,\eta \ge 0\), with \(|K|\le M\), \(|f|\le F\), \(|L-K|\le \delta \) and \(|g-f|\le \eta \) on the respective domains. Then

\[ |V_Lg(x)-V_Kf(x)|\le x\bigl(\delta F+(M+\delta )\eta \bigr). \]

For continuous approximants \(L_n,g_n\) with such nonnegative uniform error bounds \(\delta _n,\eta _n\to 0\), the outputs converge uniformly to \(V_Kf\) on \([0,1]\).

Lean Formalisation
theorem Real.abs_volterraIntegral_sub_le {K L : (Fin 2 → ℝ) → ℝ} {f g : ℝ → ℝ} (hK : ContinuousOn K Real.volterraTriangle)
  (hL : ContinuousOn L Real.volterraTriangle) (hf : ContinuousOn f (Set.Icc 0 1)) (hg : ContinuousOn g (Set.Icc 0 1))
  {M F δ η : ℝ} (hM : 0 ≤ M) (_hF : 0 ≤ F) (hδ : 0 ≤ δ) (_hη : 0 ≤ η) (bK : ∀ z ∈ Real.volterraTriangle, |K z| ≤ M)
  (bf : ∀ y ∈ Set.Icc 0 1, |f y| ≤ F) (eK : ∀ z ∈ Real.volterraTriangle, |L z - K z| ≤ δ)
  (ef : ∀ y ∈ Set.Icc 0 1, |g y - f y| ≤ η) (x : ↑(Set.Icc 0 1)) :
  |Real.volterraIntegral (Real.VolterraIntegralInput.ofContinuous hL hg x) -
        Real.volterraIntegral (Real.VolterraIntegralInput.ofContinuous hK hf x)| ≤
    (δ * F + (M + δ) * η) * ↑x
Lean proof
/-- Kernel and input errors contribute separately, including their cross term. -/
theorem abs_volterraIntegral_sub_le {K L : (Fin 2 → ℝ) → ℝ} {f g : ℝ → ℝ}
    (hK : ContinuousOn K volterraTriangle) (hL : ContinuousOn L volterraTriangle)
    (hf : ContinuousOn f (Icc 0 1)) (hg : ContinuousOn g (Icc 0 1))
    {M F δ η : ℝ} (hM : 0 ≤ M) (_hF : 0 ≤ F) (hδ : 0 ≤ δ) (_hη : 0 ≤ η)
    (bK : ∀ z ∈ volterraTriangle, |K z| ≤ M)
    (bf : ∀ y ∈ Icc 0 1, |f y| ≤ F)
    (eK : ∀ z ∈ volterraTriangle, |L z-K z| ≤ δ)
    (ef : ∀ y ∈ Icc 0 1, |g y-f y| ≤ η)
    (x : Icc (0 : ℝ) 1) :
    |volterraIntegral (VolterraIntegralInput.ofContinuous hL hg x) -
      volterraIntegral (VolterraIntegralInput.ofContinuous hK hf x)| ≤
      (δ*F + (M+δ)*η)*x := by
  have hx := x.property
  simp only [VolterraIntegralInput.ofContinuous, volterraIntegral_ofKernel]
  rw [← intervalIntegral.integral_sub (intervalIntegrable_volterra hL hg hx)
    (intervalIntegrable_volterra hK hf hx)]
  have hb : ∀ y ∈ uIoc (0 : ℝ) x,
      ‖L ![x,y]*g y-K ![x,y]*f y‖ ≤ δ*F+(M+δ)*η := by
    intro y hy
    rw [uIoc_of_le hx.1] at hy
    have hyx : y ∈ Icc (0 : ℝ) (x : ℝ) := Ioc_subset_Icc_self hy
    have hy1 : y ∈ Icc (0 : ℝ) 1 := ⟨hyx.1, hyx.2.trans hx.2⟩
    have hz : (![x,y] : Fin 2 → ℝ) ∈ volterraTriangle := ⟨hx, hyx⟩
    have bL : |L ![x,y]| ≤ M+δ := by
      calc
        _ = |K ![x,y]+(L ![x,y]-K ![x,y])| := by congr 1; ring
        _ ≤ _ := abs_add_le _ _
        _ ≤ M+δ := add_le_add (bK _ hz) (eK _ hz)
    rw [Real.norm_eq_abs]
    calc
      _ = |(L ![x,y]-K ![x,y])*f y + L ![x,y]*(g y-f y)| := by congr 1; ring
      _ ≤ _ := abs_add_le _ _
      _ ≤ δ*F+(M+δ)*η := by
        simp only [abs_mul]
        exact add_le_add (mul_le_mul (eK _ hz) (bf y hy1) (abs_nonneg _) hδ)
          (mul_le_mul bL (ef y hy1) (abs_nonneg _) (by positivity))
  simpa only [Real.norm_eq_abs, sub_zero, abs_of_nonneg hx.1] using
    intervalIntegral.norm_integral_le_of_norm_le_const hb
source

Every continuous real kernel on \(\Delta \) admits uniform bivariate polynomial approximations. More generally, polynomial functions uniformly approximate continuous real functions on any compact subset of \(\mathbb {R}^2\). Let \(P\) be a polynomial kernel and \(p=\sum _n c_nJ_n\) a finite shifted-Jacobi input, with \(J_n=P_n^{(1,0)}(2x-1)\). If their kernel and input errors relative to \(K,f\) are bounded by \(\delta ,\eta \), then

\[ \left|x\sum _j(B_Pc)_jJ_j(1-x)-V_Kf(x)\right| \le x\bigl(\delta F+(M+\delta )\eta \bigr),\qquad B_P=D M_P E. \]

Vanishing uniform approximation errors therefore give uniform convergence of these assembled physical outputs on all of \([0,1]\), including the endpoints. For each continuous \(K,f\) and each \(\varepsilon {\gt}0\), there exist a polynomial \(P\) and finite coefficient vector \(c\) for which this output error is less than \(\varepsilon \) everywhere on \([0,1]\). Reference: [GO20, Sections 3.1–3.2].

Lean Formalisation
theorem MvPolynomial.isCompact_volterraTriangle : IsCompact Real.volterraTriangle
Lean proof
/-- The physical Volterra triangle is compact. -/
theorem isCompact_volterraTriangle : IsCompact volterraTriangle := by
  have he : volterraTriangle = Icc (0 : Fin 2 → ℝ) 1 ∩ {z | z 1 ≤ z 0} := by
    ext z
    constructor
    · intro ⟨hx, hy⟩
      refine ⟨⟨?_, ?_⟩, hy.2⟩
      · intro i; fin_cases i <;> simp_all
      · intro i; fin_cases i <;> simp_all; exact hy.2.trans hx.2
    · rintro ⟨⟨h0,h1⟩,hy⟩
      exact ⟨⟨h0 0,h1 0⟩,⟨h0 1,hy⟩⟩
  rw [he]
  exact isCompact_Icc.inter_right (isClosed_le (continuous_apply 1) (continuous_apply 0))
source

These are operator-action approximation results; no coefficient-norm or inverse-solver convergence is asserted.

For \(a,b{\gt}-1\), the affine Jacobi measure has strictly positive polynomial square integrals, and its normalized shifted Jacobi polynomials form a Hilbert basis of real \(L^2\). The normalization is the reciprocal positive square root of the squared polynomial norm. In particular, \(\mu _{0,0}^{\mathrm{unit}}=2\, dx|_{[0,1]}\); the affine measure preserves the original mass rather than being normalized to probability.

Lean Formalisation
theorem Polynomial.hasPositiveDefiniteIntegral_unitJacobiMeasure {α β : ℝ} (hα : -1 < α) (hβ : -1 < β) :
  Polynomial.HasPositiveDefiniteIntegral (Polynomial.unitJacobiMeasure α β)
Lean proof
/-- Strict positivity of polynomial squares for the affine Jacobi measure. -/
@[aesop (rule_sets := [PolynomialIntegrability]) unsafe 80% apply]
theorem hasPositiveDefiniteIntegral_unitJacobiMeasure {α β : ℝ}
    (hα : -1 < α) (hβ : -1 < β) : HasPositiveDefiniteIntegral (unitJacobiMeasure α β) := by
  apply HasPositiveDefiniteIntegral.of_positive
  intro p hp
  let q : ℝ[X] := p.comp ((X+1)*C (1/2))
  have hq : q ≠ 0 := by
    intro hz
    apply hp
    apply Polynomial.funext
    intro x
    have he := congrArg (fun r : ℝ[X] ↦ r.eval (2*x-1)) hz
    simpa only [q, eval_comp, eval_mul, eval_add, eval_X, eval_one, eval_C, eval_zero,
      show (2*x-1+1)*(1/2 : ℝ)=x by ring] using he
  have h := hasPositiveDefiniteIntegral_jacobiMeasure hα hβ q hq
  rw [integral_unitJacobiMeasure α β ⟨fun x ↦ p.eval x ^ 2,
    hasFiniteMoments_unitJacobiMeasure hα hβ p⟩]
  simpa [q, eval_comp, div_eq_mul_inv] using h
source

For any measure, an almost-everywhere bound \(|k|\le M\), \(M\ge 0\), gives bounded multiplication on real \(L^2\) with norm at most \(M\). Let \(\mu ,\nu \) be finite measures and let \(k\) be an almost-everywhere strongly measurable real kernel with \(|k|\le M\) on their product. There is a bounded operator \(T:L^2(\nu )\to L^2(\mu )\) such that

\[ \langle g,Tf\rangle =\iint k(x,y)g(x)f(y)\, d\mu (x)d\nu (y),\qquad \| T\| \le M\sqrt{\mu (X)\nu (Y)}. \]

Every displayed pairing is absolutely integrable. The kernel may have either sign.

Lean Formalisation
theorem MeasureTheory.memLp_bounded_mul.{u_1, u_3} {X : Type u_1} [MeasurableSpace X] {𝕜 : Type u_3} [RCLike 𝕜]
  (μ : MeasureTheory.Measure X) (k : X → 𝕜) (hk : MeasureTheory.AEStronglyMeasurable k μ) {M : ℝ}
  (hb : ∀ᵐ (x : X) ∂μ, ‖k x‖ ≤ M) (u : ↥(MeasureTheory.Lp 𝕜 2 μ)) : MeasureTheory.MemLp (fun x => k x * ↑↑u x) 2 μ
Lean proof
/-- A bounded measurable multiplier preserves L². -/
theorem memLp_bounded_mul (μ : Measure X) (k : X → 𝕜) (hk : AEStronglyMeasurable k μ)
    {M : ℝ} (hb : ∀ᵐ x ∂μ, ‖k x‖ ≤ M) (u : Lp 𝕜 2 μ) :
    MemLp (fun x ↦ k x * u x) 2 μ := by
  apply (Lp.memLp u).of_le_mul (c := M) (hk.mul (Lp.aestronglyMeasurable u))
  filter_upwards [hb] with x hx
  rw [Pi.mul_apply, norm_mul]
  exact mul_le_mul_of_nonneg_right hx (norm_nonneg _)
source
Theorem 6.1.27 Integrable Volterra rows from square-integrable inputs
✓ 🤖

For \(\mu =2\, dx|_{[0,1]}\), every \(f\in L^2(\mu )\) is integrable on \([0,1]\). For every kernel \(K\) continuous on \(\Delta \) and \(x\in [0,1]\), the product \(y\mapsto K(x,y)f(y)\) is integrable between \(0\) and \(x\).

Lean Formalisation
theorem Real.integrableOn_coe_unitLegendreLp (f : ↥(MeasureTheory.Lp ℝ 2 (Polynomial.unitJacobiMeasure 0 0))) :
  MeasureTheory.IntegrableOn (fun y => ↑↑f y) (Set.Icc 0 1) MeasureTheory.volume
Lean proof
/-- L² data for the affine Legendre measure are integrable on the physical interval. -/
theorem integrableOn_coe_unitLegendreLp (f : Lp ℝ 2 (unitJacobiMeasure 0 0)) :
    IntegrableOn (fun y ↦ f y) (Icc (0 : ℝ) 1) := by
  have hi := (Lp.memLp f).integrable (by norm_num : (1 : ℝ≥0∞) ≤ 2)
  conv at hi => arg 2; rw [unitJacobiMeasure_zero_zero]
  exact (integrable_smul_measure (by norm_num : (2 : ℝ≥0∞) ≠ 0) (by norm_num)).mp hi
source

Let \(K\) be continuous on the physical triangle \(\Delta \), with \(|K|\le M\), \(M\ge 0\), and put \(\mu =2\, dx|_{[0,1]}\). Extend the kernel by zero outside \(0\le y\le x\le 1\), obtaining \(\widetilde K\). The bounded operator \(T_K:L^2(\mu )\to L^2(\mu )\) has norm at most \(M\) and satisfies

\[ \langle g,T_Kf\rangle =\tfrac 12\iint \widetilde K(x,y)g(x)f(y)\, d\mu (x)d\mu (y) =\int _{[0,1]} g(x)V_Kf(x)\, d\mu (x). \]

The double pairing is absolutely integrable for every \(f,g\in L^2(\mu )\). For \(x\in [0,1]\), the row integral against \(\mu \) is \(2V_Kf(x)\).

Lean Formalisation
theorem Real.measurable_volterraL2Kernel {K : (Fin 2 → ℝ) → ℝ} (hK : ContinuousOn K Real.volterraTriangle) :
  Measurable (Real.volterraL2Kernel K)
Lean proof
/-- Continuity on the triangle suffices for measurability of the zero extension. -/
theorem measurable_volterraL2Kernel {K : (Fin 2 → ℝ) → ℝ}
    (hK : ContinuousOn K volterraTriangle) : Measurable (volterraL2Kernel K) := by
  apply ContinuousOn.measurable_piecewise
    (f := fun z : ℝ × ℝ ↦ K ![z.1,z.2]) (g := fun _ ↦ (0 : ℝ))
    (s := {z : ℝ × ℝ | z.1 ∈ Icc (0 : ℝ) 1 ∧ z.2 ∈ Icc 0 z.1})
  · exact hK.comp (by fun_prop) (fun z hz ↦ hz)
  · fun_prop
  · exact (measurableSet_Icc.preimage measurable_fst).inter
      ((measurableSet_le measurable_const measurable_snd).inter
        (measurableSet_le measurable_snd measurable_fst))
source

For \(x\in [0,1]\), the row integral against \(\mu \) is \(2V_Kf(x)\), explaining the factor \(1/2\) in the operator construction.

Reference details: Volterra coefficient-section convergence and related results

Use the normalized shifted Legendre Hilbert basis of \(L^2(\mu )\), with coordinate isometry \(U\). Then \(A_K=UT_KU^{-1}\) satisfies \(A_K(Uf)=U(T_Kf)\), \(\| A_K\| \le M\), and

\[ P_NA_KP_Nc\longrightarrow A_Kc\quad \hbox{in }\ell ^2 \qquad (c\in \ell ^2). \]

Every continuous triangle kernel admits a finite bound \(M\) and hence these realizations.

Lean Formalisation
theorem Real.norm_volterraL2CoefficientOperator_le {K : (Fin 2 → ℝ) → ℝ} (hK : ContinuousOn K Real.volterraTriangle) {M : ℝ}
  (hM : 0 ≤ M) (hb : ∀ z ∈ Real.volterraTriangle, |K z| ≤ M) : ‖Real.volterraL2CoefficientOperator hK hM hb‖ ≤ M
Lean proof
/-- Coordinate transport preserves the physical Volterra norm bound. -/
theorem norm_volterraL2CoefficientOperator_le : ‖volterraL2CoefficientOperator hK hM hb‖ ≤ M := by
  rw [volterraL2CoefficientOperator, HilbertBasis.norm_coefficientOperator]
  exact norm_volterraL2Operator_le hK hM hb
source

Operator-norm convergence and second-kind solves are given in Theorems 6.1.36 and 6.1.44.

For a polynomial kernel \(K\) and finite shifted-Jacobi input \(p=\sum _n c_nP_n^{(1,0)}(2x-1)\), form

\[ q(x)=x\sum _j(B_Kc)_jP_j^{(1,0)}(1-2x),\qquad B_K=D M_K E. \]

The polynomial \(q\) evaluates to \(V_Kp\) and its \(L^2(\mu )\) class is exactly \(T_K[p]\). Thus \(A_K(U[p])=U[q]\). More generally, any polynomial identity \(V_Kp=q\) on \([0,1]\) identifies the bounded operator’s polynomial output. The normalized shifted Legendre coordinates \(U\) describe the physical output; they are distinct from the unscaled shifted-Jacobi coordinates inside \(B_K\).

Lean Formalisation
theorem Real.volterraL2Operator_polynomial {K : (Fin 2 → ℝ) → ℝ} (hK : ContinuousOn K Real.volterraTriangle) {M : ℝ}
  (hM : 0 ≤ M) (hb : ∀ z ∈ Real.volterraTriangle, |K z| ≤ M) (p q : Polynomial ℝ)
  (hq :
    ∀ (x : ↑(Set.Icc 0 1)),
      Real.volterraIntegral (Real.VolterraIntegralInput.ofContinuous hK ⋯ x) = Polynomial.eval (↑x) q) :
  (Real.volterraL2Operator hK hM hb) ((Polynomial.polynomialToL2 ⋯) p) = (Polynomial.polynomialToL2 ⋯) q
Lean proof
/-- A physical polynomial integral identity identifies the L² output exactly. -/
theorem volterraL2Operator_polynomial {K : (Fin 2 → ℝ) → ℝ}
    (hK : ContinuousOn K volterraTriangle) {M : ℝ} (hM : 0 ≤ M)
    (hb : ∀ z ∈ volterraTriangle, |K z| ≤ M) (p q : ℝ[X])
    (hq : ∀ x : Icc (0 : ℝ) 1,
      volterraIntegral (.ofContinuous hK p.continuous.continuousOn x) = q.eval (x : ℝ)) :
    volterraL2Operator hK hM hb
      (polynomialToL2 (hasFiniteMoments_unitJacobiMeasure (by norm_num) (by norm_num)) p) =
      polynomialToL2 (hasFiniteMoments_unitJacobiMeasure (by norm_num) (by norm_num)) q := by
  let hm := hasFiniteMoments_unitJacobiMeasure (by norm_num : (-1 : ℝ) < 0)
    (by norm_num : (-1 : ℝ) < 0)
  apply ext_inner_left ℝ
  intro g
  have hp := (Measure.quasiMeasurePreserving_snd (μ := unitJacobiMeasure 0 0)
    (ν := unitJacobiMeasure 0 0)).ae_eq_comp (coe_polynomialToL2 hm p)
  have he : (fun z : ℝ × ℝ ↦ volterraL2Kernel K z * (g z.1 * polynomialToL2 hm p z.2)) =ᵐ[(unitJacobiMeasure 0 0).prod (unitJacobiMeasure 0 0)]
      (fun z ↦ volterraL2Kernel K z * (g z.1*p.eval z.2)) := by
    filter_upwards [hp] with z hz
    simp only [Function.comp_apply] at hz
    rw [hz]
  have hi := (integrable_volterraL2_pair hK hM hb (polynomialToL2 hm p) g).congr he
  rw [inner_volterraL2Operator, integral_congr_ae he, integral_prod _ hi, ← integral_const_mul,
    L2.inner_def]
  apply integral_congr_ae
  filter_upwards [ae_mem_Icc_unitJacobiMeasure 0 0, coe_polynomialToL2 hm q] with x hx hqx
  simp_rw [show ∀ y, volterraL2Kernel K (x,y)*(g x*p.eval y) =
    g x*(volterraL2Kernel K (x,y)*p.eval y) by intro y; ring]
  rw [integral_const_mul, integral_volterraL2Kernel K (fun y ↦ p.eval y) ⟨x,hx⟩
    (intervalIntegrable_volterra hK p.continuous.continuousOn hx)]
  rw [show volterraIntegral (.ofKernel K (fun y ↦ p.eval y)
      (intervalIntegrable_volterra hK p.continuous.continuousOn hx)) = q.eval x from
    hq ⟨x,hx⟩]
  simp only [Real.inner_apply, hqx]
  ring
source

For continuous triangle kernels \(K,L\), with finite nonnegative bounds as above, \(T_K-T_L=T_{K-L}\). If \(|K-L|\le \delta \) on \(\Delta \), \(\delta \ge 0\), then \(\| T_K-T_L\| \le \delta \). Every continuous \(K\) therefore admits polynomial kernels \(p\) with \(\| T_p-T_K\| {\lt}\varepsilon \), for any \(\varepsilon {\gt}0\). More generally, uniform kernel error bounds tending to zero imply convergence of the corresponding physical operators in operator norm.

Lean Formalisation
theorem Real.volterraL2Operator_sub {K L : (Fin 2 → ℝ) → ℝ} (hK : ContinuousOn K Real.volterraTriangle)
  (hL : ContinuousOn L Real.volterraTriangle) {M N δ : ℝ} (hM : 0 ≤ M) (hN : 0 ≤ N)
  (bK : ∀ z ∈ Real.volterraTriangle, |K z| ≤ M) (bL : ∀ z ∈ Real.volterraTriangle, |L z| ≤ N) (hδ : 0 ≤ δ)
  (hKL : ∀ z ∈ Real.volterraTriangle, |K z - L z| ≤ δ) :
  Real.volterraL2Operator hK hM bK - Real.volterraL2Operator hL hN bL = Real.volterraL2Operator ⋯ hδ hKL
Lean proof
/-- Subtracting physical kernels subtracts their bounded L² realizations. -/
theorem volterraL2Operator_sub :
    volterraL2Operator hK hM bK - volterraL2Operator hL hN bL =
      volterraL2Operator (hK.sub hL) hδ hKL := by
  apply ContinuousLinearMap.ext
  intro f
  apply ext_inner_left ℝ
  intro g
  rw [sub_apply, inner_sub_right]
  simp only [inner_volterraL2Operator]
  rw [← mul_sub, ← integral_sub (integrable_volterraL2_pair hK hM bK f g)
    (integrable_volterraL2_pair hL hN bL f g)]
  congr 1
  apply integral_congr_ae
  filter_upwards [] with z
  simp only [volterraL2Kernel, Pi.sub_apply]
  split_ifs <;> ring
source
Theorem 6.1.32 Dominated convergence of real L² classes
✓ 🤖

For real \(L^2\) representatives, \(\| f\| _2^2=\int f^2\, d\mu \). Let \(f_i,g\in L^2(\mu )\), with \(f_i\to g\) almost everywhere along a countably generated filter. If \(|f_i-g|\le B\) almost everywhere for every \(i\), and \(B^2\) is integrable, then \([f_i]\to [g]\) in \(L^2\) norm.

Lean Formalisation
theorem MeasureTheory.L2.norm_sq_eq_integral_sq.{u_1} {X : Type u_1} [MeasurableSpace X] {μ : MeasureTheory.Measure X}
  (f : ↥(MeasureTheory.Lp ℝ 2 μ)) : ‖f‖ ^ 2 = ∫ (x : X), ↑↑f x ^ 2 ∂μ
Lean proof
/-- The squared norm of an L² class is the integral of the squared representative. -/
theorem L2.norm_sq_eq_integral_sq (f : Lp ℝ 2 μ) :
    ‖f‖ ^ 2 = ∫ x, (f x) ^ 2 ∂μ := by
  rw [← real_inner_self_eq_norm_sq, L2.inner_def]
  simp only [Real.inner_apply, pow_two]
source

On real or complex \(\ell ^2\), the initial coordinate maps \(P_N\) are compact, self-adjoint projections. If \(A\) is compact, its adjoint is compact and

\[ P_NA\to A,\qquad AP_N\to A,\qquad P_NAP_N\to A \quad \hbox{in operator norm}. \]
Lean Formalisation
theorem lp.isCompactOperator_initialL2Projection.{u_1} {𝕜 : Type u_1} [RCLike 𝕜] (N : ℕ) :
  IsCompactOperator ⇑(lp.initialL2Projection N)
Lean proof
/-- Initial coordinate projections have finite rank and are compact. -/
theorem isCompactOperator_initialL2Projection (N : ℕ) :
    IsCompactOperator (initialL2Projection (𝕜 := 𝕜) N) := by
  unfold initialL2Projection
  have h (s : Finset ℕ) : IsCompactOperator
      (∑ i ∈ s, (singleContinuousLinearMap 𝕜 (fun _ : ℕ ↦ 𝕜) 2 i).comp
        (evalCLM 𝕜 (fun _ : ℕ ↦ 𝕜) 2 i) :
        lp (fun _ : ℕ ↦ 𝕜) 2 →L[𝕜] lp (fun _ : ℕ ↦ 𝕜) 2) := by
    induction s using Finset.induction_on with
    | empty => simpa using (isCompactOperator_zero :
        IsCompactOperator (0 : lp (fun _ : ℕ ↦ 𝕜) 2 →L[𝕜] lp (fun _ : ℕ ↦ 𝕜) 2))
    | @insert i s hi ih =>
      rw [Finset.sum_insert hi]
      exact ((isCompactOperator_of_locallyCompactSpace_rng
        (singleContinuousLinearMap 𝕜 (fun _ : ℕ ↦ 𝕜) 2 i)).comp_clm _).add ih
  exact h _
source
Theorem 6.1.34 Compactness from continuous Hilbert-space rows
✓ 🤖

Let \(\mu \) be a finite measure supported almost everywhere on a compact set \(S\), and let \(T:\ell ^2(\mathbb R)\to L^2(\mu )\) be bounded. Suppose \(r:S\to \ell ^2(\mathbb R)\) is continuous and \((Tf)(x)=\langle r(x),f\rangle \) almost everywhere, for every \(f\). Then \(T\) is compact.

Lean Formalisation
theorem MeasureTheory.isCompactOperator_of_continuous_L2_rows.{u_1} {X : Type u_1} [MeasurableSpace X] [TopologicalSpace X]
  (μ : MeasureTheory.Measure X) [MeasureTheory.IsFiniteMeasure μ]
  (T : ↥(lp (fun x => ℝ) 2) →L[ℝ] ↥(MeasureTheory.Lp ℝ 2 μ)) (r : X → ↥(lp (fun x => ℝ) 2)) {S : Set X}
  (hS : IsCompact S) (hr : ContinuousOn r S) (hs : ∀ᵐ (x : X) ∂μ, x ∈ S)
  (hT : ∀ (f : ↥(lp (fun x => ℝ) 2)), ↑↑(T f) =ᵐ[μ] fun x => inner ℝ (r x) f) : IsCompactOperator ⇑T
Lean proof
/-- An L² operator with continuous coefficient-space rows on compact support is compact. -/
theorem isCompactOperator_of_continuous_L2_rows
    (T : lp (fun _ : ℕ ↦ ℝ) 2 →L[ℝ] Lp ℝ 2 μ)
    (r : X → lp (fun _ : ℕ ↦ ℝ) 2) {S : Set X}
    (hS : IsCompact S) (hr : ContinuousOn r S) (hs : ∀ᵐ x ∂μ, x ∈ S)
    (hT : ∀ f, T f =ᵐ[μ] fun x ↦ ⟪r x, f⟫_ℝ) : IsCompactOperator T := by
  apply isClosed_setOfPred_isCompactOperator.closure_subset
  rw [Metric.mem_closure_iff]
  intro ε hε
  let c : ℝ := (measureUnivNNReal μ : ℝ) ^ (2 : ℝ≥0∞).toReal⁻¹
  have hc : 0 ≤ c := Real.rpow_nonneg (by positivity) _
  let δ := ε / (c + 1)
  have hd : 0 < δ := div_pos hε (by positivity)
  have hu := tendstoUniformlyOn_of_strongly_tendsto_id
    (lp.initialL2Projection (𝕜 := ℝ)) lp.norm_initialL2Projection_le
    lp.tendsto_initialL2Projection (hS.image_of_continuousOn hr)
  obtain ⟨N, hN⟩ := eventually_atTop.1 (Metric.tendstoUniformlyOn_iff.mp hu δ hd)
  refine ⟨T.comp (lp.initialL2Projection N),
    (lp.isCompactOperator_initialL2Projection N).clm_comp T, ?_⟩
  rw [dist_eq_norm, norm_sub_rev]
  have hb : ‖T.comp (lp.initialL2Projection N) - T‖ ≤ c * δ := by
    apply opNorm_le_bound _ (mul_nonneg hc hd.le)
    intro f
    have ha : ∀ᵐ x ∂μ, ‖((T.comp (lp.initialL2Projection N) - T) f) x‖ ≤ δ * ‖f‖ := by
      filter_upwards [hs, hT (lp.initialL2Projection N f), hT f,
        Lp.coeFn_sub (T (lp.initialL2Projection N f)) (T f)] with x hx hp ht he
      change ‖(T (lp.initialL2Projection N f) - T f) x‖ ≤ _
      rw [he, Pi.sub_apply, hp, ht, ← lp.adjoint_initialL2Projection N,
        adjoint_inner_right, ← inner_sub_left]
      apply (norm_inner_le_norm _ _).trans
      apply mul_le_mul_of_nonneg_right _ (norm_nonneg _)
      simpa only [dist_eq_norm, id_eq, norm_sub_rev] using (hN N le_rfl (r x) ⟨x, hx, rfl⟩).le
    simpa only [mul_assoc] using Lp.norm_le_of_ae_bound (mul_nonneg hd.le (norm_nonneg f)) ha
  apply hb.trans_lt
  dsimp only [δ]
  rw [← mul_div_assoc, div_lt_iff₀ (by positivity : 0 < c + 1)]
  nlinarith
source

Under the continuous-kernel hypotheses above, put \(r_x=[y\mapsto \widetilde K(x,y)]\in L^2(\mu )\), \(\mu =2\, dx|_{[0,1]}\). Every row is square integrable, \(\| r_x\| \le \sqrt2 M\), and

\[ \langle r_x,f\rangle =\int \widetilde K(x,y)f(y)\, d\mu (y),\qquad T_Kf(x)=\tfrac 12\langle r_x,f\rangle \quad \hbox{almost everywhere}. \]

The row pairing belongs to \(L^2(\mu )\) for every \(f\in L^2(\mu )\), and \(x\mapsto r_x\) is continuous on the closed unit interval in \(L^2\) norm.

Lean Formalisation
theorem Real.memLp_volterraL2Kernel_row {K : (Fin 2 → ℝ) → ℝ} (hK : ContinuousOn K Real.volterraTriangle) {M : ℝ} (hM : 0 ≤ M)
  (hb : ∀ z ∈ Real.volterraTriangle, |K z| ≤ M) (x : ℝ) :
  MeasureTheory.MemLp (fun y => Real.volterraL2Kernel K (x, y)) 2 (Polynomial.unitJacobiMeasure 0 0)
Lean proof
/-- Every zero-extended Volterra row belongs to the physical L² space. -/
theorem memLp_volterraL2Kernel_row (x : ℝ) :
    MemLp (fun y ↦ volterraL2Kernel K (x,y)) 2 (unitJacobiMeasure 0 0) :=
  MemLp.of_bound ((measurable_volterraL2Kernel hK).comp
    (measurable_const.prodMk measurable_id)).aestronglyMeasurable M
    (Eventually.of_forall (fun y ↦ norm_volterraL2Kernel_le hM hb (x,y)))
source

For every continuous triangle kernel, \(T_K\) and its normalized shifted Legendre coefficient operator \(A_K\) are compact. Consequently \(\| P_NA_KP_N-A_K\| \to 0\).

Lean Formalisation
theorem Real.isCompactOperator_volterraL2Operator {K : (Fin 2 → ℝ) → ℝ} (hK : ContinuousOn K Real.volterraTriangle) {M : ℝ}
  (hM : 0 ≤ M) (hb : ∀ z ∈ Real.volterraTriangle, |K z| ≤ M) : IsCompactOperator ⇑(Real.volterraL2Operator hK hM hb)
Lean proof
/-- Every continuous triangle kernel gives a compact physical Volterra operator. -/
theorem isCompactOperator_volterraL2Operator :
    IsCompactOperator (volterraL2Operator hK hM hb) := by
  let b := hilbertBasisShiftedJacobi (by norm_num : (-1 : ℝ) < 0)
    (by norm_num : (-1 : ℝ) < 0)
  let S := (volterraL2Operator hK hM hb).comp
    b.repr.symm.toContinuousLinearEquiv.toContinuousLinearMap
  have hc : IsCompactOperator S := by
    apply isCompactOperator_of_continuous_L2_rows (unitJacobiMeasure 0 0) S
      (fun x ↦ (1/2 : ℝ) • b.repr (volterraL2Row hK hM hb x)) isCompact_Icc
    · exact (b.repr.continuous.comp_continuousOn
        (continuousOn_volterraL2Row hK hM hb)).const_smul (1/2 : ℝ)
    · exact ae_mem_Icc_unitJacobiMeasure 0 0
    · intro f
      filter_upwards [volterraL2Operator_ae_inner_row hK hM hb (b.repr.symm f)] with x hx
      change volterraL2Operator hK hM hb (b.repr.symm f) x = _
      rw [hx, real_inner_smul_left]
      congr 1
      rw [← b.repr.inner_map_map, LinearIsometryEquiv.apply_symm_apply]
  have he : S.comp b.repr.toContinuousLinearEquiv.toContinuousLinearMap =
      volterraL2Operator hK hM hb := by
    apply ContinuousLinearMap.ext
    intro f
    change volterraL2Operator hK hM hb (b.repr.symm (b.repr f)) = _
    rw [LinearIsometryEquiv.symm_apply_apply]
  rw [← he]
  exact hc.comp_clm _
source
Reference details: Resolvents from summable or factorially bounded iterates

For a bounded operator \(T\) on a real or complex Banach space, summability of \(\sum _{n\ge 0}T^n\) implies invertibility of \(I-T\), with inverse that series. Every right-hand side has a unique solution of \(u-Tu=f\). A bound \(\| T^n\| \le C M^n/n!\) for all \(n\) suffices for summability. No assumption \(\| T\| {\lt}1\) is required.

Lean Formalisation
theorem ContinuousLinearMap.summable_pow_of_factorial_bound.{u_1, u_2} {𝕜 : Type u_1} {E : Type u_2} [RCLike 𝕜]
  [NormedAddCommGroup E] [NormedSpace 𝕜 E] [CompleteSpace E] (T : E →L[𝕜] E) {C M : ℝ}
  (h : ∀ (n : ℕ), ‖T ^ n‖ ≤ C * (M ^ n / ↑n.factorial)) : Summable fun n => T ^ n
Lean proof
/-- A factorial bound on powers makes the operator Neumann series summable. -/
theorem summable_pow_of_factorial_bound (T : E →L[𝕜] E) {C M : ℝ}
    (h : ∀ n : ℕ, ‖T ^ n‖ ≤ C * (M ^ n / n.factorial)) :
    Summable (fun n : ℕ ↦ T ^ n) :=
  Summable.of_norm_bounded ((Real.summable_pow_div_factorial M).mul_left C) h
source

For \(|K|\le M\) on \(\Delta \), \(M\ge 0\), and \(n\ge 0\),

\[ |T_K^{n+1}f(x)|\le \frac{\| f\| _{L^2(\mu )}}{\sqrt2} \frac{M^{n+1}x^n}{n!}\quad \hbox{almost everywhere}, \qquad \| T_K^{n+1}\| \le \frac{M^{n+1}}{n!}. \]

More generally, an almost-everywhere majorant \(|f(x)|\le Cx^n\), \(C\ge 0\), gives \(|T_Kf(x)|\le MCx^{n+1}/(n+1)\) almost everywhere. The series of powers is norm summable; \(I-T_K\) is invertible and \(u-T_Ku=f\) has exactly one \(L^2(\mu )\) solution for each \(f\).

Lean Formalisation
theorem Real.volterraL2Operator_ae_bound_of_power {K : (Fin 2 → ℝ) → ℝ} (hK : ContinuousOn K Real.volterraTriangle) {M : ℝ}
  (hM : 0 ≤ M) (hb : ∀ z ∈ Real.volterraTriangle, |K z| ≤ M)
  (f : ↥(MeasureTheory.Lp ℝ 2 (Polynomial.unitJacobiMeasure 0 0))) {C : ℝ} (_hC : 0 ≤ C) (n : ℕ)
  (hf : ∀ᵐ (y : ℝ) ∂Polynomial.unitJacobiMeasure 0 0, |↑↑f y| ≤ C * y ^ n) :
  ∀ᵐ (x : ℝ) ∂Polynomial.unitJacobiMeasure 0 0,
    |↑↑((Real.volterraL2Operator hK hM hb) f) x| ≤ M * C * x ^ (n + 1) / (↑n + 1)
Lean proof
/-- One Volterra application integrates a power majorant, gaining its next denominator. -/
theorem volterraL2Operator_ae_bound_of_power
    (f : Lp ℝ 2 (unitJacobiMeasure 0 0)) {C : ℝ} (_hC : 0 ≤ C) (n : ℕ)
    (hf : ∀ᵐ y ∂unitJacobiMeasure 0 0, |f y| ≤ C * y ^ n) :
    ∀ᵐ x ∂unitJacobiMeasure 0 0,
      |volterraL2Operator hK hM hb f x| ≤ M * C * x ^ (n+1) / (n+1) := by
  filter_upwards [volterraL2Operator_ae_inner_row hK hM hb f,
    ae_mem_Icc_unitJacobiMeasure 0 0] with x hx hs
  rw [hx, abs_mul, abs_of_nonneg (by norm_num : (0 : ℝ) ≤ 1/2), inner_volterraL2Row]
  have he : (fun y ↦ volterraL2Kernel K (x,y) * f y) =
      (Icc 0 x).indicator (fun y ↦ K ![x,y] * f y) := by
    funext y
    simp [volterraL2Kernel, hs, Set.indicator_apply]
  rw [he, integral_indicator measurableSet_Icc]
  have hi : IntegrableOn (fun y : ℝ ↦ M * C * y ^ n) (Icc 0 x) (unitJacobiMeasure 0 0) :=
    (by fun_prop : Continuous (fun y : ℝ ↦ M * C * y ^ n)).continuousOn.integrableOn_compact
      isCompact_Icc
  have ha : ∀ᵐ y ∂(unitJacobiMeasure 0 0).restrict (Icc 0 x),
      ‖K ![x,y] * f y‖ ≤ M * C * y ^ n := by
    filter_upwards [ae_restrict_of_ae hf, ae_restrict_mem measurableSet_Icc] with y hy hyx
    rw [norm_mul]
    exact (mul_le_mul (hb _ ⟨hs, hyx⟩) hy (abs_nonneg _) hM).trans_eq (by ring)
  have hm : AEStronglyMeasurable (fun y ↦ K ![x,y] * f y)
      ((unitJacobiMeasure 0 0).restrict (Icc 0 x)) := by
    apply AEStronglyMeasurable.mul
    · exact (hK.comp (by fun_prop) (fun y hy ↦ ⟨hs, hy⟩)).aestronglyMeasurable measurableSet_Icc
    · exact (Lp.memLp f).aestronglyMeasurable.restrict
  have hi' := hi.mono' hm ha
  have hn := (norm_integral_le_integral_norm (fun y ↦ K ![x,y] * f y)
    (μ := (unitJacobiMeasure 0 0).restrict (Icc 0 x))).trans
      (integral_mono_ae hi'.norm hi ha)
  rw [integral_const_mul, integral_unitJacobi_pow hs n] at hn
  have hh := mul_le_mul_of_nonneg_left hn (by norm_num : (0 : ℝ) ≤ 1/2)
  convert hh using 1
  ring
source
Reference details: Invertibility in normalized Volterra coordinates and related results
Theorem 6.1.39 Invertibility in normalized Volterra coordinates
✓ 🤖

For a continuous kernel on the closed Volterra triangle, the normalized coefficient operator \(I-A_K\) is invertible.

Lean Formalisation
theorem Real.isUnit_one_sub_volterraL2CoefficientOperator {K : (Fin 2 → ℝ) → ℝ} (hK : ContinuousOn K Real.volterraTriangle)
  {M : ℝ} (hM : 0 ≤ M) (hb : ∀ z ∈ Real.volterraTriangle, |K z| ≤ M) :
  IsUnit (1 - Real.volterraL2CoefficientOperator hK hM hb)
Lean proof
/-- Normalized coefficient coordinates preserve second-kind invertibility. -/
theorem isUnit_one_sub_volterraL2CoefficientOperator :
    IsUnit (1 - volterraL2CoefficientOperator hK hM hb) := by
  let b := hilbertBasisShiftedJacobi (by norm_num : (-1 : ℝ) < 0)
    (by norm_num : (-1 : ℝ) < 0)
  have h := (isUnit_one_sub_volterraL2Operator hK hM hb).map
    b.repr.toContinuousLinearEquiv.conjContinuousAlgEquiv.toAlgEquiv.toMonoidHom
  change IsUnit (b.repr.toContinuousLinearEquiv.conjContinuousAlgEquiv
    (1 - volterraL2Operator hK hM hb)) at h
  rw [map_sub, map_one] at h
  exact h
source
Definition 6.1.40 Second-kind Volterra coefficient inverse
✓ 🤖
#

For a continuous kernel \(K\) on the closed Volterra triangle, define \(R_K=(I-A_K)^{-1}\) on \(\ell ^2\).

Lean Formalisation
def Real.volterraCoefficientInverse {K : (Fin 2 → ℝ) → ℝ} (hK : ContinuousOn K Real.volterraTriangle) {M : ℝ} (hM : 0 ≤ M)
  (hb : ∀ z ∈ Real.volterraTriangle, |K z| ≤ M) : ↥(lp (fun x => ℝ) 2) →L[ℝ] ↥(lp (fun x => ℝ) 2)
Lean definition
/-- The classical inverse of the second-kind normalized coefficient operator. -/
def volterraCoefficientInverse :
    lp (fun _ : ℕ ↦ ℝ) 2 →L[ℝ] lp (fun _ : ℕ ↦ ℝ) 2 :=
  ↑((isUnit_one_sub_volterraL2CoefficientOperator hK hM hb).unit⁻¹)
source
Theorem 6.1.41 Characterization of the Volterra coefficient inverse
✓ 🤖

The coefficient inverse satisfies \(R_K(I-A_K)=I\) and \((I-A_K)R_K=I\).

Lean Formalisation
theorem Real.volterraCoefficientInverse_mul {K : (Fin 2 → ℝ) → ℝ} (hK : ContinuousOn K Real.volterraTriangle) {M : ℝ}
  (hM : 0 ≤ M) (hb : ∀ z ∈ Real.volterraTriangle, |K z| ≤ M) :
  Real.volterraCoefficientInverse hK hM hb * (1 - Real.volterraL2CoefficientOperator hK hM hb) = 1 ∧
    (1 - Real.volterraL2CoefficientOperator hK hM hb) * Real.volterraCoefficientInverse hK hM hb = 1
Lean proof
/-- The inverse has the two defining operator identities. -/
theorem volterraCoefficientInverse_mul :
    volterraCoefficientInverse hK hM hb * (1 - volterraL2CoefficientOperator hK hM hb) = 1 ∧
      (1 - volterraL2CoefficientOperator hK hM hb) * volterraCoefficientInverse hK hM hb = 1 := by
  exact ⟨by simpa only [volterraCoefficientInverse, IsUnit.unit_spec] using
      Units.inv_mul (isUnit_one_sub_volterraL2CoefficientOperator hK hM hb).unit,
    by simpa only [volterraCoefficientInverse, IsUnit.unit_spec] using
      Units.mul_inv (isUnit_one_sub_volterraL2CoefficientOperator hK hM hb).unit⟩
source
Definition 6.1.42 Lifted second-kind Volterra sections
✓ 🤖

For a continuous kernel \(K\) and a natural cutoff \(N\), put \(B_{K,N}=I-P_NA_K\) on normalized coefficient space.

Lean Formalisation
def Real.volterraCoefficientSection {K : (Fin 2 → ℝ) → ℝ} (hK : ContinuousOn K Real.volterraTriangle) {M : ℝ} (hM : 0 ≤ M)
  (hb : ∀ z ∈ Real.volterraTriangle, |K z| ≤ M) (N : ℕ) : ↥(lp (fun x => ℝ) 2) →L[ℝ] ↥(lp (fun x => ℝ) 2)
Lean definition
/-- Lifted normalized finite-section equations retain the identity on unresolved rows. -/
def volterraCoefficientSection (N : ℕ) :
    lp (fun _ : ℕ ↦ ℝ) 2 →L[ℝ] lp (fun _ : ℕ ↦ ℝ) 2 :=
  liftedFiniteSection (lp.initialL2Projection N) (-volterraL2CoefficientOperator hK hM hb)
source
Theorem 6.1.43 Action of lifted Volterra sections
✓ 🤖

For every \(u\in \ell ^2\), \(B_{K,N}u=u-P_NA_Ku\).

Lean Formalisation
theorem Real.volterraCoefficientSection_apply {K : (Fin 2 → ℝ) → ℝ} (hK : ContinuousOn K Real.volterraTriangle) {M : ℝ}
  (hM : 0 ≤ M) (hb : ∀ z ∈ Real.volterraTriangle, |K z| ≤ M) (N : ℕ) (u : ↥(lp (fun x => ℝ) 2)) :
  (Real.volterraCoefficientSection hK hM hb N) u =
    u - (lp.initialL2Projection N) ((Real.volterraL2CoefficientOperator hK hM hb) u)
Lean proof
/-- The lifted section keeps the identity on unresolved output coordinates. -/
theorem volterraCoefficientSection_apply (N : ℕ) (u : lp (fun _ : ℕ ↦ ℝ) 2) :
    volterraCoefficientSection hK hM hb N u =
      u - lp.initialL2Projection N (volterraL2CoefficientOperator hK hM hb u) := by
  simp only [volterraCoefficientSection, liftedFiniteSection, add_apply, one_apply_eq_self,
    comp_apply, _root_.neg_apply, map_neg, sub_eq_add_neg]
source

Let \(A=A_K\) and \(B_N=I-P_NA\). The operator \(I-A\) is invertible. For sufficiently large \(N\), \(B_N\) is invertible with \(\| B_N^{-1}\| \le \| (I-A)^{-1}\| +1\). For every \(f\in \ell ^2\), the finite system has exactly one solution

\[ u_N\in \operatorname {ran}P_N,\qquad P_N(I-A)u_N=P_Nf. \]

For every cutoff \(N\) at which \(B_N\) is invertible, the solution is \(u_N=B_N^{-1}P_Nf\). Such cutoffs include every sufficiently large \(N\). As \(N\to \infty \) through these cutoffs, \(u_N\) converges in \(\ell ^2\) to \(u=(I-A)^{-1}f\). Eventually, for every exact solution \(u\),

\[ \| B_N^{-1}P_N(I-A)u-u\| \le (\| (I-A)^{-1}\| +1)\| P_Nu-u\| . \]

On \(\operatorname {ran}P_N\), the projected equation is precisely the finite matrix equation with \(I-P_NAP_N\). All coordinates here are normalized shifted Legendre coordinates of the physical output.

Lean Formalisation
theorem Real.volterraCoefficientSection_filter_neBot {K : (Fin 2 → ℝ) → ℝ} (hK : ContinuousOn K Real.volterraTriangle) {M : ℝ}
  (hM : 0 ≤ M) (hb : ∀ z ∈ Real.volterraTriangle, |K z| ≤ M) :
  (Ring.invertibleIndexFilter (Real.volterraCoefficientSection hK hM hb) Filter.atTop).NeBot
Lean proof
/-- The domain of invertible second-kind sections is cofinal and nontrivial. -/
theorem volterraCoefficientSection_filter_neBot :
    NeBot (Ring.invertibleIndexFilter (volterraCoefficientSection hK hM hb) atTop) :=
  Ring.invertibleIndexFilter_neBot _ _
    ((eventually_stable_volterraCoefficientSection_ringInverse hK hM hb).mono (fun _ h ↦ h.1))
source
Reference details: Algebraic and normalized shifted Jacobi coordinates and related results

For \(\alpha ,\beta {\gt}-1\), the shifted Jacobi polynomials form an algebraic basis of \(\mathbb R[x]\); synthesis of a polynomial’s finite coordinates recovers that polynomial. Write \(h_j\) for its squared norm in the affine Jacobi measure. The polynomial \(\widehat P_j=h_j^{-1/2}P_j\) represents exactly the \(j\)th vector of the normalized shifted Jacobi Hilbert basis.

Lean Formalisation
theorem Polynomial.shiftedJacobiBasis_apply {α β : ℝ} (hα : -1 < α) (hβ : -1 < β) (n : ℕ) :
  (Polynomial.shiftedJacobiBasis hα hβ) n = Polynomial.shiftedJacobi α β n
Lean proof
/-- Algebraic basis vectors are the existing shifted Jacobi polynomials. -/
@[simp] theorem shiftedJacobiBasis_apply (n : ℕ) :
    shiftedJacobiBasis hα hβ n = shiftedJacobi α β n := by
  exact (shiftedJacobiSequence hα hβ).basis_eq_self _ n
source

Let \(J_N:\mathbb K^N\to \ell ^2\) be zero extension, for \(\mathbb K=\mathbb R\) or \(\mathbb C\). Restriction followed by \(J_N\) is \(P_N\), and \(P_NJ_N=J_N\). For bounded \(T\), define \(G_N(i,j)=(Te_j)_i\), \(0\le i,j{\lt}N\). Then

\[ (G_Nv)_i=(TJ_Nv)_i,\qquad (I-G_N)v=(f_i)_{i{\lt}N} \iff P_N(J_Nv-TJ_Nv)=P_Nf. \]

A unique solution of the projected equation in \(\operatorname {ran}P_N\) gives a unique finite matrix solution.

Lean Formalisation
theorem lp.initialL2Vector_apply.{u_1} {𝕜 : Type u_1} [RCLike 𝕜] {N : ℕ} (v : Fin N → 𝕜) (i : Fin N) :
  ↑(lp.initialL2Vector v) ↑i = v i
Lean proof
/-- Restriction of zero extension recovers each finite coordinate. -/
@[simp] theorem initialL2Vector_apply {N : ℕ} (v : Fin N → 𝕜) (i : Fin N) :
    initialL2Vector v i = v i := by
  classical
  change (lp.evalCLM 𝕜 (fun _ : ℕ ↦ 𝕜) 2 i) (∑ j : Fin N, lp.single 2 (j : ℕ) (v j)) = _
  rw [map_sum]
  change (∑ j : Fin N, (lp.single 2 (j : ℕ) (v j) : lp (fun _ : ℕ ↦ 𝕜) 2) i) = v i
  simp [Pi.single_apply, Fin.val_inj]
source

Let \(P_n\) be contractions on a real or complex Banach space, converging strongly to \(I\), let \(K\) be compact, and suppose \(L_n\to K\) in operator norm. Then \(B_n=I+P_nL_n\to I+K\) in operator norm. If \(I+K\) is invertible, then eventually \(B_n\) is invertible and \(\| B_n^{-1}\| \le \| (I+K)^{-1}\| +1\). For any contraction \(P\) and bounded \(K,L\), whenever \(B=I+PL\) is invertible,

\[ B^{-1}P(I+K)u-u=B^{-1}\bigl(Pu-u+P(K-L)u\bigr), \]
\[ \| B^{-1}P(I+K)u-u\| \le \| B^{-1}\| \bigl(\| Pu-u\| +\| K-L\| \| u\| \bigr). \]

The fixed-section inverse \((I+PL)^{-1}\) is defined for operators \(L\) such that \(I+PL\) is invertible. The indices \(n\) for which \(B_n\) is invertible include every sufficiently large integer. The error identity and estimate do not require compactness.

Lean Formalisation
theorem ContinuousLinearMap.approximateLiftedFiniteSection_filter_neBot.{u_1, u_2} {𝕜 : Type u_1} [RCLike 𝕜] {E : Type u_2}
  [NormedAddCommGroup E] [NormedSpace 𝕜 E] [CompleteSpace E] (P : ℕ → E →L[𝕜] E) (hC : ∀ (n : ℕ), ‖P n‖ ≤ 1)
  (hP : ∀ (x : E), Filter.Tendsto (fun n => (P n) x) Filter.atTop (nhds x)) (K : E →L[𝕜] E) (hK : IsCompactOperator ⇑K)
  (hT : IsUnit (1 + K)) (L : ℕ → E →L[𝕜] E) (hL : Filter.Tendsto L Filter.atTop (nhds K)) :
  (Ring.invertibleIndexFilter (fun n => (P n).liftedFiniteSection (L n)) Filter.atTop).NeBot
Lean proof
/-- Norm-consistent sections have a nontrivial invertible-cutoff filter. -/
theorem approximateLiftedFiniteSection_filter_neBot
    (P : ℕ → E →L[𝕜] E) (hC : ∀ n, ‖P n‖ ≤ 1)
    (hP : ∀ x, Tendsto (fun n ↦ P n x) atTop (𝓝 x))
    (K : E →L[𝕜] E) (hK : IsCompactOperator K) (hT : IsUnit (1 + K))
    (L : ℕ → E →L[𝕜] E) (hL : Tendsto L atTop (𝓝 K)) :
    NeBot (Ring.invertibleIndexFilter (fun n ↦ liftedFiniteSection (P n) (L n)) atTop) :=
  Ring.invertibleIndexFilter_neBot _ _
    ((eventually_stable_approximateLiftedFiniteSection_ringInverse P hC hP K hK hT L hL).mono
      (fun _ h ↦ h.1))
source
Definition 6.1.48 Volterra sections with varying kernels
✓ 🤖

For continuous kernels \(K_n\) on the closed Volterra triangle, define \(B_n=I-P_nA_{K_n}\) on normalized coefficient space.

Lean Formalisation
def Real.approximateVolterraCoefficientSection {Ks : ℕ → (Fin 2 → ℝ) → ℝ}
  (hs : ∀ (n : ℕ), ContinuousOn (Ks n) Real.volterraTriangle) {B : ℕ → ℝ} (hB : ∀ (n : ℕ), 0 ≤ B n)
  (bs : ∀ (n : ℕ), ∀ z ∈ Real.volterraTriangle, |Ks n z| ≤ B n) (N : ℕ) :
  ↥(lp (fun x => ℝ) 2) →L[ℝ] ↥(lp (fun x => ℝ) 2)
Lean definition
/-- The section family for simultaneously varying kernels and cutoffs. -/
def approximateVolterraCoefficientSection (N : ℕ) :
    lp (fun _ : ℕ ↦ ℝ) 2 →L[ℝ] lp (fun _ : ℕ ↦ ℝ) 2 :=
  volterraCoefficientSection (hs N) (hB N) (bs N) N
source
Theorem 6.1.49 Action of varying-kernel Volterra sections
✓ 🤖

For every \(u\in \ell ^2\), \(B_nu=u-P_nA_{K_n}u\).

Lean Formalisation
theorem Real.approximateVolterraCoefficientSection_apply {Ks : ℕ → (Fin 2 → ℝ) → ℝ}
  (hs : ∀ (n : ℕ), ContinuousOn (Ks n) Real.volterraTriangle) {B : ℕ → ℝ} (hB : ∀ (n : ℕ), 0 ≤ B n)
  (bs : ∀ (n : ℕ), ∀ z ∈ Real.volterraTriangle, |Ks n z| ≤ B n) (N : ℕ) (u : ↥(lp (fun x => ℝ) 2)) :
  (Real.approximateVolterraCoefficientSection hs hB bs N) u =
    u - (lp.initialL2Projection N) ((Real.volterraL2CoefficientOperator ⋯ ⋯ ⋯) u)
Lean proof
/-- Each approximate section keeps the identity on unresolved output coordinates. -/
theorem approximateVolterraCoefficientSection_apply (N : ℕ) (u : lp (fun _ : ℕ ↦ ℝ) 2) :
    approximateVolterraCoefficientSection hs hB bs N u =
      u - lp.initialL2Projection N (volterraL2CoefficientOperator (hs N) (hB N) (bs N) u) := by
  simp only [approximateVolterraCoefficientSection, volterraCoefficientSection,
    liftedFiniteSection, add_apply, one_apply_eq_self, comp_apply, _root_.neg_apply, map_neg,
    sub_eq_add_neg]
source

Let \(K,K_n\) be continuous on the closed Volterra triangle, with finite nonnegative uniform bounds, and suppose \(|K_n-K|\le \varepsilon _n\) there, where \(\varepsilon _n\ge 0\) and \(\varepsilon _n\to 0\). In normalized physical coordinates, \(\| A_{K_n}-A_K\| \le \varepsilon _n\). Put \(B_n=I-P_nA_{K_n}\) and \(C=\| (I-A_K)^{-1}\| +1\). Eventually \(B_n\) is invertible with \(\| B_n^{-1}\| \le C\), and for every \(f\in \ell ^2\) the projected system has a unique solution. The invertible-cutoff domain contains a tail, and along its induced nontrivial filter,

\[ B_n^{-1}P_nf\longrightarrow (I-A_K)^{-1}f, \]

and eventually, for every \(u\in \ell ^2\),

\[ \| B_n^{-1}P_n(I-A_K)u-u\| \le C\bigl(\| P_nu-u\| +\varepsilon _n\| u\| \bigr). \]

No smallness restriction on \(K\) or common bound on all \(K_n\) is required.

Lean Formalisation
theorem Real.approximateVolterraSection_filter_neBot {K : (Fin 2 → ℝ) → ℝ} (hK : ContinuousOn K Real.volterraTriangle) {M : ℝ}
  (hM : 0 ≤ M) (bK : ∀ z ∈ Real.volterraTriangle, |K z| ≤ M) {Ks : ℕ → (Fin 2 → ℝ) → ℝ}
  (hs : ∀ (n : ℕ), ContinuousOn (Ks n) Real.volterraTriangle) {B e : ℕ → ℝ} (hB : ∀ (n : ℕ), 0 ≤ B n)
  (bs : ∀ (n : ℕ), ∀ z ∈ Real.volterraTriangle, |Ks n z| ≤ B n) (he : ∀ (n : ℕ), 0 ≤ e n)
  (err : ∀ (n : ℕ), ∀ z ∈ Real.volterraTriangle, |Ks n z - K z| ≤ e n) (hte : Filter.Tendsto e Filter.atTop (nhds 0)) :
  (Ring.invertibleIndexFilter (Real.approximateVolterraCoefficientSection hs hB bs) Filter.atTop).NeBot
Lean proof
/-- The approximate-section limiting filter is nontrivial. -/
theorem approximateVolterraSection_filter_neBot :
    NeBot (Ring.invertibleIndexFilter (approximateVolterraCoefficientSection hs hB bs) atTop) :=
  Ring.invertibleIndexFilter_neBot _ _
    ((eventually_stable_approximateVolterraSection_ringInverse hK hM bK hs hB bs he err hte).mono
      (fun _ h ↦ h.1))
source

For a polynomial kernel \(p\), let \(c_j\) be the finite shifted-Jacobi \((1,0)\) coordinates of the normalized shifted Legendre polynomial \(\widehat P_j\). Let \(q_j\) be the physical polynomial reconstructed from \(D M_p E c_j\), including reflection and multiplication by \(x\). With \(\mu =2\, dx\) on \([0,1]\), define the actual \(N\times N\) matrix

\[ G_{p,N}(i,j)=\int \widehat P_i(x)q_j(x)\, d\mu (x). \]

Then \(G_{p,N}(i,j)=(A_pe_j)_i\); its multiplication is exactly the finite restriction of \(A_pJ_Nv\), and

\[ (I-G_{p,N})v=(f_i)_{i{\lt}N} \iff P_N(J_Nv-A_pJ_Nv)=P_Nf. \]

For all sufficiently large \(N\), this finite matrix equation has exactly one solution for every coefficient right-hand side.

Lean Formalisation
theorem MvPolynomial.volterraProriolMatrix_eq (K : MvPolynomial (Fin 2) ℝ) (N : ℕ) {M : ℝ} (hM : 0 ≤ M)
  (hb : ∀ z ∈ Real.volterraTriangle, |(MvPolynomial.eval z) K| ≤ M) :
  K.volterraProriolMatrix N = lp.initialL2Matrix (Real.volterraL2CoefficientOperator ⋯ hM hb) N
Lean proof
/-- Exact equality of assembled entries and the bounded normalized coefficient matrix. -/
theorem volterraProriolMatrix_eq (K : MvPolynomial (Fin 2) ℝ) (N : ℕ)
    {M : ℝ} (hM : 0 ≤ M) (hb : ∀ z ∈ volterraTriangle, |eval z K| ≤ M) :
    volterraProriolMatrix K N = lp.initialL2Matrix
      (volterraL2CoefficientOperator K.continuous_eval.continuousOn hM hb) N := by
  funext i j
  change Polynomial.integralInner _ (Polynomial.IntegrablePair.of _ _ _ (h := (Polynomial.hasFiniteMoments_unitJacobiMeasure (by norm_num) (by norm_num)).integrable_mul _ _)) =
    (hilbertBasisShiftedJacobi (by norm_num : (-1 : ℝ) < 0)
      (by norm_num : (-1 : ℝ) < 0)).coefficientOperator _ _ _
  rw [HilbertBasis.coefficientOperator_single,
    ← polynomialToL2_normalizedShiftedJacobi, ← polynomialToL2_normalizedShiftedJacobi]
  have he := volterraL2Operator_proriol K (volterraNormalizedInput j) hM hb
  simp only [volterraNormalizedInput, linearCombination_shiftedJacobi_repr] at he
  rw [he, Polynomial.inner_polynomialToL2]
  rfl
source
Definition 6.1.52 Classical assembled Proriol solutions
✓ 🤖

For polynomial kernels \(p_n\), let \(B_n=I-P_nA_{p_n}\). For an invertible cutoff \(n\) and \(f\in \ell ^2\), define \(v_n\) by restricting \(B_n^{-1}P_nf\) to its first \(n\) coordinates.

Lean Formalisation
def MvPolynomial.volterraProriolMatrixSolution (p : ℕ → MvPolynomial (Fin 2) ℝ) {B : ℕ → ℝ} (hB : ∀ (n : ℕ), 0 ≤ B n)
  (bp : ∀ (n : ℕ), ∀ z ∈ Real.volterraTriangle, |(MvPolynomial.eval z) (p n)| ≤ B n) (f : ↥(lp (fun x => ℝ) 2))
  (n : Ring.InvertibleIndex (Real.approximateVolterraCoefficientSection ⋯ hB bp)) : Fin ↑n → ℝ
Lean definition
/-- Finite coordinates of the classical lifted solution at an invertible cutoff. -/
def volterraProriolMatrixSolution (f : lp (fun _ : ℕ ↦ ℝ) 2)
    (n : Ring.InvertibleIndex (approximateVolterraCoefficientSection
      (fun n ↦ (p n).continuous_eval.continuousOn) hB bp)) : Fin n.val → ℝ :=
  fun i ↦ Ring.inverseAt (approximateVolterraCoefficientSection
    (fun n ↦ (p n).continuous_eval.continuousOn) hB bp) n
      (lp.initialL2Projection n.val f) i
source
Theorem 6.1.53 Characterization of assembled Proriol solutions
✓ 🤖

At every invertible cutoff, \(J_nv_n=B_n^{-1}P_nf\) and \((I-G_{p_n,n})v_n=(f_i)_{i{\lt}n}\).

Lean Formalisation
theorem MvPolynomial.volterraProriolMatrixSolution_spec (p : ℕ → MvPolynomial (Fin 2) ℝ) {B : ℕ → ℝ} (hB : ∀ (n : ℕ), 0 ≤ B n)
  (bp : ∀ (n : ℕ), ∀ z ∈ Real.volterraTriangle, |(MvPolynomial.eval z) (p n)| ≤ B n)
  (n : Ring.InvertibleIndex (Real.approximateVolterraCoefficientSection ⋯ hB bp)) (f : ↥(lp (fun x => ℝ) 2)) :
  lp.initialL2Vector (MvPolynomial.volterraProriolMatrixSolution p hB bp f n) =
      (Ring.inverseAt (Real.approximateVolterraCoefficientSection ⋯ hB bp) n) ((lp.initialL2Projection ↑n) f) ∧
    (1 - (p ↑n).volterraProriolMatrix ↑n).mulVec (MvPolynomial.volterraProriolMatrixSolution p hB bp f n) = fun i =>
      ↑f ↑i
Lean proof
/-- At every invertible cutoff, zero extension recovers the lifted solution
and the finite coordinates solve the assembled matrix equation. -/
theorem volterraProriolMatrixSolution_spec
    (n : Ring.InvertibleIndex (approximateVolterraCoefficientSection
      (fun n ↦ (p n).continuous_eval.continuousOn) hB bp))
    (f : lp (fun _ : ℕ ↦ ℝ) 2) :
    lp.initialL2Vector (volterraProriolMatrixSolution p hB bp f n) =
      Ring.inverseAt (approximateVolterraCoefficientSection
        (fun n ↦ (p n).continuous_eval.continuousOn) hB bp) n
        (lp.initialL2Projection n.val f) ∧
    (1 - volterraProriolMatrix (p n.val) n.val) *ᵥ
      volterraProriolMatrixSolution p hB bp f n = (fun i : Fin n.val ↦ f i) := by
  have hs := liftedFiniteSection_solution_mem (lp.initialL2Projection n.val)
    (-volterraL2CoefficientOperator (p n.val).continuous_eval.continuousOn
      (hB n.val) (bp n.val)) (lp.initialL2Projection_idempotent n.val)
    (by simpa only [approximateVolterraCoefficientSection, volterraCoefficientSection]
      using n.property) f
  have hv : lp.initialL2Vector (volterraProriolMatrixSolution p hB bp f n) =
      Ring.inverseAt (approximateVolterraCoefficientSection
        (fun n ↦ (p n).continuous_eval.continuousOn) hB bp) n
        (lp.initialL2Projection n.val f) := by
    unfold volterraProriolMatrixSolution
    rw [lp.initialL2Vector_restrict, Ring.inverseAt_eq_ringInverse]
    exact hs.1
  refine ⟨hv, (volterraProriolMatrix_equation_iff (p n.val) (hB n.val) (bp n.val) _ f).mpr ?_⟩
  rw [hv, Ring.inverseAt_eq_ringInverse]
  simpa only [approximateVolterraCoefficientSection, volterraCoefficientSection,
    sub_eq_add_neg, add_apply, one_apply_eq_self, _root_.neg_apply] using hs.2
source

Let \(K\) be continuous on the closed Volterra triangle and let \(p_n\) be polynomial kernels with finite nonnegative bounds and uniform errors \(|p_n-K|\le \varepsilon _n\to 0\), \(\varepsilon _n\ge 0\). For all sufficiently large \(n\), the assembled system

\[ (I-G_{p_n,n})v_n=(f_i)_{i{\lt}n} \]

has a unique solution. For every cutoff \(n\) at which \(B_n=I-P_nA_{p_n}\) is invertible, define \(v_n\) as in Definition 6.1.52; its zero extension equals the lifted solution and solves the matrix equation at every such cutoff. These cutoffs include every sufficiently large \(n\). For every \(f\in \ell ^2\), with \(u=(I-A_K)^{-1}f\), the zero extensions converge to \(u\) as \(n\to \infty \) through these cutoffs, and eventually

\[ \| J_nv_n-u\| \le (\| (I-A_K)^{-1}\| +1) \bigl(\| P_nu-u\| +\varepsilon _n\| u\| \bigr). \]

Every continuous \(K\) admits such a sequence with error at most \(1/(n+1)\) and convergent solves for every \(f\). No relation between the polynomial kernel degrees and section sizes is assumed; the columns use the full finite polynomial assembly before the final row restriction.

Lean Formalisation
theorem MvPolynomial.eventually_existsUnique_approximateProriolMatrix_solution {K : (Fin 2 → ℝ) → ℝ}
  (hK : ContinuousOn K Real.volterraTriangle) {M : ℝ} (hM : 0 ≤ M) (bK : ∀ z ∈ Real.volterraTriangle, |K z| ≤ M)
  (p : ℕ → MvPolynomial (Fin 2) ℝ) {B e : ℕ → ℝ} (hB : ∀ (n : ℕ), 0 ≤ B n)
  (bp : ∀ (n : ℕ), ∀ z ∈ Real.volterraTriangle, |(MvPolynomial.eval z) (p n)| ≤ B n) (he : ∀ (n : ℕ), 0 ≤ e n)
  (err : ∀ (n : ℕ), ∀ z ∈ Real.volterraTriangle, |(MvPolynomial.eval z) (p n) - K z| ≤ e n)
  (hte : Filter.Tendsto e Filter.atTop (nhds 0)) :
  ∀ᶠ (n : ℕ) in Filter.atTop,
    ∀ (f : ↥(lp (fun x => ℝ) 2)), ∃! v, (1 - (p n).volterraProriolMatrix n).mulVec v = fun i => ↑f ↑i
Lean proof
/-- Eventually every approximating assembled matrix has a unique finite solution. -/
theorem eventually_existsUnique_approximateProriolMatrix_solution :
    ∀ᶠ n in atTop, ∀ f : lp (fun _ : ℕ ↦ ℝ) 2,
      ∃! v : Fin n → ℝ, (1 - volterraProriolMatrix (p n) n) *ᵥ v = (fun i : Fin n ↦ f i) := by
  filter_upwards [eventually_existsUnique_approximateVolterra_solution hK hM bK
    (fun n ↦ (p n).continuous_eval.continuousOn) hB bp he err hte] with n hn f
  rw [volterraProriolMatrix_eq (p n) n (hB n) (bp n)]
  exact lp.existsUnique_initialL2Matrix_solution _ n f (hn f)
source