def IsPolynomialOn (a b : ℝ) (f : ↑(Set.Icc a b) → ℝ) : Prop

Definition 3.12: Let a,b ∈ ℝ with a ≤ b. A polynomial on [a,b] is a function f : [a,b] → ℝ for which there exist n ≥ 0 and coefficients c₀, …, cₙ ∈ ℝ such that f(x) = ∑_{i=0}^n cᵢ x^i for all x ∈ [a,b]. If f is a polynomial and n is the largest index with cₙ ≠ 0, then n is called the degree of f.

Equations

• IsPolynomialOn a b f = (a ≤ b ∧ ∃ (p : Polynomial ℝ), ∀ (x : ↑(Set.Icc a b)), f x = Polynomial.eval (↑x) p)

def IsPolynomialDegreeOn (a b : ℝ) (f : ↑(Set.Icc a b) → ℝ) (n : ℕ) : Prop

A natural number n is the degree of f on [a,b] if f agrees on [a,b] with a nonzero real polynomial of natDegree n.

Equations

• IsPolynomialDegreeOn a b f n = (a ≤ b ∧ ∃ (p : Polynomial ℝ), (∀ (x : ↑(Set.Icc a b)), f x = Polynomial.eval (↑x) p) ∧ p.natDegree = n ∧ p.coeff n ≠ 0)

def examplePolynomialFunctionOnIcc : ↑(Set.Icc 1 2) → ℝ

The specific function x ↦ 3x^4 + 2x^3 - 4x + 5 on [1,2].

Equations

• examplePolynomialFunctionOnIcc x = 3 * ↑x ^ 4 + 2 * ↑x ^ 3 - 4 * ↑x + 5

theorem helperForExample_3_8_2_eval_witness (x : ↑(Set.Icc 1 2)) : examplePolynomialFunctionOnIcc x = Polynomial.eval (↑x) (3 * Polynomial.X ^ 4 + 2 * Polynomial.X ^ 3 - 4 * Polynomial.X + 5)

Helper for Example 3.8.2: evaluation of the witness polynomial equals the given function.

theorem helperForExample_3_8_2_natDegree_witness : (3 * Polynomial.X ^ 4 + 2 * Polynomial.X ^ 3 - 4 * Polynomial.X + 5).natDegree = 4

Helper for Example 3.8.2: the witness polynomial has natDegree 4.

theorem helperForExample_3_8_2_coeff4_witness_ne_zero : (3 * Polynomial.X ^ 4 + 2 * Polynomial.X ^ 3 - 4 * Polynomial.X + 5).coeff 4 ≠ 0

Helper for Example 3.8.2: the witness polynomial has nonzero coefficient at index 4.

theorem example_3_8_2 : IsPolynomialDegreeOn 1 2 examplePolynomialFunctionOnIcc 4

Example 3.8.2: The function f(x) = 3x^4 + 2x^3 - 4x + 5 on [1,2] is a polynomial of degree 4.

def polynomialFunctionsOnIcc (a b : ℝ) : Set (BoundedContinuousFunction ↑(Set.Icc a b) ℝ)

The set of bounded continuous functions on [a,b] that are polynomial on [a,b].

Equations

• polynomialFunctionsOnIcc a b = {f : BoundedContinuousFunction ↑(Set.Icc a b) ℝ | IsPolynomialOn a b ⇑f}

theorem helperForText_3_8_1_polynomial_bcf_mem (a b : ℝ) (h : a ≤ b) (p : Polynomial ℝ) : BoundedContinuousFunction.mkOfCompact (p.toContinuousMapOn (Set.Icc a b)) ∈ polynomialFunctionsOnIcc a b

Helper for Text 3.8.1: a polynomial bundled as a bounded continuous function belongs to polynomialFunctionsOnIcc.

theorem helperForText_3_8_1_dist_mkOfCompact_lt (a b ε : ℝ) (f : BoundedContinuousFunction ↑(Set.Icc a b) ℝ) (p : Polynomial ℝ) (hnorm : ‖p.toContinuousMapOn (Set.Icc a b) - f.toContinuousMap‖ < ε) : dist (BoundedContinuousFunction.mkOfCompact (p.toContinuousMapOn (Set.Icc a b))) f < ε

