Samplinglib mathematical lesson

ChebyshevLobattoMomentum actual source component

AutoSamplingTheory.TechnicalLemmas.Analysis.ChebyshevLobattoMomentum.momentum_absolute_sum_le · theorem · Teaching coverage

Read this first

Mathematical statement

For these actual source nodes and integral coefficients, sum_j |b_j| ≤ h*Lambda. The finite compact supremum and every needed interval integrability are derived from polynomial continuity. No b_j≥0 or supplied coefficient envelope is assumed.

\[\sum_j|b_j|\le\int_0^h\sum_j|\ell_j(s)|\,ds\le h\Lambda_J.\]

Lean statement · momentum_absolute_sum_le

Complete exact statement with all constructed source arrays, probability laws, terminal-query identities and Euclidean cost as applicable.

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.

Download module (.lean)

theorem momentum_absolute_sum_le {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)
    (∑ j : Fin J, |∫ s in 0..h, (ell j).eval s|) ≤ h*Lambda

Exact module and namespace context

Proof roadmap

1Bound the actual compact supremum
The basis polynomials are continuous. Thus F(s)=sum|ell_j(s)| is continuous and bounded above on[0,h]. The defining supremum bounds every F(s) on that interval. All basis and absolute-basis functions are interval integrable by continuity.
2Sum absolute defining integrals
Bound each absolute integral by its norm integral. Use derived interval integrability to move the finite sum inside the integral. Integrate F≤Lambda over the positive ordered interval. No source-prose positivity assertion is imported as a premise.

Full assumptions and notation

All objects and hypotheses

J is a natural number≥2 and h is a positive real. Fin J uses indices i=0,...,J-1 corresponding to source j=i+1.
t_i=h/2[1-cos(i*pi/(J-1))]; ell_j is the real Mathlib Lagrange cardinal polynomial at those nodes; Lambda is the actual supremum of sum_j|ell_j(s)| on the compact interval[0,h]; b_j=integral_0^h ell_j(s) ds using real Lebesgue measure.

Mathematical proof

1. Bound the actual compact supremum

The basis polynomials are continuous. Thus F(s)=sum|ell_j(s)| is continuous and bounded above on[0,h]. The defining supremum bounds every F(s) on that interval. All basis and absolute-basis functions are interval integrable by continuity.

\[F(s)\le\sup_{u\in[0,h]}F(u)=\Lambda_J.\]

Corresponding Lean step

Polynomial.continuous; IsCompact.bddAbove_image; le_csSup; Continuous.intervalIntegrable

2. Sum absolute defining integrals

Bound each absolute integral by its norm integral. Use derived interval integrability to move the finite sum inside the integral. Integrate F≤Lambda over the positive ordered interval. No source-prose positivity assertion is imported as a premise.

\[\sum_j|b_j|\le\int_0^h\sum_j|\ell_j(s)|\,ds\le h\Lambda_J.\]

Corresponding Lean step

intervalIntegral.norm_integral_le_integral_norm; integral_finsetSum; integral_mono_on; integral_const

Lean verification

The exact proof begins folded immediately after the mathematical argument; the statement is folded beside the claim above.

Lean proof · momentum_absolute_sum_le

Entire current module is covered, including private phase, finite weighted difference, measurability, actual kernel and transport helpers. Extraction carries no new mathematical credit.

Download module (.lean)

theorem momentum_absolute_sum_le {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)
    (∑ j : Fin J, |∫ s in 0..h, (ell j).eval s|) ≤ h*Lambda := by
  classical
  dsimp only
  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 F := fun s : ℝ => ∑ j : Fin J, |(ell j).eval s|
  let Lambda := sSup (F '' Icc 0 h)
  have hF : Continuous F := continuous_finsetSum Finset.univ
    (fun j _ => (ell j).continuous.abs)
  have hbound : BddAbove (F '' Icc 0 h) := isCompact_Icc.bddAbove_image hF.continuousOn
  calc
    _ ≤ ∑ j : Fin J, ∫ s in 0..h, |(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 => (ell j).eval s) hh.le
    _ = ∫ s in 0..h, F s := by
      exact (intervalIntegral.integral_finsetSum
        (fun j _ => (ell j).continuous.abs.intervalIntegrable _ _)).symm
    _ ≤ ∫ s in 0..h, Lambda := by
      apply intervalIntegral.integral_mono_on hh.le (hF.intervalIntegrable _ _)
        (continuous_const.intervalIntegrable _ _)
      intro s hs
      exact le_csSup hbound (mem_image_of_mem F hs)
    _ = h*Lambda := by simp

end AutoSamplingTheory.TechnicalLemmas.Analysis.ChebyshevLobattoMomentum

Exact module and namespace context

Scope and omitted-condition boundaries

Derived absolute-integral prerequisite for Appendix D1/D2 using the actual B1 coefficients. This does not prove individual Clenshaw-Curtis weight nonnegativity, logarithmic Lambda, complete B1, interpolation remainder B2 or either main theorem.

Sources, dependencies, and reuse

Source and reuse

Samplinglib parents called

Mathlib API called (external library)

Polynomial.continuous
IsCompact.bddAbove_image
le_csSup
intervalIntegral.integral_finsetSum
intervalIntegral.norm_integral_le_integral_norm
intervalIntegral.integral_mono_on

Mathematical sources

SPHMC proximal phase and coefficient prerequisites — Derived absolute-integral prerequisite for Appendix D1/D2 using the actual B1 coefficients. This does not prove individual Clenshaw-Curtis weight nonnegativity, logarithmic Lambda, complete B1, interpolation remainder B2 or either main theorem.

Samplinglib prose is not a quotation or a source-equivalence certificate. Definitions and aliases are explained as constructions, not counted as new mathematical proofs.