Commit 2023-12-27 18:34 98e2ce28

View on Github →

archive: smooth functions whose integral calculates the values of polynomials (#9138) Test case of the library suggested by Martin Hairer, see https://leanprover.zulipchat.com/#narrow/stream/116395-maths/topic/Hairer.20challenge/near/404836147.

Estimated changes

Modified Archive.lean

Created Archive/Hairer.lean

added def L

added theorem MvPolynomial.continuous_eval

added theorem SmoothSupportedOn.coe_mk

added theorem SmoothSupportedOn.contDiff

added theorem SmoothSupportedOn.continuous

added theorem SmoothSupportedOn.hasCompactSupport

added theorem SmoothSupportedOn.integrable_eval_mul

added theorem SmoothSupportedOn.support_subset

added theorem SmoothSupportedOn.tsupport_subset

added def SmoothSupportedOn

added theorem hairer

added theorem inj_L

Modified Mathlib.lean

Created Mathlib/Analysis/Analytic/Polynomial.lean

added theorem AnalyticAt.aeval_mvPolynomial

added theorem AnalyticAt.aeval_polynomial

added theorem AnalyticOn.aeval_mvPolynomial

added theorem AnalyticOn.aeval_polynomial

added theorem AnalyticOn.eval_continuousLinearMap'

added theorem AnalyticOn.eval_continuousLinearMap

added theorem AnalyticOn.eval_linearMap'

added theorem AnalyticOn.eval_linearMap

added theorem AnalyticOn.eval_mvPolynomial

added theorem AnalyticOn.eval_polynomial

Modified Mathlib/RingTheory/MvPolynomial/Basic.lean

added def MvPolynomial.basisRestrictSupport

added def MvPolynomial.restrictSupport

added theorem MvPolynomial.restrictSupport_mono

modified def MvPolynomial.restrictTotalDegree

added theorem MvPolynomial.restrictTotalDegree_le_restrictDegree