Keyboard shortcuts

Press ← or → to navigate between chapters

Press ? to show this help

Press Esc to hide this help

bibkey: tan2026coefficientonenorm authors: Jiyuan Tan year: 2026 title: Causalean polynomial coefficient one-norm doi: null url: https://github.com/Jiyuan-Tan/CausalSmith/tree/e56c1daecf6fc95cad721ff71d188e8fc526cbca/Causalean/Mathlib/Analysis/Approximation/Chebyshev claim: The coefficient one-norm, its triangle inequality, homogeneity and submultiplicativity. strata_touched: [] license: citation-only triage: anchor

Causalean polynomial coefficient one-norm

The leaf proofs in TrigExtraction.lean and PolynomialOneNorm.lean supply the sum of absolute monomial coefficients and its elementary norm identities. UniformCoefficientBudget adapts those source portions with direct support-sum and monomial APIs.

The immutable source revision is e56c1daecf6fc95cad721ff71d188e8fc526cbca. The Apache-2.0 license and upstream NOTICE are retained at docs/reports/interpolation-suppliers/Causalean-LICENSE.txt and Causalean-NOTICE.txt. These licensed leaf results do not supply the arbitrary-node smooth interpolation budget or the joint Laplace endpoint bounds.

Verified locator

  • URL: https://github.com/Jiyuan-Tan/CausalSmith/tree/e56c1daecf6fc95cad721ff71d188e8fc526cbca/Causalean/Mathlib/Analysis/Approximation/Chebyshev
  • Commit: e56c1daecf6fc95cad721ff71d188e8fc526cbca, authored and committed by Jiyuan-Tan on 2026-10-08 at 22:39:02 UTC.
  • Source files: TrigExtraction.lean and PolynomialOneNorm.lean in the pinned directory.

The pinned GitHub tree returned HTTP 200 on 2026-10-11 UTC and lists both source files. GitHub’s commit API confirms the full revision, author and commit timestamp. Locator verification identifies the immutable source tree; it does not independently validate the Lean proofs.