6.4 First-kind Volterra equations
The integration diagonal provides a preconditioner for the Jacobi operator. We use it to prove uniqueness and finite-section convergence in the weighted solution spaces below, under the stated nonvanishing-diagonal conditions.
Let \(\ell ^2_1\) be the real sequences \(q\) for which \(((n+1)q_n)_{n\ge 0}\) belongs to \(\ell ^2\), equipped with norm
Lean Formalisation
def lp.firstOrderL2Submodule : Submodule ℝ (ℕ → ℝ)Lean definition
/-- Real sequences whose degree-weighted coefficients are square summable. -/
def firstOrderL2Submodule : Submodule ℝ (ℕ → ℝ) where
carrier := {u | Memℓp (fun n : ℕ ↦ ((n : ℝ)+1)*u n) 2}
zero_mem' := by
change Memℓp (fun n : ℕ ↦ ((n : ℝ)+1)*0) 2
simpa only [Pi.zero_apply, mul_zero] using (zero_mem_ℓp' : Memℓp (fun _ : ℕ ↦ (0 : ℝ)) 2)
add_mem' {u v} hu hv := by
change Memℓp (fun n : ℕ ↦ ((n : ℝ)+1)*(u n+v n)) 2
simpa only [Pi.add_def, mul_add] using hu.add hv
smul_mem' c u hu := by
change Memℓp (fun n : ℕ ↦ ((n : ℝ)+1)*(c*u n)) 2
simpa only [Pi.smul_def, smul_eq_mul, mul_left_comm] using hu.const_smul cDegree weighting is a linear isometric equivalence \(\ell ^2_1\to \ell ^2\); in particular this is a Banach space.
Lean Formalisation
theorem lp.norm_firstOrderL2 (u : lp.FirstOrderL2) : ‖u‖ = ‖⟨fun n => (↑n + 1) * ↑u n, ⋯⟩‖Lean proof
/-- Weighted coefficient norm, expressed using Mathlib's existing ℓ² norm. -/
theorem norm_firstOrderL2 (u : FirstOrderL2) :
‖u‖ = ‖(⟨fun n : ℕ ↦ ((n : ℝ)+1)*u.1 n, u.2⟩ : lp (fun _ : ℕ ↦ ℝ) 2)‖ := rflThe norm is on raw coefficients; it is not the norm induced by normalized physical \(L^2\) coordinates.
The endpoint-factor-free constant-kernel diagonal extends to a linear isometric equivalence \(D:\ell ^2\to \ell ^2_1\), with
It agrees with the existing finite coefficient map on every coordinate vector. Every \(q\in \ell ^2_1\) therefore has exactly one solution \(u\in \ell ^2\) to \(Du=q\). The endpoint factor and reflection remain outside this map. Reference: [GO20, Lemma 5.6]; [Gut22, Lemma 2.3].
Lean Formalisation
theorem lp.norm_alternating_mul (n : ℕ) (a : ℝ) : ‖(-1) ^ n * a‖ = ‖a‖Lean proof
/-- Alternating signs preserve each real coefficient norm. -/
theorem norm_alternating_mul (n : ℕ) (a : ℝ) : ‖(-1 : ℝ)^n*a‖ = ‖a‖ := by
simp [norm_mul, norm_pow]For \(q\in \ell ^2_1\), the truncated solution \(u_N=P_ND^{-1}q\) has coefficients
It satisfies \((Du_N)_n=q_n\) for every \(n{\lt}N\) and converges in raw \(\ell ^2\) to the exact solution. Every candidate \(v\in \ell ^2\) has the exact error identity
Lean Formalisation
theorem MvPolynomial.volterraJacobiFiniteSolution_apply (N : ℕ) (q : lp.FirstOrderL2) (i : ℕ) :
↑(MvPolynomial.volterraJacobiFiniteSolution N q) i = if i < N then (-1) ^ i * (↑i + 1) * ↑q i else 0Lean proof
/-- Each resolved coefficient is obtained by the exact first-kind diagonal inverse. -/
theorem volterraJacobiFiniteSolution_apply (N : ℕ) (q : lp.FirstOrderL2) (i : ℕ) :
volterraJacobiFiniteSolution N q i =
if i < N then ((-1 : ℝ)^i*((i : ℝ)+1))*q.1 i else 0 := by
simp only [volterraJacobiFiniteSolution, lp.initialL2Projection_apply, lp.coeFn_sum,
lp.coeFn_single, Finset.sum_apply, Finset.sum_pi_single, Finset.mem_range,
volterraJacobiL2Equiv_symm_apply]This is the constant-kernel diagonal problem, not yet the general polynomial-kernel solver.
Reference details: Raw shifted Jacobi multiplication entries and related results
Writing \(Q_n(x)=P_n^{(1,0)}(2x-1)\), multiplication by \(x\) has upper, diagonal and lower column coefficients
For \(n\ge 1\), \(xQ_n=a_nQ_{n+1}+b_nQ_n+c_nQ_{n-1}\); the constant column is \(xQ_0=a_0Q_1+b_0Q_0\).
Lean Formalisation
theorem Polynomial.X_mul_shiftedJacobi_one_zero_succ (n : ℕ) :
Polynomial.X * Polynomial.shiftedJacobi 1 0 (n + 1) =
Polynomial.C (Polynomial.shiftedJacobiOneZeroUpper (n + 1)) * Polynomial.shiftedJacobi 1 0 (n + 2) +
Polynomial.C (Polynomial.shiftedJacobiOneZeroDiag (n + 1)) * Polynomial.shiftedJacobi 1 0 (n + 1) +
Polynomial.C (Polynomial.shiftedJacobiOneZeroLower (n + 1)) * Polynomial.shiftedJacobi 1 0 nLean proof
/-- Multiplication by x in every positive-degree raw shifted Jacobi column. -/
theorem X_mul_shiftedJacobi_one_zero_succ (n : ℕ) :
X*shiftedJacobi 1 0 (n+1) =
C (shiftedJacobiOneZeroUpper (n+1))*shiftedJacobi 1 0 (n+2) +
C (shiftedJacobiOneZeroDiag (n+1))*shiftedJacobi 1 0 (n+1) +
C (shiftedJacobiOneZeroLower (n+1))*shiftedJacobi 1 0 n := by
apply Polynomial.funext
intro x
have h := congrArg (fun p : ℝ[X] ↦ p.eval (2*x-1)) (jacobi_recurrence (1 : ℝ) 0 n)
simp only [eval_mul, eval_C, eval_sub, eval_add, eval_X] at h
simp only [eval_mul, eval_add, eval_C, eval_X, eval_shiftedJacobi,
shiftedJacobiOneZeroUpper, shiftedJacobiOneZeroDiag, shiftedJacobiOneZeroLower,
Nat.cast_add, Nat.cast_one]
have h3 : (2*(n : ℝ)+3) ≠ 0 := by positivity
have h5 : (2*(n : ℝ)+5) ≠ 0 := by positivity
field_simp
simp only [mul_comm 2 x] at h
apply mul_left_cancel₀ (show (2*(n : ℝ)+4) ≠ 0 by positivity)
linear_combination -hOver real or complex scalars, \(T_1=I\). If \(A-T_p\) and \(B-T_q\) are compact, then \(A+B-T_{p+q}\), \(AB-T_{pq}\), and \(A^n-T_{p^n}\) are compact. This keeps the real coefficient convention available without complexifying the underlying integral equation.
Lean Formalisation
theorem lp.laurentToeplitz_one.{u_1} {𝕜 : Type u_1} [RCLike 𝕜] : lp.laurentToeplitz 1 = 1Lean proof
/-- The constant-one symbol gives the identity operator. -/
theorem laurentToeplitz_one : laurentToeplitz (1 : LaurentPolynomial 𝕜) = 1 := by
change laurentToeplitz (AddMonoidAlgebra.single (0 : ℤ) (1 : 𝕜)) = 1
rw [laurentToeplitz_single, one_smul]
rflThe canonical linear embedding of finitely supported real or complex sequences into \(\ell ^2\) preserves every coordinate and every coordinate vector, and is injective.
Lean Formalisation
theorem lp.finsuppL2_apply.{u_1} {𝕜 : Type u_1} [RCLike 𝕜] (c : ℕ →₀ 𝕜) (n : ℕ) : ↑(lp.finsuppL2 c) n = c nLean proof
/-- Embedding leaves every coordinate unchanged. -/
@[simp] theorem finsuppL2_apply (c : ℕ →₀ 𝕜) (n : ℕ) : finsuppL2 c n = c n := rflLet \(J_0=\tfrac 12 I+\tfrac 14(S+S^*)\). The raw shifted Jacobi \((1,0)\) multiplication matrix extends to a bounded real \(\ell ^2\) operator \(J=J_0+C_J\) with \(C_J\) compact. Its columns are exactly the coefficients \(a_n,b_n,c_n\) of the shifted Jacobi recurrence, and the embedding of every polynomial satisfies \(J\, \operatorname {coeff}(p)=\operatorname {coeff}(xp)\). There is a bounded tridiagonal operator \(H=J_0+C_H\) with \(C_H\) compact.
Lean Formalisation
theorem Polynomial.isCompactOperator_shiftedJacobiOneZeroCorrection :
IsCompactOperator ⇑Polynomial.shiftedJacobiOneZeroCorrectionLean proof
/-- The correction is compact because its reciprocal diagonals tend to zero. -/
theorem isCompactOperator_shiftedJacobiOneZeroCorrection :
IsCompactOperator shiftedJacobiOneZeroCorrection := by
have h1 := lp.isCompactOperator_reciprocalAffineDiagonal 2 1 (by norm_num) (by norm_num)
have h3 := lp.isCompactOperator_reciprocalAffineDiagonal 2 3 (by norm_num) (by norm_num)
unfold shiftedJacobiOneZeroCorrection
apply IsCompactOperator.sub
· apply IsCompactOperator.sub
· exact (h3.clm_comp lp.forwardShiftL2.toContinuousLinearMap).smul (1/4 : ℝ)
· exact (h1.comp_clm (lp.reciprocalAffineDiagonal 2 3 (by norm_num))).smul (1/2 : ℝ)
· exact (h1.clm_comp lp.backwardShiftL2).smul (1/4 : ℝ)The reflected preconditioner identity for \(H\) is Theorem 6.4.9.
The bounded raw diagonal \(D_n=(-1)^n/(n+1)\) agrees coefficientwise with the existing equivalence into weighted \(\ell ^2_1\). The second Jacobi operator satisfies \(DH=(I-J)D\). Its upper, diagonal and lower column entries are
Thus the reflected expression is \(D^{-1}(I-J)D\); the statement does not treat \(D^{-1}\) as a bounded endomorphism of raw \(\ell ^2\).
Lean Formalisation
theorem Polynomial.reflectedJacobiOneZeroL2_apply_zero (u : ↥(lp (fun x => ℝ) 2)) :
↑(Polynomial.reflectedJacobiOneZeroL2 u) 0 = 2 / 3 * ↑u 0 + 1 / 12 * ↑u 1Lean proof
/-- The first row of the reflected conjugate. -/
theorem reflectedJacobiOneZeroL2_apply_zero (u : H) :
reflectedJacobiOneZeroL2 u 0 = (2/3 : ℝ)*u 0+(1/12 : ℝ)*u 1 := by
simp only [reflectedJacobiOneZeroL2, shiftedJacobiToeplitzPart,
reflectedJacobiOneZeroCorrection, ContinuousLinearMap.comp_apply,
add_apply, sub_apply, smul_apply, one_apply_eq_self, lp.coeFn_add, lp.coeFn_sub,
lp.coeFn_smul, Pi.add_apply, Pi.sub_apply, Pi.smul_apply, smul_eq_mul,
LinearIsometry.coe_toContinuousLinearMap, lp.forwardShiftL2_zero,
lp.backwardShiftL2_apply, lp.reciprocalAffineDiagonal_apply]
norm_num
ringBoth \(J\) and \(H\) differ compactly from \(T_t\), where \(t(z)=(2+z+z^{-1})/4\). Consequently \(H^rJ^s-T_{t^{r+s}}\) is compact. On a circle with nonzero signed period the symbol is real, \(t(z)=(1+\operatorname {Re}z)/2\in [0,1]\).
Lean Formalisation
theorem Polynomial.laurentToeplitz_shiftedJacobiLaurentSymbol :
lp.laurentToeplitz Polynomial.shiftedJacobiLaurentSymbol = Polynomial.shiftedJacobiToeplitzPartLean proof
/-- Laurent quantization gives exactly the constant Jacobi tridiagonal part. -/
theorem laurentToeplitz_shiftedJacobiLaurentSymbol :
lp.laurentToeplitz shiftedJacobiLaurentSymbol = shiftedJacobiToeplitzPart := by
simp only [shiftedJacobiLaurentSymbol, map_add, lp.laurentToeplitz_single,
lp.laurentShiftL2, pow_zero, pow_one, shiftedJacobiToeplitzPart, smul_add]
abelFor a polynomial kernel \(K(x,y)=\sum _{r,s}k_{rs}x^ry^s\), define the bounded ordered coefficient operator \(A_K=\sum _{r,s}k_{rs}H^rJ^s\) and the Laurent symbol \(p_K=K(t,t)\). Then \(A_K-T_{p_K}\) is compact. On a circle with nonzero signed period, \(p_K(z)=K(\tau ,\tau )\) where \(\tau =(1+\operatorname {Re}z)/2\in [0,1]\).
Lean Formalisation
theorem MvPolynomial.isCompactOperator_volterraPreconditionedL2_sub_symbol (K : MvPolynomial (Fin 2) ℝ) :
IsCompactOperator ⇑(K.volterraPreconditionedL2 - lp.laurentToeplitz K.volterraDiagonalLaurentSymbol)Lean proof
/-- Every polynomial expression differs compactly from its diagonal-symbol Toeplitz operator. -/
theorem isCompactOperator_volterraPreconditionedL2_sub_symbol
(K : MvPolynomial (Fin 2) ℝ) :
IsCompactOperator (volterraPreconditionedL2 K-
lp.laurentToeplitz (volterraDiagonalLaurentSymbol K)) := by
classical
simp only [volterraPreconditionedL2, volterraDiagonalLaurentSymbol, map_sum, map_smul,
← Finset.sum_sub_distrib]
change (∑ d ∈ K.support, (K.coeff d •
(reflectedJacobiOneZeroL2^(d 0)*shiftedJacobiOneZeroL2^(d 1))-
K.coeff d • lp.laurentToeplitz (shiftedJacobiLaurentSymbol^(d 0+d 1)))) ∈
compactOperator (RingHom.id ℝ) H H
apply Submodule.sum_mem
intro d hd
have he : K.coeff d • (reflectedJacobiOneZeroL2^(d 0)*shiftedJacobiOneZeroL2^(d 1))-
K.coeff d • lp.laurentToeplitz (shiftedJacobiLaurentSymbol^(d 0+d 1)) =
K.coeff d • (reflectedJacobiOneZeroL2^(d 0)*shiftedJacobiOneZeroL2^(d 1)-
lp.laurentToeplitz (shiftedJacobiLaurentSymbol^(d 0+d 1))) := by module
rw [he]
exact Submodule.smul_mem _ _ (isCompactOperator_reflectedJacobi_pow_mul_sub_symbol _ _)The integral realization is given in Theorem 6.4.24.
Assume \(K(x,x)\ge a{\gt}0\) on \([0,1]\) and that the ordered coefficient operator \(A_K\) is injective. The Toeplitz part has quadratic form bounded below by \(a\| u\| ^2\), and \(A_K\) is invertible. Its leading sections \(I-P_N+P_NA_KP_N\) are eventually invertible, and their solutions for right-hand sides \(P_Ng\) converge in raw \(\ell ^2\) to \(A_K^{-1}g\).
Lean Formalisation
theorem MvPolynomial.inner_volterraDiagonalToeplitz_le (K : MvPolynomial (Fin 2) ℝ) {a : ℝ}
(hK : ∀ x ∈ Set.Icc 0 1, a ≤ (MvPolynomial.eval fun x_1 => x) K) (u : ↥(lp (fun x => ℝ) 2)) :
a * ‖u‖ ^ 2 ≤ inner ℝ u ((lp.laurentToeplitz K.volterraDiagonalLaurentSymbol) u)Lean proof
/-- A lower bound on the kernel diagonal controls the real Toeplitz quadratic form. -/
theorem inner_volterraDiagonalToeplitz_le (K : MvPolynomial (Fin 2) ℝ) {a : ℝ}
(hK : ∀ x ∈ Set.Icc (0 : ℝ) 1, a ≤ eval (fun _ ↦ x) K) (u : H) :
a*‖u‖^2 ≤ ⟪u, lp.laurentToeplitz (volterraDiagonalLaurentSymbol K) u⟫_ℝ := by
let : Fact (0 < (1 : ℝ)) := ⟨zero_lt_one⟩
apply lp.inner_laurentToeplitz_le (T := 1)
intro x
rw [volterraDiagonalLaurentSymbol_circle, Complex.ofReal_re]
exact hK _ (Polynomial.shiftedJacobiLaurentSymbol_circle_mem_Icc (T := ⟨1, one_ne_zero⟩) x)Theorem 6.4.32 removes the injectivity hypothesis for polynomial kernels with nonvanishing diagonal.
For a real polynomial kernel \(K(x,y)\), write the classical oriented integral \(V_K f(x)=\int _0^xK(x,y)f(y)\, dy\). If \(f\) is locally integrable on \(\mathbb R\), then \(V_K f\) is continuous and, almost everywhere,
Polynomial kernel slices times \(f\) are interval-integrable. Kernel addition commutes with integration; multiplying the kernel by \(x\) multiplies the output by \(x\), and multiplying it by \(y\) multiplies the input by its coordinate. The algebraic identities also hold at any fixed endpoint whenever their row products are integrable; the factors need not be separately integrable. Reference: [Lin85], first-kind equations with differentiable kernels.
Lean Formalisation
theorem MvPolynomial.polynomialVolterraIntegral_add (K L : MvPolynomial (Fin 2) ℝ) (f : ℝ → ℝ) (x : ℝ)
(hK : IntervalIntegrable (fun y => (MvPolynomial.eval ![x, y]) K * f y) MeasureTheory.volume 0 x)
(hL : IntervalIntegrable (fun y => (MvPolynomial.eval ![x, y]) L * f y) MeasureTheory.volume 0 x) :
Real.volterraIntegral (Real.VolterraIntegralInput.ofKernel (fun z => (MvPolynomial.eval z) (K + L)) f ⋯) =
Real.volterraIntegral (Real.VolterraIntegralInput.ofKernel (fun z => (MvPolynomial.eval z) K) f hK) +
Real.volterraIntegral (Real.VolterraIntegralInput.ofKernel (fun z => (MvPolynomial.eval z) L) f hL)Lean proof
/-- Polynomial-kernel integration is additive whenever the two row products exist. -/
theorem polynomialVolterraIntegral_add (K L : MvPolynomial (Fin 2) ℝ)
(f : ℝ → ℝ) (x : ℝ)
(hK : IntervalIntegrable (fun y ↦ eval ![x,y] K * f y) volume 0 x)
(hL : IntervalIntegrable (fun y ↦ eval ![x,y] L * f y) volume 0 x) :
Real.volterraIntegral (.ofKernel (x := x) (fun z ↦ eval z (K+L)) f
(by simpa only [eval_add, add_mul] using hK.add hL)) =
Real.volterraIntegral (.ofKernel (x := x) (fun z ↦ eval z K) f hK) +
Real.volterraIntegral (.ofKernel (x := x) (fun z ↦ eval z L) f hL) := by
simp only [Real.volterraIntegral_ofKernel, eval_add, add_mul]
exact intervalIntegral.integral_add hK hLLet \(b{\gt}0\), let \(K\) be a real polynomial kernel, and suppose \(K(x,x)\ne 0\) on \([0,b]\). For every \(f\in L^1([0,b])\),
The diagonal may have either sign. The same conclusion is proved for locally integrable inputs; globally continuous inputs vanish pointwise on the interval. A zero output satisfies \(K(x,x)f(x)=-V_{\partial _xK}f(x)\) almost everywhere. Volterra integration on any \([0,x]\subseteq [0,b]\) respects almost-everywhere equality of inputs whenever the kernel–input products are integrable on that row. The supporting integral inequality states that a globally continuous real \(g\) with \(\| g(x)\| \le M\int _0^x\| g(y)\| \, dy\) on \([0,b]\) vanishes there.
Lean Formalisation
theorem Real.eq_zero_of_norm_le_volterra_integral {f : ℝ → ℝ} {b M : ℝ} (hf : Continuous f)
(hbound : ∀ x ∈ Set.Icc 0 b, ‖f x‖ ≤ M * ∫ (y : ℝ) in 0..x, ‖f y‖) (x : ℝ) : x ∈ Set.Icc 0 b → f x = 0Lean proof
/-- The homogeneous Volterra integral inequality forces a continuous function to vanish. -/
theorem Real.eq_zero_of_norm_le_volterra_integral {f : ℝ → ℝ} {b M : ℝ}
(hf : Continuous f)
(hbound : ∀ x ∈ Icc 0 b, ‖f x‖ ≤ M * ∫ y in (0 : ℝ)..x, ‖f y‖) :
∀ x ∈ Icc 0 b, f x = 0 := by
have hi (a c : ℝ) : IntervalIntegrable (fun y ↦ ‖f y‖) volume a c :=
hf.norm.intervalIntegrable a c
have hF := intervalIntegral.continuous_primitive hi 0
have hd (x : ℝ) : HasDerivAt (fun x ↦ ∫ y in (0 : ℝ)..x, ‖f y‖) ‖f x‖ x :=
intervalIntegral.integral_hasDerivAt_right (hi 0 x)
hf.norm.stronglyMeasurable.stronglyMeasurableAtFilter hf.norm.continuousAt
have hz := eq_zero_of_abs_deriv_le_mul_abs_self_of_eq_zero_right (a := 0) (b := b)
hF.continuousOn (fun x _ ↦ (hd x).hasDerivWithinAt)
(by simp) (fun x hx ↦ (by
rw [norm_norm]
exact (hbound x ⟨hx.1, hx.2.le⟩).trans_eq (by
rw [Real.norm_of_nonneg (intervalIntegral.integral_nonneg hx.1
(fun y _ ↦ norm_nonneg (f y)))])))
intro x hx
have hh := hbound x hx
rw [hz x hx, mul_zero] at hh
exact norm_le_zero_iff.mp hhReference details: Injectivity of exact finite Proriol assembly and related results
If \(K(x,x)\ne 0\) on some interval \([0,b]\) with \(b{\gt}0\), then the exact Proriol Volterra coefficient map is injective on finitely supported shifted Jacobi \((1,0)\) inputs. In particular, a finite input with zero assembled output is zero. This concerns the full finite-support map, not injectivity of every square truncation or of its extension to infinite raw coefficient sequences.
Lean Formalisation
theorem MvPolynomial.eq_zero_of_volterraProriolCoefficients_eq_zero {K : MvPolynomial (Fin 2) ℝ} {b : ℝ} (hb : 0 < b)
(hdiag : ∀ x ∈ Set.Icc 0 b, (MvPolynomial.eval fun x_1 => x) K ≠ 0) {c : ℕ →₀ ℝ}
(hc : K.volterraProriolCoefficients c = 0) : c = 0Lean proof
/-- A finite coefficient input with zero assembled output must vanish. -/
theorem eq_zero_of_volterraProriolCoefficients_eq_zero
{K : MvPolynomial (Fin 2) ℝ} {b : ℝ} (hb : 0 < b)
(hdiag : ∀ x ∈ Icc 0 b, eval (fun _ ↦ x) K ≠ 0)
{c : ℕ →₀ ℝ} (hc : volterraProriolCoefficients K c = 0) : c = 0 := by
let p := Finsupp.linearCombination ℝ (shiftedJacobi 1 0) c
have hv : ∀ x ∈ Icc 0 b, Real.volterraIntegral (.ofPolynomial K p.continuous.locallyIntegrable x) = 0 := by
intro x hx
rw [Real.VolterraIntegralInput.ofPolynomial, Real.volterraIntegral_ofKernel]
change (∫ y in (0 : ℝ)..x, eval (![x,y] : Fin 2 → ℝ) K * p.eval y) = 0
rw [← volterraProriolCoefficients_exact K c x, hc]
simp
have he := eq_zero_of_polynomialVolterraIntegral_eq_zero hb p.continuous hdiag hv
have hp : p = 0 := p.eq_zero_of_infinite_isRoot
((Icc_infinite hb).mono (fun x hx ↦ he x hx))
let B := shiftedJacobiBasis (by norm_num : (-1 : ℝ) < 1)
(by norm_num : (-1 : ℝ) < 0)
have hB : shiftedJacobi 1 0 = B := by
funext n
exact (shiftedJacobiBasis_apply _ _ n).symm
have hl : LinearIndependent ℝ (shiftedJacobi 1 0) := by
rw [hB]
exact B.linearIndependent
apply hl.finsuppLinearCombination_injective
simpa only [map_zero] using hpFor \(\mu =\mathrm{unitJacobiMeasure}(1,0)\) the raw shifted Jacobi polynomial \(\widetilde P_n^{(1,0)}\) has squared norm \(2/(n+1)\). Scaling normalized Hilbert coordinates by \(\sqrt{2/(n+1)}\le \sqrt2\) defines a bounded injective synthesis map \(S:\ell ^2\to L^2(\mu )\). It sends each coordinate vector to its raw polynomial, agrees with finite polynomial synthesis, and sends coefficient truncations to a sequence converging to \(Sc\) in \(L^2(\mu )\).
Lean Formalisation
theorem Polynomial.integral_sq_shiftedJacobi_one_zero (n : ℕ) :
∫ (x : ℝ), Polynomial.eval x (Polynomial.shiftedJacobi 1 0 n) ^ 2 ∂Polynomial.unitJacobiMeasure 1 0 = 2 / (↑n + 1)Lean proof
/-- The raw shifted (1,0) Jacobi squared norm after affine transport. -/
theorem integral_sq_shiftedJacobi_one_zero (n : ℕ) :
(∫ x, (shiftedJacobi 1 0 n).eval x ^ 2 ∂unitJacobiMeasure 1 0) =
2 / ((n : ℝ) + 1) := by
have he := integralInner_shiftedJacobi 1 0 n n
(hi := (hasFiniteMoments_jacobiMeasure (by norm_num) (by norm_num)).integrable_mul _ _)
simp only [integralInner, ← sq] at he
rw [he]
cases n with
| zero =>
rw [integral_sq_jacobi_zero (by norm_num) (by norm_num)]
norm_num [GammaOn, GammaPoint.ofPos, Gamma_add_one, Gamma_one]
| succ n =>
rw [integral_sq_jacobi_succ (by norm_num) (by norm_num)]
simp only [GammaOn, GammaPoint.ofPos]
have hG : Gamma ((n : ℝ) + 1 + 2) ≠ 0 :=
(Gamma_pos_of_pos (by positivity)).ne'
have hF : ((n + 1).factorial : ℝ) ≠ 0 := by positivity
have hG2 : Gamma ((n : ℝ) + 0 + 2) = (n + 1).factorial := by
rw [show (n : ℝ) + 0 + 2 = ((n+1 : ℕ) : ℝ) + 1 by push_cast; ring]
exact Gamma_nat_eq_factorial (n+1)
rw [hG2]
norm_num only [add_zero, zero_add, Nat.cast_add, Nat.cast_one, Real.rpow_natCast]
field_simp
ringNo bounded inverse on its range or surjectivity is asserted.
Ordered polynomial quantization \(A_K=\sum _{i,j}K_{ij}H^iJ^j\) is linear in \(K\), has \(A_a=aI\), and obeys \(A_{xK}=HA_K\) and \(A_{yK}=A_KJ\). A monomial \(ax^iy^j\) gives exactly \(aH^iJ^j\); the order of these factors is retained.
Lean Formalisation
theorem MvPolynomial.volterraPreconditionedLinear_apply (K : MvPolynomial (Fin 2) ℝ) :
MvPolynomial.volterraPreconditionedLinear K = K.volterraPreconditionedL2Lean proof
/-- The linear quantization is the existing bounded ordered operator. -/
theorem volterraPreconditionedLinear_apply (K : MvPolynomial (Fin 2) ℝ) :
volterraPreconditionedLinear K = volterraPreconditionedL2 K := rflLet \(V_K\) denote the exact finite Proriol coefficient assembly and \(\iota \) the embedding of finite coefficients into raw \(\ell ^2\). Then
The raw coefficient map recovers \(c\) from its polynomial synthesis, and \(D\iota c\) agrees with the finite integration diagonal. Assembly is linear in the kernel and sends a constant kernel \(a\) to \(aD\). Multiplication of the kernel by \(x\) multiplies the reflected output polynomial by \(1-X\) (and its raw coefficient vector by \(I-J\)); multiplication by \(y\) replaces the input polynomial by \(X\) times that polynomial.
Lean Formalisation
theorem Polynomial.shiftedJacobiOneZeroCoefficients_linearCombination (c : ℕ →₀ ℝ) :
Polynomial.shiftedJacobiOneZeroCoefficients ((Finsupp.linearCombination ℝ (Polynomial.shiftedJacobi 1 0)) c) =
lp.finsuppL2 cLean proof
/-- The raw polynomial coefficient map recovers every finite coefficient vector. -/
theorem shiftedJacobiOneZeroCoefficients_linearCombination (c : ℕ →₀ ℝ) :
shiftedJacobiOneZeroCoefficients (Finsupp.linearCombination ℝ (shiftedJacobi 1 0) c) =
lp.finsuppL2 c := by
let B := shiftedJacobiBasis (by norm_num : (-1 : ℝ) < 1)
(by norm_num : (-1 : ℝ) < 0)
have hB : shiftedJacobi 1 0 = B := by
funext n
exact (shiftedJacobiBasis_apply _ _ n).symm
change lp.finsuppL2 (B.repr (Finsupp.linearCombination ℝ (shiftedJacobi 1 0) c)) = _
rw [hB, Module.Basis.repr_linearCombination]Let a joint measure \(\kappa \) have coordinate marginals \(\mu \) and \(\nu \). If a real kernel \(k\) is almost-everywhere strongly measurable and \(|k|\le M\) almost everywhere, with \(M\ge 0\), then it defines a bounded operator \(B:L^2(\nu )\to L^2(\mu )\) with \(\| B\| \le M\) and
The displayed integrand is absolutely integrable for every pair of inputs.
Lean Formalisation
theorem MeasureTheory.inner_marginalKernelL2Operator.{u_1, u_2} {X : Type u_1} {Y : Type u_2} [MeasurableSpace X]
[MeasurableSpace Y] (μ : MeasureTheory.Measure X) (ν : MeasureTheory.Measure Y) (κ : MeasureTheory.Measure (X × Y))
(hfst : MeasureTheory.Measure.map Prod.fst κ = μ) (hsnd : MeasureTheory.Measure.map Prod.snd κ = ν) (k : X × Y → ℝ)
(hk : MeasureTheory.AEStronglyMeasurable k κ) {M : ℝ} (hM : 0 ≤ M) (hb : ∀ᵐ (z : X × Y) ∂κ, ‖k z‖ ≤ M)
(f : ↥(MeasureTheory.Lp ℝ 2 ν)) (g : ↥(MeasureTheory.Lp ℝ 2 μ)) :
inner ℝ g ((MeasureTheory.marginalKernelL2Operator μ ν κ hfst hsnd k hk hM hb) f) =
∫ (z : X × Y), k z * (↑↑g z.1 * ↑↑f z.2) ∂κLean proof
/-- The weak integral formula defining the marginal kernel operator. -/
theorem inner_marginalKernelL2Operator (f : Lp ℝ 2 ν) (g : Lp ℝ 2 μ) :
⟪g, marginalKernelL2Operator μ ν κ hfst hsnd k hk hM hb f⟫_ℝ =
∫ z, k z * (g z.1*f z.2) ∂κ := by
rw [marginalKernelL2Operator, ContinuousLinearMap.comp_apply,
ContinuousLinearMap.adjoint_inner_right, ContinuousLinearMap.comp_apply, L2.inner_def]
apply integral_congr_ae
filter_upwards [boundedMulL2_ae κ k hk hM hb
(dominatedL2Pullback ν κ Prod.snd measurable_snd ENNReal.one_ne_top
(by rw [one_smul, hsnd]) f),
dominatedL2Pullback_ae μ κ Prod.fst measurable_fst ENNReal.one_ne_top
(by rw [one_smul, hfst]) g,
dominatedL2Pullback_ae ν κ Prod.snd measurable_snd ENNReal.one_ne_top
(by rw [one_smul, hsnd]) f] with z hz hg hf
simp only [hz, hg, hf, Function.comp_apply, Real.inner_apply]
ringArea measure on \(\{ (s,y)\in [0,1]^2:s+y\le 1\} \) has both coordinate marginals \((1-t)\, dt\). Thus the joint measure \(\kappa \) obtained by multiplying this area measure by four has both marginals \(\mu =\mathrm{unitJacobiMeasure}(1,0)=4(1-t)\, dt\). It is supported on that simplex and, for every \(\kappa \)-integrable real function \(F\),
For a real integrable input \(f\) against \(\mu \), the function \(t\mapsto (1-t)f(t)\) is integrable on \([0,1]\), and \(\int f\, d\mu =4\int _0^1(1-t)f(t)\, dt\).
Lean Formalisation
theorem Real.map_fst_reflectedVolterraTriangleMeasure :
MeasureTheory.Measure.map Prod.fst Real.reflectedVolterraTriangleMeasure =
(MeasureTheory.volume.restrict (Set.Icc 0 1)).withDensity fun x => ENNReal.ofReal (1 - x)Lean proof
/-- The first marginal of simplex area has density 1-x. -/
theorem map_fst_reflectedVolterraTriangleMeasure :
reflectedVolterraTriangleMeasure.map Prod.fst = (ν).withDensity (fun x ↦ ENNReal.ofReal (1-x)) := by
ext s hs
rw [reflectedVolterraTriangleMeasure, Measure.map_apply measurable_fst hs,
Measure.restrict_apply (measurable_fst hs),
Measure.prod_apply ((measurable_fst hs).inter (measurableSet_le (show Measurable (fun z : ℝ × ℝ ↦ z.1 + z.2) from measurable_fst.add measurable_snd) measurable_const)),
withDensity_apply _ hs, ← lintegral_indicator (μ := ν) hs (fun x : ℝ ↦ ENNReal.ofReal (1-x))]
apply lintegral_congr_ae
filter_upwards [ae_restrict_mem measurableSet_Icc] with x hx
by_cases hxs : x ∈ s
· have he : Prod.mk x ⁻¹' (Prod.fst ⁻¹' s ∩ {z : ℝ × ℝ | z.1 + z.2 ≤ 1}) = Iic (1-x) := by
ext y; simp [hxs, le_sub_iff_add_le, add_comm]
rw [he, Measure.restrict_apply measurableSet_Iic]
have hi : Iic (1-x) ∩ Icc (0 : ℝ) 1 = Icc 0 (1-x) := by
ext y; simp only [mem_inter_iff, mem_Iic, mem_Icc]; constructor <;> intro h
· exact ⟨h.2.1,h.1⟩
· exact ⟨h.2,h.1,h.2.trans (by linarith [hx.1])⟩
rw [hi, Real.volume_Icc]
simp [hxs]
· have he : Prod.mk x ⁻¹' (Prod.fst ⁻¹' s ∩ {z : ℝ × ℝ | z.1 + z.2 ≤ 1}) = ∅ := by
ext y; simp [hxs]
simp [he,hxs]The measure \(\mu =\mathrm{unitJacobiMeasure}(1,0)\) and Lebesgue measure restricted to \([0,1]\) have the same null sets. Every \(f\in L^2(\mu )\) is Lebesgue integrable on \([0,b]\) for every \(b{\lt}1\).
Lean Formalisation
theorem Polynomial.ae_unitJacobiMeasure_one_zero_iff {p : ℝ → Prop} :
(∀ᵐ (x : ℝ) ∂Polynomial.unitJacobiMeasure 1 0, p x) ↔ ∀ᵐ (x : ℝ) ∂MeasureTheory.volume.restrict (Set.Icc 0 1), p xLean proof
/-- The Jacobi weight changes no null sets on the unit interval. -/
theorem ae_unitJacobiMeasure_one_zero_iff {p : ℝ → Prop} :
(∀ᵐ x ∂μ, p x) ↔ ∀ᵐ x ∂ν, p x := by
rw [unitJacobiMeasure_one_zero_triangle, Real.map_fst_reflectedVolterraTriangleMeasure,
Measure.ae_ennreal_smul_measure_iff (by norm_num : (4 : ℝ≥0∞) ≠ 0),
ae_withDensity_iff (by fun_prop)]
have hp : ∀ᵐ x ∂ν, ENNReal.ofReal (1-x) ≠ 0 := by
filter_upwards [ae_restrict_mem measurableSet_Icc, ((ν).ae_ne 1)] with x hx hx1
exact (ENNReal.ofReal_pos.mpr (by rcases hx with ⟨_,hx⟩; have : x < 1 := lt_of_le_of_ne hx hx1; linarith)).ne'
constructor
· intro h
filter_upwards [h,hp] with x hx hp
exact hx hp
· intro h
filter_upwards [h] with x hx
exact fun _ ↦ hxFor a continuous kernel on \(\Delta \) and \(f\in L^2(\mathrm{unitJacobiMeasure}(1,0))\), the product \(K(x,\cdot )f\) is integrable on every row with \(0\le x{\lt}1\). Thus \(V_Kf(x)\) is the integral of this product over \((0,x)\), with the zero row equal to zero.
Lean Formalisation
def Real.VolterraIntegralInput.ofJacobiOneZeroLp {K : (Fin 2 → ℝ) → ℝ} (hK : ContinuousOn K Real.volterraTriangle)
(f : ↥(MeasureTheory.Lp ℝ 2 (Polynomial.unitJacobiMeasure 1 0))) (x : ↑(Set.Ico 0 1)) : (↑x).VolterraIntegralInputLean definition
/-- Weighted Jacobi L² data supply each row strictly before the vanishing endpoint. -/
def VolterraIntegralInput.ofJacobiOneZeroLp
{K : (Fin 2 → ℝ) → ℝ} (hK : ContinuousOn K volterraTriangle)
(f : Lp ℝ 2 (unitJacobiMeasure 1 0)) (x : Ico (0 : ℝ) 1) :
VolterraIntegralInput (x : ℝ) :=
.ofContinuousKernel hK (f := fun y ↦ f y) ⟨x, x.property.1, x.property.2.le⟩ (by
apply intervalIntegrable_iff.mpr
rw [uIoc_of_le x.property.1]
exact (integrableOn_coe_jacobiOneZeroLp f x.property.2).mono_set Ioc_subset_Icc_self)For a real polynomial kernel \(K\) with \(|K|\le M\) on the physical unit triangle, \(M\ge 0\), the reflected joint kernel \(K(1-s,y)\) defines a bounded operator \(B_K:L^2(\mu )\to L^2(\mu )\), \(\mu =\mathrm{unitJacobiMeasure}(1,0)\), with \(\| B_K\| \le M\). For all inputs \(f,g\),
If polynomials \(p,q\) satisfy \(V_Kp(x)=xq(1-x)\) on \([0,1]\), then \(B_K[p]=[q]\) in weighted \(L^2\). Thus the polynomial output retains both the reflection and the division by the endpoint factor.
Lean Formalisation
theorem MvPolynomial.ae_norm_reflectedVolterraKernel_le (K : MvPolynomial (Fin 2) ℝ) {M : ℝ}
(hb : ∀ z ∈ Real.volterraTriangle, |(MvPolynomial.eval z) K| ≤ M) :
∀ᵐ (z : ℝ × ℝ) ∂Real.jacobiVolterraJoint, ‖(MvPolynomial.eval ![1 - z.1, z.2]) K‖ ≤ MLean proof
/-- A bound on the physical triangle bounds the reflected joint kernel. -/
theorem ae_norm_reflectedVolterraKernel_le :
∀ᵐ z ∂κ, ‖eval (![1-z.1,z.2] : Fin 2 → ℝ) K‖ ≤ M := by
filter_upwards [Real.ae_mem_jacobiVolterraJoint] with z hz
apply hb
change (1-z.1) ∈ Icc (0 : ℝ) 1 ∧ z.2 ∈ Icc 0 (1-z.1)
exact ⟨⟨by linarith [hz.1.2], by linarith [hz.1.1]⟩,
⟨hz.2.1.1, by linarith [hz.2.2]⟩⟩For every polynomial kernel \(K\) and triangle bound \(M\ge 0\), raw Jacobi synthesis \(S\) intertwines the full ordered coefficient operator and the weighted integral realization:
This is an equality of bounded operators on all of raw \(\ell ^2\), not only on finite coefficient sequences.
Lean Formalisation
theorem MvPolynomial.jacobiVolterraL2Operator_raw_synthesis (K : MvPolynomial (Fin 2) ℝ) {M : ℝ} (hM : 0 ≤ M)
(hb : ∀ z ∈ Real.volterraTriangle, |(MvPolynomial.eval z) K| ≤ M) :
Polynomial.shiftedJacobiOneZeroSynthesis ∘SL Polynomial.volterraRawDiagonal ∘SL K.volterraPreconditionedL2 =
K.jacobiVolterraL2Operator hM hb ∘SL Polynomial.shiftedJacobiOneZeroSynthesisLean proof
/-- Raw synthesis intertwines the full ordered operator, with its integration
diagonal, and the bounded weighted Volterra realization. -/
theorem jacobiVolterraL2Operator_raw_synthesis (K : MvPolynomial (Fin 2) ℝ)
{M : ℝ} (hM : 0 ≤ M) (hb : ∀ z ∈ Real.volterraTriangle, |eval z K| ≤ M) :
shiftedJacobiOneZeroSynthesis.comp
(volterraRawDiagonal.comp (volterraPreconditionedL2 K)) =
(jacobiVolterraL2Operator K hM hb).comp shiftedJacobiOneZeroSynthesis := by
apply lp.ext_continuousLinearMap (by norm_num : (2 : ℝ≥0∞) ≠ ⊤)
intro i
apply ContinuousLinearMap.ext
intro a
change shiftedJacobiOneZeroSynthesis
(volterraRawDiagonal (volterraPreconditionedL2 K (lp.single 2 i a))) =
jacobiVolterraL2Operator K hM hb (shiftedJacobiOneZeroSynthesis (lp.single 2 i a))
rw [← lp.finsuppL2_single, volterraRawDiagonal_preconditioned_finsupp,
shiftedJacobiOneZeroSynthesis_finsupp, shiftedJacobiOneZeroSynthesis_finsupp]
apply (jacobiVolterraL2Operator_polynomial K hM hb _ _ _).symm
intro x hx
simpa only [Real.VolterraIntegralInput.ofPolynomial, Real.volterraIntegral_ofKernel] using
(volterraProriolCoefficients_exact K (Finsupp.single i a) x).symmLet \(\Delta =\{ (x,y):0\le y\le x\le 1\} \) and \(\mu (ds)=4(1-s)\, ds\) on \([0,1]\). For a real kernel \(K\) continuous on \(\Delta \) and \(|K|\le M\), \(M\ge 0\), the averaged reflected operator \(B_K\) is bounded on \(L^2(\mu )\), with \(\| B_K\| \le M\). Its weak formula is
Each inner Volterra integral exists for \(0{\lt}s{\lt}1\); no endpoint value is needed. The joint-measure pairing is integrable, and reflection lands in \(\Delta \) almost everywhere for that measure. This construction agrees with the polynomial one. Subtraction of kernels subtracts operators; if \(|K-L|\le \delta \) on \(\Delta \), \(\delta \ge 0\), then \(\| B_K-B_L\| \le \delta \).
Lean Formalisation
theorem Real.ae_reflected_mem_volterraTriangle :
∀ᵐ (z : ℝ × ℝ) ∂Real.jacobiVolterraJoint, ![1 - z.1, z.2] ∈ Real.volterraTriangleLean proof
/-- Reflection carries almost every joint-measure point to the physical triangle. -/
theorem ae_reflected_mem_volterraTriangle :
∀ᵐ z ∂κ, (![1-z.1,z.2] : Fin 2 → ℝ) ∈ volterraTriangle := by
filter_upwards [ae_mem_jacobiVolterraJoint] with z hz
change (1-z.1) ∈ Icc (0 : ℝ) 1 ∧ z.2 ∈ Icc 0 (1-z.1)
exact ⟨⟨by linarith [hz.1.2],by linarith [hz.1.1]⟩,
⟨hz.2.1.1,by linarith [hz.2.2]⟩⟩For \(K\) continuous on \(\Delta \) and \(f\in L^1(\mathbb R)\), every slice \(K(x,\cdot )f\) is integrable on \([0,x]\), \(0\le x\le 1\), and \(V_Kf\) is continuous on \([0,1]\). If \(K,L\) are continuous and \(|K-L|\le e\), \(e\ge 0\), on \(\Delta \), then
Consequently, uniformly convergent polynomial kernel approximants give uniformly convergent primitives for each such input.
Lean Formalisation
theorem Real.intervalIntegrable_continuousVolterra_mul {K : (Fin 2 → ℝ) → ℝ} (hK : ContinuousOn K Real.volterraTriangle)
{f : ℝ → ℝ} (hf : MeasureTheory.Integrable f MeasureTheory.volume) {x : ℝ} (hx : x ∈ Set.Icc 0 1) :
IntervalIntegrable (fun y => K ![x, y] * f y) MeasureTheory.volume 0 xLean proof
/-- Continuous triangle kernels may be integrated against an integrable input on each slice. -/
theorem intervalIntegrable_continuousVolterra_mul
{K : (Fin 2 → ℝ) → ℝ} (hK : ContinuousOn K volterraTriangle)
{f : ℝ → ℝ} (hf : Integrable f volume) {x : ℝ} (hx : x ∈ Icc 0 1) :
IntervalIntegrable (fun y ↦ K ![x,y]*f y) volume 0 x := by
apply hf.intervalIntegrable.continuousOn_mul
rw [uIcc_of_le hx.1]
exact hK.comp (by fun_prop) (fun y hy ↦ ⟨hx,hy⟩)Let \(f\) be integrable on \([0,b]\). Suppose each slice \(y\mapsto K(x,y)\) is absolutely continuous on \([0,x]\) and \(K(x,x)\ne 0\). Suppose that for one real constant \(C\), each row has an integrable derivative representative \(h_x\) with
The condition is independent of the derivative representative. If \(V_Kf\) vanishes throughout \([0,b]\), then \(f=0\) almost everywhere there. For locally integrable \(f\), its primitive \(\int _0^x f\) also vanishes throughout that interval. Changing the input on a null subset of \([0,b]\) does not change its Volterra integrals on the interval.
Lean Formalisation
theorem Real.volterraIntegral_congr_ae_on (K : (Fin 2 → ℝ) → ℝ) {f g : ℝ → ℝ} {b x : ℝ} (hx : x ∈ Set.Icc 0 b)
(hfg : f =ᵐ[MeasureTheory.volume.restrict (Set.Icc 0 b)] g)
(hf : IntervalIntegrable (fun y => K ![x, y] * f y) MeasureTheory.volume 0 x)
(hg : IntervalIntegrable (fun y => K ![x, y] * g y) MeasureTheory.volume 0 x) :
Real.volterraIntegral (Real.VolterraIntegralInput.ofKernel K f hf) =
Real.volterraIntegral (Real.VolterraIntegralInput.ofKernel K g hg)Lean proof
/-- Volterra integrals on a subinterval depend only on the input's local almost-everywhere class. -/
theorem volterraIntegral_congr_ae_on (K : (Fin 2 → ℝ) → ℝ)
{f g : ℝ → ℝ} {b x : ℝ} (hx : x ∈ Icc 0 b)
(hfg : f =ᵐ[volume.restrict (Icc 0 b)] g)
(hf : IntervalIntegrable (fun y ↦ K ![x,y]*f y) volume 0 x)
(hg : IntervalIntegrable (fun y ↦ K ![x,y]*g y) volume 0 x) :
volterraIntegral (.ofKernel K f hf) = volterraIntegral (.ofKernel K g hg) := by
simp only [volterraIntegral_ofKernel]
apply intervalIntegral.integral_congr_ae_restrict
have hs : Set.uIoc 0 x ⊆ Icc 0 b := by
rw [uIoc_of_le hx.1]
exact fun y hy ↦ ⟨hy.1.le,hy.2.trans hx.2⟩
filter_upwards [ae_restrict_of_ae_restrict_of_subset hs hfg] with y hy
rw [hy]Reference details: Injectivity of the continuous weighted Volterra realization and related results
Let \(K\) be continuous and bounded on \(\Delta \). If \(B_Kf=0\), then \(V_Kf=0\) on every \([0,b]\) with \(0{\lt}b{\lt}1\). If additionally the absolutely continuous slice, derivative-bound and nonvanishing-diagonal hypotheses of Theorem 6.4.27 hold on \([0,1]\), then \(B_K\) is injective on \(L^2(\mu )\).
Lean Formalisation
theorem Real.volterraIntegral_eq_zero_of_jacobiVolterraL2Operator_eq_zero (K : (Fin 2 → ℝ) → ℝ)
(hK : ContinuousOn K Real.volterraTriangle) {M : ℝ} (hM : 0 ≤ M) (hbnd : ∀ z ∈ Real.volterraTriangle, |K z| ≤ M)
(f : ↥(MeasureTheory.Lp ℝ 2 (Polynomial.unitJacobiMeasure 1 0)))
(hz : (Real.jacobiVolterraL2Operator hK hM hbnd) f = 0) {b : ℝ} (hb0 : 0 < b) (hb1 : b < 1) (x : ↑(Set.Icc 0 b)) :
Real.volterraIntegral (Real.VolterraIntegralInput.ofJacobiOneZeroLp hK f ⟨↑x, ⋯⟩) = 0Lean proof
/-- A zero weighted output gives zero classical rows on each compact interior interval. -/
theorem volterraIntegral_eq_zero_of_jacobiVolterraL2Operator_eq_zero
(K : (Fin 2 → ℝ) → ℝ) (hK : ContinuousOn K volterraTriangle) {M : ℝ} (hM : 0 ≤ M)
(hbnd : ∀ z ∈ volterraTriangle, |K z| ≤ M)
(f : Lp ℝ 2 μ) (hz : jacobiVolterraL2Operator hK hM hbnd f = 0)
{b : ℝ} (hb0 : 0 < b) (hb1 : b < 1) :
∀ x : Icc (0 : ℝ) b, volterraIntegral
(.ofJacobiOneZeroLp hK f ⟨x, x.property.1, x.property.2.trans_lt hb1⟩) = 0 := by
intro x
simpa only [VolterraIntegralInput.ofJacobiOneZeroLp,
VolterraIntegralInput.ofContinuousKernel, volterraIntegral_ofKernel] using
volterraIntegral_eq_zero_of_jacobiVolterraL2Operator_eq_zero_integral
K hK hM hbnd f hz hb0 hb1 x x.propertyFor a polynomial kernel with \(K(x,x)\ne 0\) on \([0,1]\), the weighted operator \(B_K\) is injective on \(L^2(\mathrm{unitJacobiMeasure}(1,0))\). In particular a zero weighted output forces a zero input. Independently of the diagonal condition, \(B_Kf=0\) forces \(V_Kf(x)=0\) throughout every \([0,b]\), \(0{\lt}b{\lt}1\).
Lean Formalisation
theorem MvPolynomial.polynomialVolterraIntegral_eq_zero_of_jacobiVolterraL2Operator_eq_zero (K : MvPolynomial (Fin 2) ℝ) {M : ℝ}
(hM : 0 ≤ M) (hbnd : ∀ z ∈ Real.volterraTriangle, |(MvPolynomial.eval z) K| ≤ M)
(f : ↥(MeasureTheory.Lp ℝ 2 (Polynomial.unitJacobiMeasure 1 0))) (hz : (K.jacobiVolterraL2Operator hM hbnd) f = 0)
{b : ℝ} (hb0 : 0 < b) (hb1 : b < 1) (x : ↑(Set.Icc 0 b)) :
Real.volterraIntegral (Real.VolterraIntegralInput.ofIntegrableOnPolynomial K ⋯ x) = 0Lean proof
/-- A zero weighted output gives a zero physical primitive on every interior interval. -/
theorem polynomialVolterraIntegral_eq_zero_of_jacobiVolterraL2Operator_eq_zero
(K : MvPolynomial (Fin 2) ℝ) {M : ℝ} (hM : 0 ≤ M)
(hbnd : ∀ z ∈ Real.volterraTriangle, |eval z K| ≤ M)
(f : Lp ℝ 2 μ) (hz : jacobiVolterraL2Operator K hM hbnd f = 0)
{b : ℝ} (hb0 : 0 < b) (hb1 : b < 1) :
∀ x : Icc (0 : ℝ) b, Real.volterraIntegral
(.ofIntegrableOnPolynomial K (integrableOn_coe_jacobiOneZeroLp f hb1) x) = 0 := by
have hz' : Real.jacobiVolterraL2Operator K.continuous_eval.continuousOn hM hbnd f = 0 := by
rwa [Real.jacobiVolterraL2Operator_polynomial]
intro x
simpa only [Real.VolterraIntegralInput.ofIntegrableOnPolynomial,
Real.VolterraIntegralInput.ofJacobiOneZeroLp,
Real.VolterraIntegralInput.ofContinuousKernel, Real.volterraIntegral_ofKernel] using
Real.volterraIntegral_eq_zero_of_jacobiVolterraL2Operator_eq_zero
(fun z ↦ eval z K) K.continuous_eval.continuousOn hM hbnd f hz' hb0 hb1 xIf \(K(x,x)\ne 0\) on \([0,1]\), the ordered operator \(A_K\) is injective on raw \(\ell ^2\). If moreover \(K(x,x)\ge a{\gt}0\) there, then \(A_K\) is invertible and its leading finite sections \(A_{K,N}=I-P_N+P_NA_KP_N\) are eventually invertible, with
No separate injectivity assumption is required.
Lean Formalisation
theorem MvPolynomial.injective_volterraPreconditionedL2 (K : MvPolynomial (Fin 2) ℝ)
(hdiag : ∀ x ∈ Set.Icc 0 1, (MvPolynomial.eval fun x_1 => x) K ≠ 0) : Function.Injective ⇑K.volterraPreconditionedL2Lean proof
/-- A nonvanishing kernel diagonal gives injectivity on the full raw coefficient space. -/
theorem injective_volterraPreconditionedL2 (K : MvPolynomial (Fin 2) ℝ)
(hdiag : ∀ x ∈ Icc (0 : ℝ) 1, eval (fun _ ↦ x) K ≠ 0) :
Function.Injective (volterraPreconditionedL2 K) := by
obtain ⟨M,hb⟩ := isCompact_volterraTriangle.exists_bound_of_continuousOn K.continuous_eval.continuousOn
have hb' : ∀ z ∈ Real.volterraTriangle, |eval z K| ≤ |M| :=
fun z hz ↦ (hb z hz).trans (le_abs_self M)
have he := jacobiVolterraL2Operator_raw_synthesis K (abs_nonneg M) hb'
intro u v huv
apply shiftedJacobiOneZeroSynthesis_injective
apply injective_jacobiVolterraL2Operator K (abs_nonneg M) hb' hdiag
have hu := congrArg (fun A ↦ A u) he
have hv := congrArg (fun A ↦ A v) he
simp only [ContinuousLinearMap.comp_apply] at hu hv
rw [← hu, ← hv, huv]Theorem 6.4.32 also covers a negative diagonal.
For a bounded projection \(P\) on a real inner-product space and a bounded operator \(A\), put \(A_P=I-P+PAP\). Then
Consequently the two sections are invertible simultaneously. On this invertible domain, \((-A)_P^{-1}(-Pg)=A_P^{-1}Pg\). For invertible \(A\), likewise \((-A)^{-1}(-g)=A^{-1}g\). For every \(A\), including singular operators and sections,
Lean Formalisation
theorem ContinuousLinearMap.coerciveFiniteSection_neg.{u_1} {E : Type u_1} [NormedAddCommGroup E] [InnerProductSpace ℝ E]
(P A : E →L[ℝ] E) (hP : P * P = P) : P.coerciveFiniteSection (-A) = (1 - 2 * P) * P.coerciveFiniteSection ALean proof
/-- Negating the resolved operator multiplies its section by the coordinate reflection. -/
theorem coerciveFiniteSection_neg (P A : E →L[ℝ] E) (hP : P*P=P) :
coerciveFiniteSection P (-A) = (1-2*P)*coerciveFiniteSection P A := by
change 1-P+P*(-A*P) = (1-2*P)*(1-P+P*(A*P))
have hPA : P*(P*(A*P)) = P*(A*P) := by rw [← mul_assoc, hP]
noncomm_ring [hP,hPA]Let \(K\) be a real polynomial kernel with \(K(x,x)\ne 0\) for all \(x\in [0,1]\). Then its raw ordered operator \(A_K\) is invertible, its leading finite sections \(A_{K,N}=I-P_N+P_NA_KP_N\) are eventually invertible, and for every raw \(\ell ^2\) right-hand side \(g\),
The real diagonal has a uniform positive bound after possibly negating \(K\), and \(A_{-K}=-A_K\). Either sign is covered, without an additional injectivity assumption.
Lean Formalisation
theorem MvPolynomial.exists_pos_volterra_diagonal_bound_or_neg (K : MvPolynomial (Fin 2) ℝ)
(hdiag : ∀ x ∈ Set.Icc 0 1, (MvPolynomial.eval fun x_1 => x) K ≠ 0) :
∃ a,
0 < a ∧
((∀ x ∈ Set.Icc 0 1, a ≤ (MvPolynomial.eval fun x_1 => x) K) ∨
∀ x ∈ Set.Icc 0 1, a ≤ -(MvPolynomial.eval fun x_1 => x) K)Lean proof
/-- A nonvanishing real diagonal has one sign and a uniform positive absolute lower bound. -/
theorem exists_pos_volterra_diagonal_bound_or_neg (K : MvPolynomial (Fin 2) ℝ)
(hdiag : ∀ x ∈ Icc (0 : ℝ) 1, eval (fun _ ↦ x) K ≠ 0) :
∃ a : ℝ, 0 < a ∧ ((∀ x ∈ Icc (0 : ℝ) 1, a ≤ eval (fun _ ↦ x) K) ∨
(∀ x ∈ Icc (0 : ℝ) 1, a ≤ -eval (fun _ ↦ x) K)) := by
let f : ℝ → ℝ := fun x ↦ eval (fun _ ↦ x) K
have hf : Continuous f := K.continuous_eval.comp (by fun_prop)
have hsign : (∀ x ∈ Icc (0 : ℝ) 1, 0 < f x) ∨ (∀ x ∈ Icc (0 : ℝ) 1, f x < 0) := by
rcases lt_or_gt_of_ne (hdiag 0 (by simp)) with hn | hp
· right
intro x hx
by_contra h
obtain ⟨y,hy,he⟩ := intermediate_value_Icc hx.1 hf.continuousOn
(show (0 : ℝ) ∈ Icc (f 0) (f x) from ⟨hn.le,le_of_not_gt h⟩)
exact hdiag y ⟨hy.1,hy.2.trans hx.2⟩ he
· left
intro x hx
by_contra h
obtain ⟨y,hy,he⟩ := intermediate_value_Icc' hx.1 hf.continuousOn
(show (0 : ℝ) ∈ Icc (f x) (f 0) from ⟨le_of_not_gt h,hp.le⟩)
exact hdiag y ⟨hy.1,hy.2.trans hx.2⟩ he
obtain ⟨t,ht,hm⟩ := isCompact_Icc.exists_isMinOn
(show (Icc (0 : ℝ) 1).Nonempty from ⟨0,by simp⟩) hf.abs.continuousOn
refine ⟨|f t|,abs_pos.mpr (hdiag t ht),?_⟩
rcases hsign with hp | hn
· left; intro x hx
have hm' : |f t| ≤ |f x| := hm hx
rwa [abs_of_pos (hp x hx)] at hm'
· right; intro x hx
have hm' : |f t| ≤ |f x| := hm hx
rwa [abs_of_neg (hn x hx)] at hm'Reference details: Weighted coefficient operator and classical solution and related results
For a real polynomial kernel \(K\), let \(A_K\) be its preconditioned coefficient operator and \(D:\ell ^2\to \ell ^2_1\) the isometric integration diagonal. Define \(W_K=DA_K\). For a kernel in the domain where \(A_K\) is invertible and weighted data \(q\in \ell ^2_1\), define \(u_K(q)=A_K^{-1}D^{-1}q\).
Lean Formalisation
def MvPolynomial.volterraWeightedL2 (K : MvPolynomial (Fin 2) ℝ) : ↥(lp (fun x => ℝ) 2) →L[ℝ] lp.FirstOrderL2Lean definition
/-- The polynomial first-kind map into its weighted coefficient range. -/
def volterraWeightedL2 (K : MvPolynomial (Fin 2) ℝ) : H →L[ℝ] lp.FirstOrderL2 :=
volterraJacobiL2Equiv.toContinuousLinearEquiv.toContinuousLinearMap.comp
(volterraPreconditionedL2 K)For every kernel in the invertible domain and every \(q\in \ell ^2_1\), \(W_Ku_K(q)=q\).
Lean Formalisation
theorem MvPolynomial.volterraWeightedSolution_property (K : Ring.InvertibleIndex MvPolynomial.volterraPreconditionedL2)
(q : lp.FirstOrderL2) : (↑K).volterraWeightedL2 (MvPolynomial.volterraWeightedSolution K q) = qLean proof
/-- The canonical weighted solution solves the equation for every invertible kernel. -/
theorem volterraWeightedSolution_property
(K : Ring.InvertibleIndex volterraPreconditionedL2) (q : lp.FirstOrderL2) :
volterraWeightedL2 K (volterraWeightedSolution K q) = q := by
have h := congrArg (fun B : H →L[ℝ] H ↦ B (volterraJacobiL2Equiv.symm q))
(Ring.inverseAt_mul volterraPreconditionedL2 K).2
change volterraPreconditionedL2 K
(Ring.inverseAt volterraPreconditionedL2 K (volterraJacobiL2Equiv.symm q)) =
volterraJacobiL2Equiv.symm q at h
change volterraJacobiL2Equiv (volterraPreconditionedL2 K
(Ring.inverseAt volterraPreconditionedL2 K (volterraJacobiL2Equiv.symm q))) = q
rw [h]
exact volterraJacobiL2Equiv.apply_symm_apply qFor a real polynomial kernel \(K\), set \(S_N(A_K)=I-P_N+P_NA_KP_N\). At a cutoff in the domain where \(S_N(A_K)\) is invertible, define \(u_{K,N}(q)=S_N(A_K)^{-1}P_ND^{-1}q\) for \(q\in \ell ^2_1\).
Lean Formalisation
def MvPolynomial.volterraWeightedSection (K : MvPolynomial (Fin 2) ℝ) (N : ℕ) :
↥(lp (fun x => ℝ) 2) →L[ℝ] ↥(lp (fun x => ℝ) 2)Lean definition
/-- The identity-padded finite weighted section. -/
def volterraWeightedSection (K : MvPolynomial (Fin 2) ℝ) (N : ℕ) : H →L[ℝ] H :=
coerciveFiniteSection (lp.initialL2Projection N) (volterraPreconditionedL2 K)At every invertible cutoff, \(u_{K,N}(q)\) has zero coefficients at indices \(i\ge N\), and \((W_Ku_{K,N}(q))_i=q_i\) for \(i{\lt}N\).
Lean Formalisation
theorem MvPolynomial.volterraWeightedFiniteSolution_equations (K : MvPolynomial (Fin 2) ℝ)
(N : Ring.InvertibleIndex K.volterraWeightedSection) (q : lp.FirstOrderL2) :
(∀ (i : ℕ), ↑N ≤ i → ↑(K.volterraWeightedFiniteSolution N q) i = 0) ∧
∀ i < ↑N, ↑(K.volterraWeightedL2 (K.volterraWeightedFiniteSolution N q)) i = ↑q iLean proof
/-- An invertible finite section solves the resolved weighted equations and has zero tail. -/
theorem volterraWeightedFiniteSolution_equations (K : MvPolynomial (Fin 2) ℝ)
(N : Ring.InvertibleIndex (volterraWeightedSection K))
(q : lp.FirstOrderL2) :
(∀ i, (N : ℕ) ≤ i → volterraWeightedFiniteSolution K N q i = 0) ∧
(∀ i, i < (N : ℕ) → (volterraWeightedL2 K (volterraWeightedFiniteSolution K N q)).1 i =
q.1 i) := by
let u := volterraWeightedFiniteSolution K N q
let P := lp.initialL2Projection (𝕜 := ℝ) N
let A := volterraPreconditionedL2 K
have he : u - P u + P (A (P u)) = P (volterraJacobiL2Equiv.symm q) := by
simpa only [u, volterraWeightedFiniteSolution_eq_ringInverse, volterraWeightedSection,
coerciveFiniteSection, mul_apply_eq_comp, add_apply, sub_apply, one_apply_eq_self, comp_apply, P, A] using
congrArg (fun B : H →L[ℝ] H ↦ B (P (volterraJacobiL2Equiv.symm q)))
(Ring.mul_inverse_cancel _ N.property)
have ht : ∀ i, (N : ℕ) ≤ i → u i = 0 := by
intro i hi
have h := congrArg (fun v : H ↦ v i) he
simpa only [lp.coeFn_add, lp.coeFn_sub, Pi.add_apply, Pi.sub_apply,
P, projection_coord, ite_eq_right (not_lt.mpr hi), sub_zero, add_zero] using h
have hp : P u = u := by
apply lp.ext
funext i
change lp.initialL2Projection N u i = u i
rw [projection_coord]
split_ifs with hi
· rfl
· exact (ht i (le_of_not_gt hi)).symm
refine ⟨ht, ?_⟩
intro i hi
rw [hp, sub_self, zero_add] at he
have h := congrArg (fun v : H ↦ v i) he
have hc : A u i = volterraJacobiL2Equiv.symm q i := by
simpa only [P, projection_coord, ite_eq_left hi] using h
change (volterraJacobiL2Equiv (A u)).1 i = q.1 i
rw [volterraJacobiL2Equiv_apply, hc]
simpa only [volterraJacobiL2Equiv_apply] using
congrArg (fun v : lp.FirstOrderL2 ↦ v.1 i)
(volterraJacobiL2Equiv.apply_symm_apply q)Write \(D:\ell ^2\to \ell ^2_1\) for the isometric integration diagonal and \(W_K=DA_K\) for the endpoint-factor-free weighted coefficient operator. For a real polynomial kernel with \(K(x,x)\ne 0\) on \([0,1]\) and any \(q\in \ell ^2_1\), the equation \(W_Ku=q\) has the unique solution \(u=A_K^{-1}D^{-1}q\). Its finite solves
are defined for every cutoff \(N\) at which \(I-P_N+P_NA_KP_N\) is invertible. These cutoffs include every sufficiently large \(N\). As \(N\to \infty \) through them, the finite solves converge to \(u\) in raw \(\ell ^2\), and their synthesized input functions converge in \(L^2(4(1-x)\, dx)\) on \([0,1]\). Whenever the section is invertible, \(u_N\) has zero tail beyond \(N\) and \((W_Ku_N)_i=q_i\) for \(i{\lt}N\); this holds eventually. For every finite coefficient vector \(c\), \(W_Kc\) agrees coefficientwise with the exact reflected Proriol assembly, so the retained finite assembly equations are precisely these weighted equations. For arbitrary raw coefficients \(v\) the full weighted residual gives
Multiplying this bound by the norm of raw Jacobi synthesis bounds the weighted physical input error. The residual includes unresolved coordinates. The output convention retains reflection and removes the endpoint factor, as in the exact assembly theorem.
Lean Formalisation
theorem MvPolynomial.volterraWeightedSolution_spec (K : MvPolynomial (Fin 2) ℝ)
(hd : ∀ x ∈ Set.Icc 0 1, (MvPolynomial.eval fun x_1 => x) K ≠ 0) (q : lp.FirstOrderL2) :
K.volterraWeightedL2 (MvPolynomial.volterraWeightedSolution ⟨K, ⋯⟩ q) = qLean proof
/-- Nonvanishing diagonal gives a solution for every weighted right-hand side. -/
theorem volterraWeightedSolution_spec (K : MvPolynomial (Fin 2) ℝ)
(hd : ∀ x ∈ Icc (0 : ℝ) 1, eval (fun _ ↦ x) K ≠ 0) (q : lp.FirstOrderL2) :
volterraWeightedL2 K (volterraWeightedSolution ⟨K, isUnit_volterraPreconditionedL2 K hd⟩ q) = q := by
have h := congrArg (fun B : H →L[ℝ] H ↦ B (volterraJacobiL2Equiv.symm q))
(Ring.mul_inverse_cancel _ (isUnit_volterraPreconditionedL2 K hd))
rw [volterraWeightedSolution_eq_ringInverse]
change volterraJacobiL2Equiv
(volterraPreconditionedL2 K (Ring.inverse (volterraPreconditionedL2 K)
(volterraJacobiL2Equiv.symm q))) = q
rw [show volterraPreconditionedL2 K (Ring.inverse (volterraPreconditionedL2 K)
(volterraJacobiL2Equiv.symm q)) = volterraJacobiL2Equiv.symm q from h]
exact volterraJacobiL2Equiv.apply_symm_apply qThe residual includes unresolved coordinates; no computable bound on the inverse norm is asserted here.
Reference details: Quantitative perturbation and stable operator families and related results
Let \(A,B\) be bounded endomorphisms of a real or complex Banach space. If \(A\) is invertible and \(\| A^{-1}\| \| A-B\| \le r{\lt}1\), then \(B\) is invertible and \(\| B^{-1}\| \le \| A^{-1}\| /(1-r)\). For invertible \(B\),
If \(A_n\) are eventually invertible with inverse norms bounded by \(C\) and \(\| A_n-B_n\| \to 0\), then \(B_n\) are eventually invertible with inverse norms bounded by \(2C\). For any eventually stable family \(B_n\), consistency \(g_n-B_nu\to 0\) implies \(B_n^{-1}g_n\to u\).
Lean Formalisation
theorem ContinuousLinearMap.isUnit_of_inverse_norm_mul_sub_lt_one.{u_1, u_2} {𝕜 : Type u_1} {E : Type u_2} [RCLike 𝕜]
[NormedAddCommGroup E] [NormedSpace 𝕜 E] [CompleteSpace E] (A B : E →L[𝕜] E) (hA : IsUnit A)
(h : ‖Ring.inverse A‖ * ‖A - B‖ < 1) : IsUnit BLean proof
/-- Small preconditioned operator errors preserve invertibility. -/
theorem isUnit_of_inverse_norm_mul_sub_lt_one (A B : E →L[𝕜] E)
(hA : IsUnit A) (h : ‖Ring.inverse A‖ * ‖A-B‖ < 1) : IsUnit B := by
have ht : ‖Ring.inverse A * (A-B)‖ < 1 := (norm_mul_le _ _).trans_lt h
have he : B = A * (1 - Ring.inverse A * (A-B)) := by
rw [mul_sub, mul_one, ← mul_assoc, Ring.mul_inverse_cancel A hA, one_mul]
abel
rw [he]
exact hA.mul (isUnit_one_sub_of_norm_lt_one ht)For the initial coordinate projections on real or complex \(\ell ^2\), write \(S_N(A)=I-P_N+P_NAP_N\). Then \(\| S_N(A)-S_N(B)\| \le \| A-B\| \). If \(B_N\to A\) in operator norm, then \(S_N(B_N)u\to Au\) for every \(u\). An eventual inverse bound \(C\) for \(S_N(A)\) transfers to an eventual bound \(2C\) for \(S_N(B_N)\). Under that stability hypothesis and \(g_N\to Au\), \(S_N(B_N)^{-1}P_Ng_N\to u\). At each invertible approximate section,
Lean Formalisation
theorem lp.norm_coerciveFiniteSection_sub_le.{u_1} {𝕜 : Type u_1} [RCLike 𝕜] (N : ℕ)
(A B : ↥(lp (fun x => 𝕜) 2) →L[𝕜] ↥(lp (fun x => 𝕜) 2)) :
‖(lp.initialL2Projection N).coerciveFiniteSection A - (lp.initialL2Projection N).coerciveFiniteSection B‖ ≤ ‖A - B‖Lean proof
/-- Double compression does not amplify operator approximation error. -/
theorem norm_coerciveFiniteSection_sub_le (N : ℕ) (A B : H →L[𝕜] H) :
‖coerciveFiniteSection (initialL2Projection N) A -
coerciveFiniteSection (initialL2Projection N) B‖ ≤ ‖A-B‖ := by
have he : coerciveFiniteSection (initialL2Projection N) A -
coerciveFiniteSection (initialL2Projection N) B =
(initialL2Projection N).comp ((A-B).comp (initialL2Projection N)) := by
simp only [coerciveFiniteSection, sub_comp, comp_sub]
abel
rw [he]
apply (opNorm_comp_le _ _).trans
calc
_ ≤ 1 * (‖A-B‖ * 1) := mul_le_mul (norm_initialL2Projection_le N)
((opNorm_comp_le _ _).trans (mul_le_mul_of_nonneg_left
(norm_initialL2Projection_le N) (norm_nonneg _))) (norm_nonneg _) zero_le_one
_ = _ := by ringWrite \(H,J\) for the reflected and raw Jacobi factors and \(K(x,y)=\sum k_{ij}x^iy^j\). Define
Then \(\| A_K\| \le m(K)\). In particular, \(m(L_N-K)\to 0\) implies \(A_{L_N}\to A_K\) in operator norm. For polynomial increments \(p_n\), if \(\sum _n m(p_n){\lt}\infty \), the operator series \(\sum _n A_{p_n}\) converges, and \(A_{\sum _{n{\lt}N}p_n}\) converges in norm to its sum.
Lean Formalisation
theorem MvPolynomial.norm_volterraPreconditionedL2_le_majorant (K : MvPolynomial (Fin 2) ℝ) :
‖K.volterraPreconditionedL2‖ ≤ K.volterraKernelMajorantLean proof
/-- The coefficient majorant bounds the preconditioned operator norm. -/
theorem norm_volterraPreconditionedL2_le_majorant (K : MvPolynomial (Fin 2) ℝ) :
‖volterraPreconditionedL2 K‖ ≤ volterraKernelMajorant K := by
apply (norm_sum_le _ _).trans
apply Finset.sum_le_sum
intro d _hd
rw [norm_smul]
apply mul_le_mul_of_nonneg_left _ (norm_nonneg _)
exact (norm_mul_le _ _).trans
(mul_le_mul (operator_pow_bound _ _) (operator_pow_bound _ _) (norm_nonneg _) (by positivity))Theorem 6.4.42 identifies the coefficient limit with the integral operator under its physical and operator-norm convergence hypotheses.
Let \(K\) be a real polynomial with \(K(x,x)\ne 0\) on \([0,1]\). The sections \(S_N(A_K)\) have a uniform eventual inverse bound, for either diagonal sign. If polynomial kernels \(L_N\) satisfy \(A_{L_N}\to A_K\) in operator norm and \(q_N\to r\) in \(\ell ^2_1\), their finite weighted solves are eventually stable and
Here the finite solves are indexed by the invertible sections, a domain containing every sufficiently large cutoff, and convergence uses its induced nontrivial filter of tails. The synthesized inputs also converge along this filter in the weighted physical Jacobi \(L^2\) space. For any polynomial \(L\), weighted data \(q,r\), and invertible section \(S_N(A_L)\),
The analogous full-solve bound omits the truncation term and uses \(\| A_L^{-1}\| \), assuming \(A_L\) invertible. Small relative kernel error \(\| A_K^{-1}\| \| A_K-A_L\| {\lt}1\) suffices for this invertibility. More generally, if \(A_{L_N}\to A\) in norm for an arbitrary invertible bounded operator \(A\), full weighted solves converge to \(A^{-1}D^{-1}r\) through the indices where \(A_{L_N}\) is invertible. This domain also contains a tail and has a nontrivial induced filter. This last assertion neither identifies a nonpolynomial integral kernel nor asserts finite-section stability for an arbitrary invertible \(A\). Reference: [Gut22, Section 2.7, Theorem 2.5 and Lemma 2.5].
Lean Formalisation
theorem MvPolynomial.exists_eventually_stable_volterraPreconditionedL2 (K : MvPolynomial (Fin 2) ℝ)
(hd : ∀ x ∈ Set.Icc 0 1, (MvPolynomial.eval fun x_1 => x) K ≠ 0) :
∃ C,
0 ≤ C ∧
∀ᶠ (N : ℕ) in Filter.atTop,
∃ (hN : IsUnit (K.volterraWeightedSection N)), ‖Ring.inverseAt K.volterraWeightedSection ⟨N, hN⟩‖ ≤ CLean proof
/-- Polynomial first-kind stability supplies genuine inverse values eventually. -/
theorem exists_eventually_stable_volterraPreconditionedL2
(K : MvPolynomial (Fin 2) ℝ)
(hd : ∀ x ∈ Icc (0 : ℝ) 1, eval (fun _ ↦ x) K ≠ 0) :
∃ C : ℝ, 0 ≤ C ∧ ∀ᶠ N in atTop,
∃ hN : IsUnit (volterraWeightedSection K N),
‖Ring.inverseAt (volterraWeightedSection K) ⟨N, hN⟩‖ ≤ C := by
obtain ⟨C, hC, hs⟩ := exists_eventually_stable_volterraPreconditionedL2_ringInverse K hd
refine ⟨C, hC, ?_⟩
filter_upwards [hs] with N hN
have hu : IsUnit (volterraWeightedSection K N) := hN.1
refine ⟨hu, ?_⟩
rw [Ring.inverseAt_eq_ringInverse]
exact hN.2Reference details: Continuous-kernel identification of raw operator limits and related results
Let \(K\) be continuous on \(\Delta \), let polynomial kernels \(p_n\) converge uniformly to \(K\), and suppose their raw preconditioned operators \(A_{p_n}\) converge in operator norm to \(A\). Then \(B_{p_n}\to B_K\) in operator norm and
where \(S\) is raw shifted-Jacobi synthesis and \(D\) the integration diagonal. In particular, for polynomial increments \(q_n\) with \(\sum _n m(q_n){\lt}\infty \) and partial sums converging uniformly to \(K\), this identity holds with \(A=\sum _n A_{q_n}\).
Lean Formalisation
theorem Real.tendsto_polynomial_jacobiVolterraL2Operator {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)) :
Filter.Tendsto (fun n => (p n).jacobiVolterraL2Operator ⋯ ⋯) Filter.atTop
(nhds (Real.jacobiVolterraL2Operator hK hM bK))Lean proof
/-- Uniform triangle approximation controls the weighted reflected operator in norm. -/
theorem tendsto_polynomial_jacobiVolterraL2Operator :
Tendsto (fun n ↦ MvPolynomial.jacobiVolterraL2Operator (p n) (hB n) (bp n))
atTop (𝓝 (jacobiVolterraL2Operator hK hM bK)) := by
rw [tendsto_iff_norm_sub_tendsto_zero]
apply squeeze_zero (fun _ ↦ norm_nonneg _) (fun n ↦ ?_) hte
rw [← jacobiVolterraL2Operator_polynomial]
exact norm_jacobiVolterraL2Operator_sub_le (p n).continuous_eval.continuousOn
(hB n) (bp n) hK hM bK (he n) (err n)Uniform physical convergence and preconditioned norm convergence are separate hypotheses; neither is silently substituted for the other.
For a real Laurent polynomial \(p\) and \(M\ge 0\), a bound \(|p(e^{it})|\le M\) on the circle gives \(\| T_p\| \le M\) on real \(\ell ^2\).
Lean Formalisation
theorem lp.norm_laurentToeplitz_le_circle {T : ℝ} [Fact (0 < T)] (p : LaurentPolynomial ℝ) {M : ℝ} (hM : 0 ≤ M)
(hb : ∀ (x : AddCircle T), ‖(AddCircle.laurentSymbol ((AddMonoidAlgebra.mapRingHom ℤ Complex.ofRealHom) p)) x‖ ≤ M) :
‖lp.laurentToeplitz p‖ ≤ MLean proof
/-- A uniform complex circle-symbol bound controls real Laurent quantization. -/
theorem norm_laurentToeplitz_le_circle {T : ℝ} [Fact (0 < T)]
(p : LaurentPolynomial ℝ) {M : ℝ} (hM : 0 ≤ M)
(hb : ∀ x : AddCircle T, ‖AddCircle.laurentSymbol (T := ⟨T, (Fact.out : 0 < T).ne'⟩)
(AddMonoidAlgebra.mapRingHom ℤ Complex.ofRealHom p) x‖ ≤ M) :
‖laurentToeplitz p‖ ≤ M := by
let q := AddMonoidAlgebra.mapRingHom ℤ Complex.ofRealHom p
have hs : ‖AddCircle.laurentSymbol (T := ⟨T, (Fact.out : 0 < T).ne'⟩) q‖ ≤ M :=
(ContinuousMap.norm_le _ hM).mpr hb
have ht := (AddCircle.norm_continuousToeplitz_le
(AddCircle.laurentSymbol (T := ⟨T, (Fact.out : 0 < T).ne'⟩) q)).trans hs
rw [AddCircle.continuousToeplitz_laurentSymbol] at ht
apply ContinuousLinearMap.opNorm_le_bound _ hM
intro u
rw [← complexifyL2.norm_map (laurentToeplitz p u), complexifyL2_laurentToeplitz]
exact ((laurentToeplitz q).le_opNorm _).trans (by
rw [complexifyL2.norm_map]
exact mul_le_mul_of_nonneg_right ht (norm_nonneg _))The norm of the Toeplitz part of a polynomial Volterra operator is bounded by a uniform bound for its diagonal \(p(x,x)\) on \([0,1]\); the same holds for differences. Hence uniform convergence \(p_n(x,x)\to K(x,x)\) gives a norm limit \(T\) of the Toeplitz parts. If also \(A_{p_n}\to A\) in norm and \(K(x,x)\ge a{\gt}0\), then \(A-T\) is compact and
Lean Formalisation
theorem MvPolynomial.norm_volterraDiagonalToeplitz_le (p : MvPolynomial (Fin 2) ℝ) {M : ℝ} (hM : 0 ≤ M)
(hb : ∀ x ∈ Set.Icc 0 1, |(MvPolynomial.eval fun x_1 => x) p| ≤ M) :
‖lp.laurentToeplitz p.volterraDiagonalLaurentSymbol‖ ≤ MLean proof
/-- The supremum bound on a polynomial diagonal controls its Toeplitz part. -/
theorem norm_volterraDiagonalToeplitz_le (p : MvPolynomial (Fin 2) ℝ)
{M : ℝ} (hM : 0 ≤ M)
(hb : ∀ x ∈ Icc (0 : ℝ) 1, |eval (fun _ ↦ x) p| ≤ M) :
‖lp.laurentToeplitz (volterraDiagonalLaurentSymbol p)‖ ≤ M := by
let : Fact (0 < (1 : ℝ)) := ⟨zero_lt_one⟩
apply lp.norm_laurentToeplitz_le_circle (T := 1) _ hM
intro x
rw [volterraDiagonalLaurentSymbol_circle, Complex.norm_real, Real.norm_eq_abs]
exact hb _ (shiftedJacobiLaurentSymbol_circle_mem_Icc (T := ⟨1, one_ne_zero⟩) x)Suppose \(K(x,x)\) is continuous and nonzero on \([0,1]\), polynomial diagonals converge uniformly to it, \(A_{p_n}\to A\) in operator norm, and \(A\) is injective. Then \(A\) is invertible and there is \(B\ge 0\) such that, eventually, \(S_N(A)=I-P_N+P_NAP_N\) is invertible and \(\| S_N(A)^{-1}\| \le B\).
Lean Formalisation
theorem MvPolynomial.isUnit_and_stable_volterra_limit (K : (Fin 2 → ℝ) → ℝ) (p : ℕ → MvPolynomial (Fin 2) ℝ)
(hK : ContinuousOn (fun x => K fun x_1 => x) (Set.Icc 0 1)) (hd : ∀ x ∈ Set.Icc 0 1, (K fun x_1 => x) ≠ 0) {e : ℕ → ℝ}
(he : ∀ (n : ℕ), 0 ≤ e n)
(herr : ∀ (n : ℕ), ∀ x ∈ Set.Icc 0 1, |(MvPolynomial.eval fun x_1 => x) (p n) - K fun x_1 => x| ≤ e n)
(hte : Filter.Tendsto e Filter.atTop (nhds 0)) (A : ↥(lp (fun x => ℝ) 2) →L[ℝ] ↥(lp (fun x => ℝ) 2))
(hA : Filter.Tendsto (fun n => (p n).volterraPreconditionedL2) Filter.atTop (nhds A)) (hinj : Function.Injective ⇑A) :
IsUnit A ∧
∃ C,
0 ≤ C ∧
∀ᶠ (N : ℕ) in Filter.atTop,
IsUnit ((lp.initialL2Projection N).coerciveFiniteSection A) ∧
‖Ring.inverse ((lp.initialL2Projection N).coerciveFiniteSection A)‖ ≤ CLean proof
/-- A continuous nonvanishing diagonal, norm consistency and injectivity give stable sections. -/
theorem isUnit_and_stable_volterra_limit
(K : (Fin 2 → ℝ) → ℝ) (p : ℕ → MvPolynomial (Fin 2) ℝ)
(hK : ContinuousOn (fun x : ℝ ↦ K (fun _ ↦ x)) (Icc 0 1))
(hd : ∀ x ∈ Icc (0 : ℝ) 1, K (fun _ ↦ x) ≠ 0)
{e : ℕ → ℝ} (he : ∀ n, 0 ≤ e n)
(herr : ∀ n x, x ∈ Icc (0 : ℝ) 1 →
|eval (fun _ ↦ x) (p n)-K (fun _ ↦ x)| ≤ e n)
(hte : Tendsto e atTop (𝓝 0))
(A : H →L[ℝ] H) (hA : Tendsto (fun n ↦ volterraPreconditionedL2 (p n)) atTop (𝓝 A))
(hinj : Function.Injective A) :
IsUnit A ∧ ∃ C : ℝ, 0 ≤ C ∧ ∀ᶠ N in atTop,
IsUnit (coerciveFiniteSection (lp.initialL2Projection N) A) ∧
‖Ring.inverse (coerciveFiniteSection (lp.initialL2Projection N) A)‖ ≤ C := by
have hb : ∃ a : ℝ, 0 < a ∧ ((∀ x ∈ Icc (0 : ℝ) 1, a ≤ K (fun _ ↦ x)) ∨
(∀ x ∈ Icc (0 : ℝ) 1, a ≤ -K (fun _ ↦ x))) := by
let f : ℝ → ℝ := fun x ↦ K (fun _ ↦ x)
have hf : ContinuousOn f (Icc 0 1) := hK
have hsign : (∀ x ∈ Icc (0 : ℝ) 1, 0 < f x) ∨ (∀ x ∈ Icc (0 : ℝ) 1, f x < 0) := by
rcases lt_or_gt_of_ne (hd 0 (by simp)) with hn | hp
· right
intro x hx
by_contra h
obtain ⟨y,hy,he⟩ := intermediate_value_Icc hx.1 (hf.mono (fun y hy ↦ ⟨hy.1,hy.2.trans hx.2⟩))
(show (0 : ℝ) ∈ Icc (f 0) (f x) from ⟨hn.le,le_of_not_gt h⟩)
exact hd y ⟨hy.1,hy.2.trans hx.2⟩ he
· left
intro x hx
by_contra h
obtain ⟨y,hy,he⟩ := intermediate_value_Icc' hx.1 (hf.mono (fun y hy ↦ ⟨hy.1,hy.2.trans hx.2⟩))
(show (0 : ℝ) ∈ Icc (f x) (f 0) from ⟨le_of_not_gt h,hp.le⟩)
exact hd y ⟨hy.1,hy.2.trans hx.2⟩ he
obtain ⟨t,ht,hm⟩ := isCompact_Icc.exists_isMinOn
(show (Icc (0 : ℝ) 1).Nonempty from ⟨0,by simp⟩) hf.abs
refine ⟨|f t|,abs_pos.mpr (hd t ht),?_⟩
rcases hsign with hp | hn
· left; intro x hx
have hm' : |f t| ≤ |f x| := hm hx
rwa [abs_of_pos (hp x hx)] at hm'
· right; intro x hx
have hm' : |f t| ≤ |f x| := hm hx
rwa [abs_of_neg (hn x hx)] at hm'
obtain ⟨a,ha,hp|hn⟩ := hb
· exact positive_limit_stable K p he herr hte A hA hinj ha hp
· have hneg : Tendsto (fun n ↦ volterraPreconditionedL2 (-p n)) atTop (𝓝 (-A)) := by
simpa only [volterraPreconditionedL2_neg] using hA.neg
obtain ⟨hu,C,hC,hs⟩ := positive_limit_stable (fun z ↦ -K z) (fun n ↦ -p n)
he (fun n x hx ↦ by simpa only [map_neg, neg_sub_neg, abs_sub_comm] using herr n x hx)
hte (-A) hneg (fun u v huv ↦ hinj (neg_injective huv)) ha hn
refine ⟨by simpa only [neg_neg] using hu.neg,C*3,by positivity,?_⟩
filter_upwards [hs] with N hN
have hiN := (isUnit_coerciveFiniteSection_neg_iff _ _
(lp.initialL2Projection_idempotent N)).mp hN.1
refine ⟨hiN,?_⟩
let P := lp.initialL2Projection (𝕜 := ℝ) N
let Q : H →L[ℝ] H := 1-2*P
have hP : P*P=P := lp.initialL2Projection_idempotent N
have hQQ : Q*Q=1 := reflection_square P hP
have hQ : IsUnit Q := isUnit_iff_exists.mpr ⟨Q,hQQ,hQQ⟩
have hQi : Ring.inverse Q = Q := by
calc
_ = Ring.inverse Q * (Q*Q) := by rw [hQQ,mul_one]
_ = Q := Ring.inverse_mul_cancel_left _ _ hQ
have hnQ : ‖Q‖ ≤ 3 := by
have heQ : Q = 1-P-P := by dsimp [Q]; noncomm_ring
rw [heQ]
have h1 := norm_sub_le (1 : H →L[ℝ] H) P
have h2 := norm_sub_le (1-P) P
have hpn := lp.norm_initialL2Projection_le (𝕜 := ℝ) N
have hon := norm_id_le (𝕜 := ℝ) (E := H)
change ‖P‖ ≤ 1 at hpn
change ‖(1 : H →L[ℝ] H)‖ ≤ 1 at hon
linarith
have hs := coerciveFiniteSection_neg P (-A) hP
rw [neg_neg] at hs
rw [hs, Ring.inverse_mul (Or.inl hQ), hQi]
exact (norm_mul_le _ _).trans (mul_le_mul hN.2 hnQ (norm_nonneg _) hC)Let \(K\) be continuous on \(\Delta \), have absolutely continuous \(y\)-slices, nonzero diagonal, and satisfy \(|\partial _yK(x,y)|\le C|K(x,x)|\) on \(\Delta \). Suppose polynomial kernels \(p_n\) converge uniformly to \(K\) and \(A_{p_n}\to A\) in operator norm. Then \(A\) is invertible and its leading sections have a uniform eventual inverse bound. For \(g_N\to g\) in raw \(\ell ^2\),
For polynomial increments \(q_n\) whose partial sums converge uniformly to \(K\), summability of \(m(q_n)\) suffices for invertibility and uniform eventual section stability of \(A=\sum _n A_{q_n}\).
Lean Formalisation
theorem Real.isUnit_and_stable_continuousVolterra {K : (Fin 2 → ℝ) → ℝ} (hK : ContinuousOn K Real.volterraTriangle) {C : ℝ}
(hAC : ∀ x ∈ Set.Icc 0 1, AbsolutelyContinuousOnInterval (fun y => K ![x, y]) 0 x)
(hder :
∀ x ∈ Set.Icc 0 1, ∃ g, ∀ᵐ (y : ℝ) ∂MeasureTheory.volume.restrict (Set.uIcc 0 x), ‖↑g.input y‖ ≤ C * |K ![x, x]|)
(hd : ∀ x ∈ Set.Icc 0 1, K ![x, x] ≠ 0) (p : ℕ → MvPolynomial (Fin 2) ℝ) {e : ℕ → ℝ} (he : ∀ (n : ℕ), 0 ≤ e n)
(herr : ∀ (n : ℕ), ∀ z ∈ Real.volterraTriangle, |(MvPolynomial.eval z) (p n) - K z| ≤ e n)
(hte : Filter.Tendsto e Filter.atTop (nhds 0)) (A : ↥(lp (fun x => ℝ) 2) →L[ℝ] ↥(lp (fun x => ℝ) 2))
(hA : Filter.Tendsto (fun n => (p n).volterraPreconditionedL2) Filter.atTop (nhds A)) :
IsUnit A ∧
∃ B,
0 ≤ B ∧
∀ᶠ (N : ℕ) in Filter.atTop,
IsUnit ((lp.initialL2Projection N).coerciveFiniteSection A) ∧
‖Ring.inverse ((lp.initialL2Projection N).coerciveFiniteSection A)‖ ≤ BLean proof
/-- A regular continuous kernel with nonvanishing diagonal gives an invertible raw limit
and uniformly stable leading sections, for either diagonal sign. -/
theorem isUnit_and_stable_continuousVolterra :
IsUnit A ∧ ∃ B : ℝ, 0 ≤ B ∧ ∀ᶠ N in atTop,
IsUnit (coerciveFiniteSection (lp.initialL2Projection N) A) ∧
‖Ring.inverse (coerciveFiniteSection (lp.initialL2Projection N) A)‖ ≤ B := by
obtain ⟨M,hb⟩ := MvPolynomial.isCompact_volterraTriangle.exists_bound_of_continuousOn hK
have bK : ∀ z ∈ volterraTriangle, |K z| ≤ |M| :=
fun z hz ↦ (hb z hz).trans (le_abs_self M)
have bp (n : ℕ) (z : Fin 2 → ℝ) (hz : z ∈ volterraTriangle) :
|MvPolynomial.eval z (p n)| ≤ |M|+e n := by
have h := abs_add_le (MvPolynomial.eval z (p n)-K z) (K z)
rw [sub_add_cancel] at h
linarith [herr n z hz,bK z hz]
have bridge := jacobiVolterraL2Operator_raw_limit hK (abs_nonneg M) bK p
(fun n ↦ add_nonneg (abs_nonneg M) (he n)) bp he herr hte A hA
have hinj : Function.Injective A := by
intro u v huv
apply shiftedJacobiOneZeroSynthesis_injective
apply injective_jacobiVolterraL2Operator K hK (abs_nonneg M) bK hAC hder hd
have hu := congrArg (fun T ↦ T u) bridge
have hv := congrArg (fun T ↦ T v) bridge
simp only [comp_apply] at hu hv
rw [← hu,← hv,huv]
have hmem (x : ℝ) (hx : x ∈ Icc (0 : ℝ) 1) :
(fun _ : Fin 2 ↦ x) ∈ volterraTriangle := ⟨hx,hx.1,le_rfl⟩
have hpair (x : ℝ) : (![x,x] : Fin 2 → ℝ) = (fun _ ↦ x) := by
funext i; fin_cases i <;> rfl
exact MvPolynomial.isUnit_and_stable_volterra_limit K p
(hK.comp (by fun_prop) hmem)
(fun x hx ↦ by simpa only [hpair] using hd x hx)
he (fun n x hx ↦ herr n _ (hmem x hx)) hte A hA hinjThese hypotheses give a sufficient nonpolynomial class; they do not assert preconditioned norm convergence for arbitrary continuous kernels.