Chebyshev-Lobatto nodes and integrated coefficient certificate
AutoSamplingTheory.TechnicalLemmas.Analysis.ChebyshevLobattoQuadrature.chebyshev_lobatto_coefficients · theorem · Teaching coverage
Mathematical statement
For natural J≥2 and real h>0, enumerate i=0,...,J-1 with Fin J and set t_i=h/2[1-cos(i*pi/(J-1))], ell_j=Lagrange.basis(univ,t,j), Lambda=sup_{s in[0,h]} sum_j |ell_j(s)|, omega_ij=integral_0^{t_i}(t_i-s)ell_j(s) ds and b_j=integral_0^h ell_j(s) ds. Each node is in[0,h], the node map is injective, and t_{J-1}=h. The cardinal identity ell_i(t_j)=1_{i=j} and the constant partition sum_j ell_j(s)=1 hold for every real s. The actual compact supremum satisfies Lambda≥1. For each i, sum_j|omega_ij|≤t_i^2*Lambda/2≤h^2*Lambda/2, and sum_j b_j=h.
Lean statement · chebyshev_lobatto_coefficients
Exact source Fin J nodes, Mathlib Lagrange basis, actual compact supremum and coefficient integrals are explicit. Consumer retains all Gaussian factors and actual output/count.
Braces mark parameters Lean can infer; square brackets request structures such as a measurable space or probability measure. Named hypotheses are mathematical premises, not facts established by this declaration. Section parameters are described in the mathematical hypotheses above; the module link retains their exact source context.
theorem chebyshev_lobatto_coefficients {J : ℕ} (hJ : 2 ≤ J) {h : ℝ} (hh : 0 < h) :
let t := fun i : Fin J => h/2*(1-Real.cos ((i : ℝ)/(J-1 : ℝ)*Real.pi))
let ell := fun j : Fin J => Lagrange.basis Finset.univ t j
let Lambda := sSup ((fun s : ℝ => ∑ j : Fin J, |(ell j).eval s|) '' Icc 0 h)
let omega := fun i j : Fin J => ∫ s in 0..t i, (t i-s)*(ell j).eval s
let momentumWeight := fun j : Fin J => ∫ s in 0..h, (ell j).eval s
(∀ i, t i ∈ Icc 0 h) ∧ Function.Injective t ∧
t ⟨J-1,by omega⟩ = h ∧
(∀ i j, (ell i).eval (t j) = if i=j then 1 else 0) ∧
(∀ s : ℝ, ∑ j : Fin J, (ell j).eval s = 1) ∧
1 ≤ Lambda ∧
(∀ i, (∑ j : Fin J, |omega i j|) ≤ (t i)^2/2*Lambda ∧
(∑ j : Fin J, |omega i j|) ≤ h^2/2*Lambda) ∧
(∑ j : Fin J, momentumWeight j) = hProof roadmap
- 1Construct distinct source nodes
Fin J index i corresponds to the paper index j=i+1. Cosine lies between minus one and one, giving 0≤t_i≤h. All cosine arguments lie in[0,pi]; cosine is injective there. Since h>0 and J-1>0, equality of nodes implies equality of arguments and indices. At the final index the argument is pi and t_{J-1}=h.
- 2Reuse actual Lagrange cardinal and constant identities
Use Mathlib Lagrange.basis at these distinct nodes. The basis equals one at its own node and zero at every other node. Mathlib sum_basis gives polynomial sum equal to one; evaluating at any real s gives the constant partition. No interpolation basis or coefficient array is supplied as a hypothesis.
- 3Make the actual supremum and regularity explicit
Each basis polynomial is continuous. The finite sum of its absolute evaluations is continuous, hence bounded above on the compact interval[0,h]. le_csSup gives the pointwise Lebesgue bound. At an actual node the absolute cardinal sum is one, yielding Lambda≥1. All subsequent coefficient integrands and absolute integrands are continuous, so their interval integrability is derived.
- 4Integrate the sharp row bound
For every i, the norm of each defining coefficient integral is at most the integral of its norm. Move the finite sum under the integral using proved interval integrability. On[0,t_i], t_i-s is nonnegative, so the absolute sum factors as (t_i-s) sum_j|ell_j(s)| and is bounded by (t_i-s)Lambda. Integrate the latter exactly to t_i^2 Lambda/2. Node range and nonnegative Lambda give the final h^2 Lambda/2 bound.
- 5Integrate the constant partition
Sum the actual b_j integrals using polynomial interval integrability. The partition identity turns the integrand into one, whose integral on[0,h] is h. This proves the total momentum weight exactly but does not prove every weight nonnegative.
Full assumptions and notation
All objects and hypotheses
- Natural J≥2, real h>0. Fin J is zero-based i=0,...,J-1, corresponding to source j=i+1.
- All nodes, real Lagrange polynomials, compact Lebesgue supremum and integral coefficients are constructed explicitly. The measure is real Lebesgue measure on the displayed closed-endpoint interval integral. Continuity and interval integrability are conclusions of polynomial regularity, not supplied extra assumptions.
Mathematical proof
1. Construct distinct source nodes
Fin J index i corresponds to the paper index j=i+1. Cosine lies between minus one and one, giving 0≤t_i≤h. All cosine arguments lie in[0,pi]; cosine is injective there. Since h>0 and J-1>0, equality of nodes implies equality of arguments and indices. At the final index the argument is pi and t_{J-1}=h.
Corresponding Lean step
nodes_mem; nodes_injective; nodes_last; Real.injOn_cos
2. Reuse actual Lagrange cardinal and constant identities
Use Mathlib Lagrange.basis at these distinct nodes. The basis equals one at its own node and zero at every other node. Mathlib sum_basis gives polynomial sum equal to one; evaluating at any real s gives the constant partition. No interpolation basis or coefficient array is supplied as a hypothesis.
Corresponding Lean step
Lagrange.eval_basis_self; Lagrange.eval_basis_of_ne; Lagrange.sum_basis; Polynomial.eval_finsetSum
3. Make the actual supremum and regularity explicit
Each basis polynomial is continuous. The finite sum of its absolute evaluations is continuous, hence bounded above on the compact interval[0,h]. le_csSup gives the pointwise Lebesgue bound. At an actual node the absolute cardinal sum is one, yielding Lambda≥1. All subsequent coefficient integrands and absolute integrands are continuous, so their interval integrability is derived.
Corresponding Lean step
Polynomial.continuous; continuous_finsetSum; IsCompact.bddAbove_image; le_csSup; Continuous.intervalIntegrable
4. Integrate the sharp row bound
For every i, the norm of each defining coefficient integral is at most the integral of its norm. Move the finite sum under the integral using proved interval integrability. On[0,t_i], t_i-s is nonnegative, so the absolute sum factors as (t_i-s) sum_j|ell_j(s)| and is bounded by (t_i-s)Lambda. Integrate the latter exactly to t_i^2 Lambda/2. Node range and nonnegative Lambda give the final h^2 Lambda/2 bound.
Corresponding Lean step
intervalIntegral.norm_integral_le_integral_norm; integral_finsetSum; integral_mono_on; integral_mul_const; integral_sub; integral_id; sq_le_sq_0
5. Integrate the constant partition
Sum the actual b_j integrals using polynomial interval integrability. The partition identity turns the integrand into one, whose integral on[0,h] is h. This proves the total momentum weight exactly but does not prove every weight nonnegative.
Corresponding Lean step
intervalIntegral.integral_finsetSum; intervalIntegral.integral_const
Lean verification
The exact proof begins folded immediately after the mathematical argument; the statement is folded beside the claim above.
Lean proof · chebyshev_lobatto_coefficients
The formula proof covers the entire current module including private node-range/injectivity/endpoint helpers for the coefficient leaf.
Braces mark parameters Lean can infer; square brackets request structures such as a measurable space or probability measure. Named hypotheses are mathematical premises, not facts established by this declaration. Section parameters are described in the mathematical hypotheses above; the module link retains their exact source context.
theorem chebyshev_lobatto_coefficients {J : ℕ} (hJ : 2 ≤ J) {h : ℝ} (hh : 0 < h) :
let t := fun i : Fin J => h/2*(1-Real.cos ((i : ℝ)/(J-1 : ℝ)*Real.pi))
let ell := fun j : Fin J => Lagrange.basis Finset.univ t j
let Lambda := sSup ((fun s : ℝ => ∑ j : Fin J, |(ell j).eval s|) '' Icc 0 h)
let omega := fun i j : Fin J => ∫ s in 0..t i, (t i-s)*(ell j).eval s
let momentumWeight := fun j : Fin J => ∫ s in 0..h, (ell j).eval s
(∀ i, t i ∈ Icc 0 h) ∧ Function.Injective t ∧
t ⟨J-1,by omega⟩ = h ∧
(∀ i j, (ell i).eval (t j) = if i=j then 1 else 0) ∧
(∀ s : ℝ, ∑ j : Fin J, (ell j).eval s = 1) ∧
1 ≤ Lambda ∧
(∀ i, (∑ j : Fin J, |omega i j|) ≤ (t i)^2/2*Lambda ∧
(∑ j : Fin J, |omega i j|) ≤ h^2/2*Lambda) ∧
(∑ j : Fin J, momentumWeight j) = h := by
classical
dsimp only
let t := nodes J h
let ell := fun j : Fin J => Lagrange.basis Finset.univ t j
let F := fun s : ℝ => ∑ j : Fin J, |(ell j).eval s|
let Lambda := sSup (F '' Icc 0 h)
have ht (i : Fin J) : t i ∈ Icc 0 h := nodes_mem hh.le i
have hinj : Function.Injective t := nodes_injective hJ hh
have hcard (i j : Fin J) : (ell i).eval (t j) = if i=j then 1 else 0 := by
by_cases he : i=j
· subst j
simpa [ell] using Lagrange.eval_basis_self (s := Finset.univ) hinj.injOn
(Finset.mem_univ i)
· simpa [ell,he] using Lagrange.eval_basis_of_ne (s := Finset.univ) (v := t) he
(Finset.mem_univ j)
have hpart (s : ℝ) : ∑ j : Fin J, (ell j).eval s = 1 := by
have he : (∑ j : Fin J, ell j) = 1 :=
Lagrange.sum_basis hinj.injOn ⟨⟨0,by omega⟩,Finset.mem_univ _⟩
simpa only [Polynomial.eval_finsetSum, Polynomial.eval_one] using
congrArg (fun p : ℝ[X] => p.eval s) he
have hF : Continuous F := by
apply continuous_finsetSum
intro j _
exact (ell j).continuous.abs
have hbound : BddAbove (F '' Icc 0 h) := isCompact_Icc.bddAbove_image hF.continuousOn
have hLeb (s : ℝ) (hs : s ∈ Icc 0 h) : F s ≤ Lambda :=
le_csSup hbound (mem_image_of_mem F hs)
have hLambda : 1 ≤ Lambda := by
let i0 : Fin J := ⟨0,by omega⟩
have hval : F (t i0) = 1 := by
simp only [F,hcard]
simp_rw [apply_ite abs,abs_one,abs_zero]
simp
exact hval ▸ hLeb (t i0) (ht i0)
have hw (i : Fin J) : (∑ j : Fin J, |∫ s in 0..t i, (t i-s)*(ell j).eval s|) ≤
(t i)^2/2*Lambda := by
have hf (j : Fin J) : Continuous (fun s : ℝ => (t i-s)*(ell j).eval s) :=
(continuous_const.sub continuous_id).mul (ell j).continuous
have hfa (j : Fin J) : Continuous (fun s : ℝ => |(t i-s)*(ell j).eval s|) := (hf j).abs
calc
_ ≤ ∑ j : Fin J, ∫ s in 0..t i, |(t i-s)*(ell j).eval s| := by
apply Finset.sum_le_sum
intro j _
simpa only [Real.norm_eq_abs] using
intervalIntegral.norm_integral_le_integral_norm (f := fun s => (t i-s)*(ell j).eval s)
(ht i).1
_ = ∫ s in 0..t i, ∑ j : Fin J, |(t i-s)*(ell j).eval s| :=
(intervalIntegral.integral_finsetSum (fun j _ => (hfa j).intervalIntegrable _ _)).symm
_ ≤ ∫ s in 0..t i, (t i-s)*Lambda := by
apply intervalIntegral.integral_mono_on (ht i).1
((continuous_finsetSum Finset.univ (fun j _ => hfa j)).intervalIntegrable _ _)
(((continuous_const.sub continuous_id).mul continuous_const).intervalIntegrable _ _)
intro s hs
have hnon : 0 ≤ t i-s := sub_nonneg.mpr hs.2
have hs' : s ∈ Icc 0 h := ⟨hs.1,hs.2.trans (ht i).2⟩
calc
_ = (t i-s)*F s := by
simp only [abs_mul,abs_of_nonneg hnon,F,Finset.mul_sum]
_ ≤ _ := mul_le_mul_of_nonneg_left (hLeb s hs') hnon
_ = (t i)^2/2*Lambda := by
rw [intervalIntegral.integral_mul_const,
intervalIntegral.integral_sub (f := fun _ : ℝ => t i) (g := fun s : ℝ => s)
(continuous_const.intervalIntegrable _ _)
(continuous_id.intervalIntegrable _ _),intervalIntegral.integral_const,
integral_id]
simp only [sub_zero]
ring
refine ⟨ht,hinj,nodes_last hJ h,hcard,hpart,hLambda,?_,?_⟩
· intro i
refine ⟨hw i,(hw i).trans ?_⟩
have hsq : (t i)^2 ≤ h^2 := sq_le_sq₀ (ht i).1 hh.le |>.mpr (ht i).2
exact mul_le_mul_of_nonneg_right (by linarith : (t i)^2/2 ≤ h^2/2)
(by linarith : 0 ≤ Lambda)
· change (∑ j : Fin J, ∫ s in 0..h, (ell j).eval s) = h
rw [← intervalIntegral.integral_finsetSum (s := Finset.univ)
(f := fun j s => (ell j).eval s)
(fun j _ => (ell j).continuous.intervalIntegrable 0 h)]
simp only [hpart,intervalIntegral.integral_const]
simp
end AutoSamplingTheory.TechnicalLemmas.Analysis.ChebyshevLobattoQuadratureScope and omitted-condition boundaries
- Exact source coefficient construction and the row/momentum-total components of B1. No input row/Lebesgue envelope. Lambda is the actual compact supremum. Nonnegative Clenshaw-Curtis momentum weights, logarithmic Lambda≤2/pi*log J+1, polynomial remainder B2, run-wide accuracy/work and main results remain independent obligations; not complete B1.
Sources, dependencies, and reuse
Source and reuse
Samplinglib parents called
Mathlib API called (external library)
- Lagrange.eval_basis_self
- Lagrange.eval_basis_of_ne
- Lagrange.sum_basis
- Real.injOn_cos
- IsCompact.bddAbove_image
- le_csSup
- intervalIntegral.integral_finsetSum
- intervalIntegral.integral_mono_on
- intervalIntegral.norm_integral_le_integral_norm
- integral_id
Mathematical sources
- SPHMC3.6 and B1 coefficient proof — Exact source coefficient construction and the row/momentum-total components of B1. No input row/Lebesgue envelope. Lambda is the actual compact supremum. Nonnegative Clenshaw-Curtis momentum weights, logarithmic Lambda<=2/pi*log J+1, polynomial remainder B2, run-wide accuracy/work and main results remain independent obligations; not complete B1.
Samplinglib prose is not a quotation or a source-equivalence certificate. Definitions and aliases are explained as constructions, not counted as new mathematical proofs.