Helper for Text 3.8.1: a sup-norm estimate in C([a,b], ℝ) transfers to a distance estimate in BoundedContinuousFunction (Set.Icc a b) ℝ.

theorem helperForText_3_8_1_exists_polynomial_in_ball (a b : ℝ) (h : a ≤ b) (f : BoundedContinuousFunction ↑(Set.Icc a b) ℝ) (ε : ℝ) (hε : 0 < ε) : ∃ g ∈ polynomialFunctionsOnIcc a b, dist g f < ε

Helper for Text 3.8.1: every open ball around a bounded continuous function on [a,b] contains a polynomial function.

theorem polynomialFunctionsOnIcc_dense (a b : ℝ) (h : a ≤ b) : Dense (polynomialFunctionsOnIcc a b)

Text 3.8.1: (Weierstrass approximation in closure form) For a closed interval [a,b], the set of polynomial functions on [a,b] is dense (with respect to the uniform norm) in the space of continuous functions on [a,b].

theorem helperForText_3_8_2_eventually_halfExp_le_absDiff (p : Polynomial ℝ) : ∀ᶠ (x : ℝ) in Filter.atTop, Real.exp x / 2 ≤ |Real.exp x - Polynomial.eval x p|

Helper for Text 3.8.2: for each polynomial, eventually |exp x - p(x)| is at least exp x / 2.

theorem helperForText_3_8_2_eventually_gt_anyBound_absDiff (p : Polynomial ℝ) (M : ℝ) : ∀ᶠ (x : ℝ) in Filter.atTop, M < |Real.exp x - Polynomial.eval x p|

Helper for Text 3.8.2: for each polynomial and each real bound M, eventually |exp x - p(x)| is larger than M.

theorem helperForText_3_8_2_iSup_eq_top_absDiff (p : Polynomial ℝ) : ⨆ (x : ℝ), ↑|Real.exp x - Polynomial.eval x p| = ⊤

Helper for Text 3.8.2: the WithTop supremum of |exp x - p(x)| over ℝ is ⊤.

theorem helperForText_3_8_2_uniformly_convergent_sequence_has_global_bound (p : ℕ → Polynomial ℝ) (hConv : TendstoUniformly (fun (n : ℕ) (x : ℝ) => Polynomial.eval x (p n)) Real.exp Filter.atTop) : ∃ (N : ℕ), ∀ (x : ℝ), |Real.exp x - Polynomial.eval x (p N)| < 1

Helper for Text 3.8.2: uniform convergence of a polynomial sequence to exp forces one polynomial in the sequence to be globally within 1.

theorem failure_uniform_polynomial_approximation_real_exp : (∀ (p : Polynomial ℝ), ⨆ (x : ℝ), ↑|Real.exp x - Polynomial.eval x p| = ⊤) ∧ ¬∃ (p : ℕ → Polynomial ℝ), TendstoUniformly (fun (n : ℕ) (x : ℝ) => Polynomial.eval x (p n)) Real.exp Filter.atTop

Text 3.8.2: [Failure of uniform polynomial approximation on ℝ] Continuous functions on ℝ cannot, in general, be uniformly approximated by polynomials. In particular, for f(x)=e^x and for every polynomial p, one has sup_{x∈ℝ} |e^x - p(x)| = +∞; hence there is no sequence of polynomials (p_n) such that p_n → e^x uniformly on ℝ.

theorem helperForTheorem_3_11_polynomial_near_bundled_map (a b ε : ℝ) (f : ↑(Set.Icc a b) → ℝ) (hf : Continuous f) (hε : 0 < ε) : ∃ (p : Polynomial ℝ), ‖p.toContinuousMapOn (Set.Icc a b) - { toFun := f, continuous_toFun := hf }‖ < ε

Helper for Theorem 3.11: obtain a polynomial whose bundled map is within ε in sup norm.

