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\):
The linear marginal \(I_yf(x)=\int _0^{1-x}f(x,y)\, dy\) satisfies
Consequently, for every finite expansion,
The endpoint factor remains explicit; these identities include \(x=1\) and hold for all real \(x\) with oriented interval integrals.
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
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
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.
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 Over every commutative \(\mathbb {Q}\)-algebra, for \(n\ge 0\),
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\),
Consequently extension in \(y\) followed by the simplex marginal satisfies
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
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\),
The complete first two columns are
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.
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
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 For \(\beta {\gt}-1\), the Jacobi norm with first parameter zero is
Writing \(P_{m+k,k}\) for the unweighted DLMF Proriol polynomial, for all \(m,k\ge 0\),
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\),
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
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
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 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)\),
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 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
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 For an integrable row pair \((k,f)\) at \(x\), define its oriented value by
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
For a row with \(K(x,\cdot )f\) integrable on \(J_x=(\min (0,x),\max (0,x))\),
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 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
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
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
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 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
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
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
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 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
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 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
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\),
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
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 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 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 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 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
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\),
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
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,
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 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 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,
and eventually, for every \(u\in \ell ^2\),
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
Then \(G_{p,N}(i,j)=(A_pe_j)_i\); its multiplication is exactly the finite restriction of \(A_pJ_Nv\), and
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 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 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
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
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