ChebyshevLobattoMomentum actual source component
AutoSamplingTheory.TechnicalLemmas.Analysis.ChebyshevLobattoMomentum.momentum_absolute_sum_le · theorem · Teaching coverage
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.
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.
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*LambdaProof 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.
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.
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.
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 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.ChebyshevLobattoMomentumSource assumptions versus formal assumptions
| Source | Actual Lean | Difference kind | Why it matters |
|---|---|---|---|
| Source uses normalized Euclidean strongly convex C2 potential and true Euclidean phase distance. | 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. | same | The abstract shared implication is an explicit prerequisite; paper consumer supplies its exact Hessian hypotheses. Main uses finite real inner-product coordinates and explicitly sqrt(sum squares), never default product max norm. |
| D2 gives universal C Lambda h delta under h²Lambda<=1 for arbitrary measurable delta-accurate oracle delta>=0; B1 includes further positivity/logarithmic claims. | 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. | unresolved | Only D1/D2 one-phase comparison or a named prerequisite is asserted. Absolute-b proof is a faithful universal-constant route adapter, not a source assumption repair or completed B1. |
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.
Encoder–denoiser: accepted · equivalent-after-elaboration
A generalization is not a source correction. Proposed missing conditions require separate independent repair review. No proposed repair silently changes the original theorem.
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.