theorem helperForTheorem_3_11_pointwise_lt_of_supnorm_lt (a b ε : ℝ) (F G : C(↑(Set.Icc a b), ℝ)) (hFG : ‖F - G‖ < ε) (x : ↑(Set.Icc a b)) : |F x - G x| < ε

Helper for Theorem 3.11: a sup-norm bound between bundled maps implies pointwise bounds.

theorem helperForTheorem_3_11_eval_form_and_weakening (a b ε : ℝ) (f : ↑(Set.Icc a b) → ℝ) (hf : Continuous f) (p : Polynomial ℝ) (hpoint : ∀ (x : ↑(Set.Icc a b)), |(p.toContinuousMapOn (Set.Icc a b) - { toFun := f, continuous_toFun := hf }) x| < ε) (x : ↑(Set.Icc a b)) : |Polynomial.eval (↑x) p - f x| ≤ ε

Helper for Theorem 3.11: rewrite evaluation form and weaken < ε to ≤ ε.

theorem weierstrassApproximationOnIcc (a b : ℝ) (h : a < b) (f : ↑(Set.Icc a b) → ℝ) (hf : Continuous f) (ε : ℝ) : ε > 0 → ∃ (p : Polynomial ℝ), ∀ (x : ↑(Set.Icc a b)), |Polynomial.eval (↑x) p - f x| ≤ ε

Theorem 3.11 (Weierstrass approximation theorem): Let a < b and let f : [a,b] → ℝ be continuous. For every ε > 0 there exists a real polynomial P such that |P(x) - f(x)| ≤ ε for all x ∈ [a,b]. Equivalently, the closure of the polynomial functions on [a,b] in the uniform metric is the set of all continuous functions on [a,b].

def IsSupportedOnIcc (a b : ℝ) (f : ℝ → ℝ) : Prop

A function f : ℝ → ℝ is supported on [a,b] if a ≤ b and f(x) = 0 for all x ∈ ℝ \ [a,b].

Equations

• IsSupportedOnIcc a b f = (a ≤ b ∧ ∀ x ∉ Set.Icc a b, f x = 0)

theorem helperForTheorem_3_12_restrict_continuousOnIcc01 (f : ℝ → ℝ) (hf : Continuous f) : Continuous fun (x : ↑(Set.Icc 0 1)) => f ↑x

Helper for Theorem 3.12: the restriction of a continuous real function to [0,1] is continuous.

theorem helperForTheorem_3_12_exists_polynomial_onIcc01 (f : ℝ → ℝ) (hf : Continuous f) (ε : ℝ) : ε > 0 → ∃ (p : Polynomial ℝ), ∀ (x : ↑(Set.Icc 0 1)), |Polynomial.eval (↑x) p - (fun (y : ↑(Set.Icc 0 1)) => f ↑y) x| ≤ ε

Helper for Theorem 3.12: instantiate Weierstrass approximation on [0,1] for the restricted function.

theorem helperForTheorem_3_12_rewrite_restricted_value (f : ℝ → ℝ) (p : Polynomial ℝ) (x : ↑(Set.Icc 0 1)) : |Polynomial.eval (↑x) p - (fun (y : ↑(Set.Icc 0 1)) => f ↑y) x| = |Polynomial.eval (↑x) p - f ↑x|

Helper for Theorem 3.12: simplify the restricted-function value at a point of [0,1] in the approximation expression.

theorem weierstrassApproximation_supportedOnIcc01 (f : ℝ → ℝ) (hf : Continuous f) (hfs : IsSupportedOnIcc 0 1 f) (ε : ℝ) : ε > 0 → ∃ (p : Polynomial ℝ), ∀ (x : ↑(Set.Icc 0 1)), |Polynomial.eval (↑x) p - f ↑x| ≤ ε

Theorem 3.12: [Weierstrass approximation theorem I] Let f : ℝ → ℝ be continuous and supported on [0,1], i.e. f(x)=0 for all x ∉ [0,1]. Then for every ε > 0 there exists a polynomial p ∈ ℝ[x] such that |p(x) - f(x)| ≤ ε for all x ∈ [0,1].

def IsCompactlySupported (f : ℝ → ℝ) : Prop

Definition 3.13: [Compactly supported functions] A function f : ℝ → ℝ is supported on a closed interval [a,b] if it vanishes outside [a,b]; it is compactly supported if there exist real numbers a ≤ b such that f is supported on [a,b]. If f is continuous and supported on [a,b], define ∫_{-∞}^{∞} f(x) dx := ∫_a^b f(x) dx.

Equations

• IsCompactlySupported f = ∃ (a : ℝ) (b : ℝ), IsSupportedOnIcc a b f

noncomputable def compactSupportIntegral (a b : ℝ) (f : ℝ → ℝ) : ℝ

The integral over ℝ of a function supported on [a,b], defined as the interval integral over [a,b].

Equations

• compactSupportIntegral a b f = ∫ (x : ℝ) in a..b, f x

theorem helperForLemma_3_1_leftEndpoint_zero_of_supported {f : ℝ → ℝ} (hf : Continuous f) {a b : ℝ} (hab : IsSupportedOnIcc a b f) : f a = 0

Helper for Lemma 3.1: a continuous function supported on [a,b] vanishes at a.

theorem helperForLemma_3_1_rightEndpoint_zero_of_supported {f : ℝ → ℝ} (hf : Continuous f) {a b : ℝ} (hab : IsSupportedOnIcc a b f) : f b = 0

Helper for Lemma 3.1: a continuous function supported on [a,b] vanishes at b.

theorem helperForLemma_3_1_support_subset_Ioc_of_supported {f : ℝ → ℝ} (hf : Continuous f) {a b : ℝ} (hab : IsSupportedOnIcc a b f) : Function.support f ⊆ Set.Ioc a b

Helper for Lemma 3.1: support of a continuous function supported on [a,b] lies in Set.Ioc a b.

theorem integral_eq_of_supported_on_two_Icc (f : ℝ → ℝ) (hf : Continuous f) (a b c d : ℝ) (hab : IsSupportedOnIcc a b f) (hcd : IsSupportedOnIcc c d f) : ∫ (x : ℝ) in a..b, f x = ∫ (x : ℝ) in c..d, f x

Lemma 3.1: If a continuous function is supported on both [a,b] and [c,d] (i.e. it vanishes outside each interval), then the interval integrals agree.

def IsApproximationToIdentity (ε δ : ℝ) (f : ℝ → ℝ) : Prop

Definition 3.14: [Approximation to the identity] Let ε > 0 and 0 < δ < 1. A function f : ℝ → ℝ is an (ε,δ)-approximation to the identity if (1) supp f ⊆ [-1,1] and f(x) ≥ 0 for all x, (2) f is continuous on ℝ and ∫_{-∞}^{∞} f(x) dx = 1, and (3) for δ ≤ |x| ≤ 1, one has |f(x)| ≤ ε.

Equations

• One or more equations did not get rendered due to their size.

theorem exists_polynomial_approximate_identity (ε δ : ℝ) (hε : 0 < ε) (hδ : 0 < δ) (hδ' : δ < 1) : ∃ (p : Polynomial ℝ), ∀ x ∈ Set.Icc (-1) (-δ) ∪ Set.Icc δ 1, |Polynomial.eval x p - x| ≤ ε

Lemma 3.2: [Polynomials can approximate the identity] For every ε > 0 and every δ with 0 < δ < 1, there exists a real polynomial P such that |P(x) - x| ≤ ε for all x ∈ [-1,-δ] ∪ [δ,1]; in particular, such P gives an (ε,δ)-approximation to the identity on [-1,1].

noncomputable def realConvolution (f g : { f : ℝ → ℝ // Continuous f ∧ IsCompactlySupported f }) : ℝ → ℝ

Definition 3.15: [Convolution] Let f,g : ℝ → ℝ be continuous with compact support. The convolution f*g is the function x ↦ ∫ y, f y * g (x - y).

Equations

• realConvolution f g x = ∫ (y : ℝ), ↑f y * ↑g (x - y)

noncomputable def realConvolutionFun (f g : ℝ → ℝ) : ℝ → ℝ

Convolution of two real functions, defined by (f*g)(x) = ∫ t, f (x - t) * g t.

Equations

• realConvolutionFun f g x = ∫ (t : ℝ), f (x - t) * g t

theorem convolution_polynomial_on_Icc (f g : ℝ → ℝ) (hf : Continuous f) (hg : Continuous g) (hfs : IsSupportedOnIcc 0 1 f) (hgs : IsSupportedOnIcc (-1) 1 g) (hgp : ∃ (n : ℕ) (p : Polynomial ℝ), p.natDegree ≤ n ∧ ∀ x ∈ Set.Icc (-1) 1, g x = Polynomial.eval x p) : ∃ (n : ℕ) (q : Polynomial ℝ), q.natDegree ≤ n ∧ ∀ x ∈ Set.Icc 0 1, realConvolutionFun f g x = Polynomial.eval x q

Lemma 3.3: Let f : ℝ → ℝ be continuous with support in [0,1] and let g : ℝ → ℝ be continuous with support in [-1,1]. If there exist n ≥ 0 and real coefficients so that g agrees with a polynomial of degree at most n on [-1,1], then the convolution f*g is a polynomial of degree at most n on [0,1] (in particular, it is a polynomial on [0,1]).

theorem convolution_approx_identity_bound (f g : ℝ → ℝ) (hf : Continuous f) (hfs : IsSupportedOnIcc 0 1 f) (M : ℝ) (hM : 0 < M) (hbound : ∀ (x : ℝ), |f x| ≤ M) (ε δ : ℝ) (hε : 0 < ε) (hδ : 0 < δ) (hδ' : δ < 1) (hmod : ∀ (x y : ℝ), |x - y| < δ → |f x - f y| < ε) (hg_integrable : MeasureTheory.Integrable g MeasureTheory.volume) (hg_one : ∫ (t : ℝ), g t = 1) (hg_nonneg : ∀ (t : ℝ), 0 ≤ g t) (hg_tail : ∫ (t : ℝ) in {t : ℝ | |t| ≥ δ}, |g t| < ε) (x : ℝ) : x ∈ Set.Icc 0 1 → |realConvolutionFun f g x - f x| ≤ (1 + 4 * M) * ε

Lemma 3.4: Let f : ℝ → ℝ be continuous, supported on [0,1], and bounded by M > 0, with |f x| ≤ M for all x. Let ε > 0 and 0 < δ < 1 be such that |f x - f y| < ε whenever |x - y| < δ. Let g satisfy (1) g is integrable and ∫ t, g t = 1, (2) g is nonnegative, and (3) ∫ t in {t | |t| ≥ δ}, |g t| < ε. Then for every x ∈ [0,1], |(f*g)(x) - f(x)| ≤ (1 + 4M) ε.

theorem helperForProposition_3_23_realConvolutionFun_eq_star (u v : ℝ → ℝ) : realConvolutionFun u v = MeasureTheory.convolution u v (ContinuousLinearMap.mul ℝ ℝ) MeasureTheory.volume

Helper for Proposition 3.23: rewrite realConvolutionFun as a mathlib convolution.

theorem helperForProposition_3_23_supportSubsetIcc_of_IsCompactlySupported (u : ℝ → ℝ) (hu : IsCompactlySupported u) : ∃ (a : ℝ) (b : ℝ), a ≤ b ∧ Function.support u ⊆ Set.Icc a b

Helper for Proposition 3.23: extract interval support bounds from compact support.

theorem helperForProposition_3_23_hasCompactSupport_of_IsCompactlySupported (u : ℝ → ℝ) (hu : IsCompactlySupported u) : HasCompactSupport u

Helper for Proposition 3.23: custom compact support implies HasCompactSupport.

theorem helperForProposition_3_23_isCompactlySupported_convolutionFun (u v : ℝ → ℝ) (hu : IsCompactlySupported u) (hv : IsCompactlySupported v) : IsCompactlySupported (realConvolutionFun u v)

Helper for Proposition 3.23: convolution of compactly supported functions is compactly supported in the textbook interval-support sense.

theorem helperForProposition_3_23_convolution_add_right (u v w : ℝ → ℝ) (hu : Continuous u) (hv : Continuous v) (hw : Continuous w) (hvs : IsCompactlySupported v) (hws : IsCompactlySupported w) (x : ℝ) : realConvolutionFun u (fun (t : ℝ) => v t + w t) x = realConvolutionFun u v x + realConvolutionFun u w x

Helper for Proposition 3.23: right-additivity of convolution under continuity and compact support hypotheses.

theorem convolution_basic_properties (f g h : ℝ → ℝ) (hf : Continuous f) (hg : Continuous g) (hh : Continuous h) (hfs : IsCompactlySupported f) (hgs : IsCompactlySupported g) (hhs : IsCompactlySupported h) : (Continuous (realConvolutionFun f g) ∧ IsCompactlySupported (realConvolutionFun f g)) ∧ (∀ (x : ℝ), realConvolutionFun f g x = realConvolutionFun g f x) ∧ (∀ (x : ℝ), realConvolutionFun f (fun (t : ℝ) => g t + h t) x = realConvolutionFun f g x + realConvolutionFun f h x) ∧ ∀ (c x : ℝ), realConvolutionFun f (fun (t : ℝ) => c * g t) x = realConvolutionFun (fun (t : ℝ) => c * f t) g x ∧ realConvolutionFun f (fun (t : ℝ) => c * g t) x = c * realConvolutionFun f g x

Proposition 3.23: (Basic properties of convolution) Let f,g,h : ℝ → ℝ be continuous functions with compact support, and define (f*g)(x) = ∫ t, f (x - t) * g t. Then: (1) f*g is continuous and has compact support; (2) (Commutativity) for all x, (f*g)(x) = (g*f)(x); (3) (Linearity) for all x, (f*(g+h))(x) = (f*g)(x) + (f*h)(x), and for any c and all x, (f*(c g))(x) = ((c f)*g)(x) = c (f*g)(x).

def ConvolutionDefined (f g : ℝ → ℝ) : Prop

The convolution of f and g is absolutely convergent at every point.

Equations

• ConvolutionDefined f g = ∀ (x : ℝ), MeasureTheory.Integrable (fun (t : ℝ) => f (x - t) * g t) MeasureTheory.volume

noncomputable def diracDelta : ℝ → ℝ

A formal Dirac delta distribution, treated as a function for convolution statements.

Equations

• diracDelta x = if x = 0 then 1 else 0

theorem diagnostic_diracDelta_ae_zero : (fun (t : ℝ) => diracDelta t) =ᵐ[MeasureTheory.volume] fun (x : ℝ) => 0

diracDelta is equal almost everywhere to 0 for Lebesgue measure on ℝ.

theorem diagnostic_diracDelta_shift_ae_zero (x : ℝ) : (fun (t : ℝ) => diracDelta (x - t)) =ᵐ[MeasureTheory.volume] fun (x : ℝ) => 0

Every translate t ↦ diracDelta (x - t) is equal almost everywhere to 0.

theorem diagnostic_integrable_diracDelta : MeasureTheory.Integrable diracDelta MeasureTheory.volume

The kernel diracDelta is integrable because it is almost everywhere zero.

theorem diagnostic_integrable_diracDelta_shift (x : ℝ) : MeasureTheory.Integrable (fun (t : ℝ) => diracDelta (x - t)) MeasureTheory.volume

Every translate t ↦ diracDelta (x - t) is integrable.

theorem diagnostic_realConvolutionFun_constOne_diracDelta_eq_zero (x : ℝ) : realConvolutionFun (fun (x : ℝ) => 1) diracDelta x = 0

Convolution of the constant-one function with diracDelta is identically 0.

theorem diagnostic_realConvolutionFun_diracDelta_constOne_eq_zero (x : ℝ) : realConvolutionFun diracDelta (fun (x : ℝ) => 1) x = 0

Convolution of diracDelta with the constant-one function is identically 0.

theorem diagnostic_diracDelta_identity_counterexample : ¬∀ (x : ℝ), realConvolutionFun (fun (x : ℝ) => 1) diracDelta x = 1 ∧ realConvolutionFun diracDelta (fun (x : ℝ) => 1) x = 1

The identity claim (f*δ)(x) = (δ*f)(x) = f(x) fails for f ≡ 1.

theorem diagnostic_convolutionDefined_constOne_diracDelta : ConvolutionDefined (fun (x : ℝ) => 1) diracDelta

ConvolutionDefined holds for f ≡ 1 with the formal diracDelta kernel.

theorem diagnostic_convolutionDefined_diracDelta_constOne : ConvolutionDefined diracDelta fun (x : ℝ) => 1

ConvolutionDefined holds for diracDelta convolved with f ≡ 1.

theorem diagnostic_counterexample_data_for_convolution_associativity_derivative_identity : ∃ (f : ℝ → ℝ) (g : ℝ → ℝ) (h : ℝ → ℝ), ConvolutionDefined f g ∧ ConvolutionDefined g h ∧ ConvolutionDefined (realConvolutionFun f g) h ∧ ConvolutionDefined f (realConvolutionFun g h) ∧ ConvolutionDefined f diracDelta ∧ ConvolutionDefined diracDelta f ∧ ¬∀ (x : ℝ), realConvolutionFun f diracDelta x = f x ∧ realConvolutionFun diracDelta f x = f x

There are explicit f,g,h satisfying all assumptions while the Dirac identity clause fails.

theorem convolution_associativity_derivative_identity (f g h : ℝ → ℝ) (hfg : ConvolutionDefined f g) (hgh : ConvolutionDefined g h) (hfg_h : ConvolutionDefined (realConvolutionFun f g) h) (hf_gh : ConvolutionDefined f (realConvolutionFun g h)) (hfd : ConvolutionDefined f diracDelta) (hdf : ConvolutionDefined diracDelta f) (hassoc : ∀ (x : ℝ), realConvolutionFun (realConvolutionFun f g) h x = realConvolutionFun f (realConvolutionFun g h) x) (hderiv : Differentiable ℝ f ∧ Differentiable ℝ g ∧ ConvolutionDefined (deriv f) g ∧ ConvolutionDefined f (deriv g) → Differentiable ℝ (realConvolutionFun f g) ∧ (∀ (x : ℝ), deriv (realConvolutionFun f g) x = realConvolutionFun (deriv f) g x) ∧ ∀ (x : ℝ), deriv (realConvolutionFun f g) x = realConvolutionFun f (deriv g) x) : (∀ (x : ℝ), realConvolutionFun (realConvolutionFun f g) h x = realConvolutionFun f (realConvolutionFun g h) x) ∧ (Differentiable ℝ f ∧ Differentiable ℝ g ∧ ConvolutionDefined (deriv f) g ∧ ConvolutionDefined f (deriv g) → Differentiable ℝ (realConvolutionFun f g) ∧ (∀ (x : ℝ), deriv (realConvolutionFun f g) x = realConvolutionFun (deriv f) g x) ∧ ∀ (x : ℝ), deriv (realConvolutionFun f g) x = realConvolutionFun f (deriv g) x) ∧ ∀ (x : ℝ), realConvolutionFun f diracDelta x = 0 ∧ realConvolutionFun diracDelta f x = 0

Proposition 3.24 packaged with explicit analytic assumptions: besides the basic ConvolutionDefined hypotheses, we assume associativity and derivative-commutation as separate premises. Under these assumptions and the present function-level diracDelta, convolution with δ vanishes pointwise.

theorem zero_mem_Icc01 : 0 ∈ Set.Icc 0 1

The left endpoint 0 belongs to [0,1] as an element of Set.Icc.

theorem one_mem_Icc01 : 1 ∈ Set.Icc 0 1

The right endpoint 1 belongs to [0,1] as an element of Set.Icc.

theorem helperForLemma_3_5_notMem_Icc01_split {x : ℝ} (hx : x ∉ Set.Icc 0 1) : x < 0 ∨ 1 < x

Helper for Lemma 3.5: points outside [0,1] satisfy x < 0 ∨ 1 < x.

theorem helperForLemma_3_5_IccExtend_zero_outside (h01 : 0 ≤ 1) (f : ↑(Set.Icc 0 1) → ℝ) (hf0 : f ⟨0, zero_mem_Icc01⟩ = 0) (hf1 : f ⟨1, one_mem_Icc01⟩ = 0) {x : ℝ} (hx : x ∉ Set.Icc 0 1) : Set.IccExtend h01 f x = 0

Helper for Lemma 3.5: the Icc extension is zero outside [0,1] using the endpoint hypotheses.

theorem helperForLemma_3_5_IccExtend_eq_ifExtension (h01 : 0 ≤ 1) (f : ↑(Set.Icc 0 1) → ℝ) (hf0 : f ⟨0, zero_mem_Icc01⟩ = 0) (hf1 : f ⟨1, one_mem_Icc01⟩ = 0) : Set.IccExtend h01 f = fun (x : ℝ) => if h : x ∈ Set.Icc 0 1 then f ⟨x, h⟩ else 0

Helper for Lemma 3.5: the Icc extension agrees with the if-defined function.

theorem helperForLemma_3_5_continuous_IccExtend (h01 : 0 ≤ 1) (f : ↑(Set.Icc 0 1) → ℝ) (hf : Continuous f) : Continuous (Set.IccExtend h01 f)

Helper for Lemma 3.5: continuity of the clamped extension Set.IccExtend.

theorem continuous_extension_by_zero_Icc01 (f : ↑(Set.Icc 0 1) → ℝ) (hf : Continuous f) (hf0 : f ⟨0, zero_mem_Icc01⟩ = 0) (hf1 : f ⟨1, one_mem_Icc01⟩ = 0) : have F := fun (x : ℝ) => if h : x ∈ Set.Icc 0 1 then f ⟨x, h⟩ else 0; Continuous F

Lemma 3.5: Let f : [0,1] → ℝ be continuous with f(0)=f(1)=0. Define F : ℝ → ℝ by F(x)=f(x) for x ∈ [0,1] and F(x)=0 for x ∉ [0,1]. Then F is continuous on ℝ.

theorem weierstrassApproximationOnIcc01_zeroEndpoints (f : ↑(Set.Icc 0 1) → ℝ) (hf : Continuous f) (hf0 : f ⟨0, zero_mem_Icc01⟩ = 0) (hf1 : f ⟨1, one_mem_Icc01⟩ = 0) (ε : ℝ) : ε > 0 → ∃ (p : Polynomial ℝ), ∀ (x : ↑(Set.Icc 0 1)), |Polynomial.eval (↑x) p - f x| ≤ ε

Theorem 3.13: (Weierstrass approximation theorem II) Let f : [0,1] → ℝ be continuous and satisfy f(0)=f(1)=0. Then for every ε > 0 there exists a polynomial P such that sup_{x ∈ [0,1]} |P(x) - f(x)| ≤ ε.

theorem weierstrassApproximationOnIcc01 (f : ↑(Set.Icc 0 1) → ℝ) (hf : Continuous f) (ε : ℝ) : ε > 0 → ∃ (p : Polynomial ℝ), ∀ (x : ↑(Set.Icc 0 1)), |Polynomial.eval (↑x) p - f x| ≤ ε

Theorem 3.14: [Weierstrass approximation theorem III] Let f : [0,1] → ℝ be continuous. For every ε > 0 there exists a polynomial P : [0,1] → ℝ such that sup_{x ∈ [0,1]} |P(x) - f(x)| ≤ ε.

theorem weierstrassApproximationOnIcc_sup (a b : ℝ) (hab : a < b) (f : ↑(Set.Icc a b) → ℝ) (hf : Continuous f) (ε : ℝ) : ε > 0 → ∃ (p : Polynomial ℝ), ∀ (y : ↑(Set.Icc a b)), |Polynomial.eval (↑y) p - f y| ≤ ε

Theorem 3.15: [Weierstrass approximation theorem on [a,b]] Let a < b and let f : [a,b] → ℝ be continuous. For every ε > 0 there exists a polynomial P such that sup_{y ∈ [a,b]} |P(y) - f(y)| ≤ ε.