Quantitative Gevrey cutoffs and partitions of unity

This file was automatically generated by Codex.

A fixed finite Gevrey-order construction of nonnegative compact interval cutoffs, a locally finite integer partition of unity, and quantitative affine-rescaling and finite-product derivative bounds. The interval cutoff is one on any prescribed compact interval strictly inside a larger open interval. All statements and supporting definitions use only Mathlib and this module.

Verified sources: blueprint/formalization_blueprint.tex, lem:gevrey, lines 107–126; and Mathlib.Analysis.SpecialFunctions.SmoothTransition, whose smooth exponential gluing function supplies the classical starting point. The derivative recurrence and its quantitative majorants are proved here.

noncomputable def TrilinearHT.Auto.gevreyDerivativePolynomial : ℕ → Polynomial ℝ

The derivative-polynomial recurrence in blueprint Lemma lem:gevrey.

Equations

• One or more equations did not get rendered due to their size.
• TrilinearHT.Auto.gevreyDerivativePolynomial 0 = 1

theorem TrilinearHT.Auto.iteratedDeriv_expNegInvGlue (n : ℕ) : iteratedDeriv n expNegInvGlue = fun (x : ℝ) => Polynomial.eval x⁻¹ (gevreyDerivativePolynomial n) * expNegInvGlue x

Blueprint Lemma lem:gevrey: the recurrence describes all derivatives, including at the gluing point and on the negative half-line.

theorem TrilinearHT.Auto.gevreyDerivativePolynomial_natDegree (n : ℕ) : (gevreyDerivativePolynomial n).natDegree ≤ 2 * n

Blueprint Lemma lem:gevrey: derivative polynomials have degree at most 2n.

theorem TrilinearHT.Auto.polynomial_derivative_step_coeff_le {p : Polynomial ℝ} {d : ℕ} {M : ℝ} (hd : p.natDegree ≤ d) (hM : 0 ≤ M) (hp : ∀ (i : ℕ), |p.coeff i| ≤ M) (i : ℕ) : |(Polynomial.X ^ 2 * (p - Polynomial.derivative p)).coeff i| ≤ (↑d + 1) * M

Coefficient bound for one step of the source's derivative recurrence.

theorem TrilinearHT.Auto.gevreyDerivativePolynomial_coeff_le (n i : ℕ) : |(gevreyDerivativePolynomial n).coeff i| ≤ ↑(2 * n).factorial

Blueprint Lemma lem:gevrey: a factorial coefficient majorant. This slightly coarser bound still gives one fixed Gevrey order.

theorem TrilinearHT.Auto.monomial_mul_exp_neg_le_factorial {z : ℝ} (hz : 0 ≤ z) (i : ℕ) : z ^ i * Real.exp (-z) ≤ ↑i.factorial

The exponential series controls every monomial in a derivative polynomial.

theorem TrilinearHT.Auto.iteratedDeriv_expNegInvGlue_factorial_bound (n : ℕ) (x : ℝ) : |iteratedDeriv n expNegInvGlue x| ≤ (2 * ↑n + 1) * ↑(2 * n).factorial ^ 2

A quantitative derivative bound for the source's smooth gluing function.

theorem TrilinearHT.Auto.iteratedDeriv_expNegInvGlue_gevrey_bound (n : ℕ) (x : ℝ) : |iteratedDeriv n expNegInvGlue x| ≤ (4 * (↑n + 1)) ^ (4 * (n + 1))

Blueprint Lemma lem:gevrey: the gluing function has a fixed Gevrey order. The explicit order four is sufficient for the source's existential fixed-order requirement.

noncomputable def TrilinearHT.Auto.gevreyBump (x : ℝ) : ℝ

The compact bump g(x)g(1-x) in blueprint Lemma lem:gevrey.

Equations

• TrilinearHT.Auto.gevreyBump x = expNegInvGlue x * expNegInvGlue (1 - x)

theorem TrilinearHT.Auto.gevreyBump_nonneg (x : ℝ) : 0 ≤ gevreyBump x

theorem TrilinearHT.Auto.gevreyBump_pos {x : ℝ} (hx : x ∈ Set.Ioo 0 1) : 0 < gevreyBump x

theorem TrilinearHT.Auto.gevreyBump_zero {x : ℝ} (hx : x ∉ Set.Ioo 0 1) : gevreyBump x = 0

theorem TrilinearHT.Auto.gevreyBump_contDiff {n : ℕ∞} : ContDiff ℝ (↑n) gevreyBump

theorem TrilinearHT.Auto.gevreyBump_hasCompactSupport : HasCompactSupport gevreyBump

theorem TrilinearHT.Auto.iteratedDeriv_gevreyBump_bound (n : ℕ) (x : ℝ) : |iteratedDeriv n gevreyBump x| ≤ (8 * (↑n + 1)) ^ (8 * (n + 1))

Blueprint Lemma lem:gevrey: a compact positive bump with a fixed all-orders bound.

noncomputable def TrilinearHT.Auto.gevreyBumpIntegral : ℝ

The positive normalization constant for the bump in blueprint Lemma lem:gevrey.

Equations

• TrilinearHT.Auto.gevreyBumpIntegral = ∫ (x : ℝ), TrilinearHT.Auto.gevreyBump x

theorem TrilinearHT.Auto.gevreyBump_integrable : MeasureTheory.Integrable gevreyBump MeasureTheory.volume

theorem TrilinearHT.Auto.gevreyBumpIntegral_pos : 0 < gevreyBumpIntegral

noncomputable def TrilinearHT.Auto.gevreyDensity (x : ℝ) : ℝ

The normalized positive bump in blueprint Lemma lem:gevrey.

Equations

• TrilinearHT.Auto.gevreyDensity x = TrilinearHT.Auto.gevreyBump x / TrilinearHT.Auto.gevreyBumpIntegral

theorem TrilinearHT.Auto.gevreyDensity_nonneg (x : ℝ) : 0 ≤ gevreyDensity x

theorem TrilinearHT.Auto.gevreyDensity_contDiff {n : ℕ∞} : ContDiff ℝ (↑n) gevreyDensity

theorem TrilinearHT.Auto.gevreyDensity_integral : ∫ (x : ℝ), gevreyDensity x = 1

theorem TrilinearHT.Auto.gevreyDensity_zero {x : ℝ} (hx : x ∉ Set.Ioo 0 1) : gevreyDensity x = 0

theorem TrilinearHT.Auto.iteratedDeriv_gevreyDensity_bound (n : ℕ) (x : ℝ) : |iteratedDeriv n gevreyDensity x| ≤ gevreyBumpIntegral⁻¹ * (8 * (↑n + 1)) ^ (8 * (n + 1))

Blueprint Lemma lem:gevrey: normalization costs one fixed positive factor.

noncomputable def TrilinearHT.Auto.gevreyStep (x : ℝ) : ℝ

The smooth increasing step obtained by integrating the probability bump.

Equations

• TrilinearHT.Auto.gevreyStep x = ∫ (t : ℝ) in 0..x, TrilinearHT.Auto.gevreyDensity t

theorem TrilinearHT.Auto.gevreyStep_hasDerivAt (x : ℝ) : HasDerivAt gevreyStep (gevreyDensity x) x

theorem TrilinearHT.Auto.gevreyStep_deriv : deriv gevreyStep = gevreyDensity

theorem TrilinearHT.Auto.gevreyStep_contDiff (n : ℕ) : ContDiff ℝ (↑n) gevreyStep

theorem TrilinearHT.Auto.iteratedDeriv_gevreyStep_succ (n : ℕ) : iteratedDeriv (n + 1) gevreyStep = iteratedDeriv n gevreyDensity

theorem TrilinearHT.Auto.gevreyStep_zero {x : ℝ} (hx : x ≤ 0) : gevreyStep x = 0

theorem TrilinearHT.Auto.gevreyStep_one {x : ℝ} (hx : 1 ≤ x) : gevreyStep x = 1

theorem TrilinearHT.Auto.gevreyStep_monotone : Monotone gevreyStep

theorem TrilinearHT.Auto.gevreyStep_mem_Icc (x : ℝ) : gevreyStep x ∈ Set.Icc 0 1

noncomputable def TrilinearHT.Auto.gevreyPartition (x : ℝ) : ℝ

The compact partition function from blueprint Lemma lem:gevrey, expressed as a difference of antiderivatives, equivalently as convolution with an interval.

Equations

• TrilinearHT.Auto.gevreyPartition x = TrilinearHT.Auto.gevreyStep (2 * x + 3 / 2) - TrilinearHT.Auto.gevreyStep (2 * x - 1 / 2)

theorem TrilinearHT.Auto.gevreyPartition_nonneg (x : ℝ) : 0 ≤ gevreyPartition x

theorem TrilinearHT.Auto.gevreyPartition_le_one (x : ℝ) : gevreyPartition x ≤ 1

theorem TrilinearHT.Auto.gevreyPartition_zero_left {x : ℝ} (hx : x ≤ -(3 / 4)) : gevreyPartition x = 0

theorem TrilinearHT.Auto.gevreyPartition_zero_right {x : ℝ} (hx : 3 / 4 ≤ x) : gevreyPartition x = 0

theorem TrilinearHT.Auto.gevreyPartition_contDiff (n : ℕ) : ContDiff ℝ (↑n) gevreyPartition

theorem TrilinearHT.Auto.gevreyPartition_tsupport_subset : tsupport gevreyPartition ⊆ Set.Icc (-(3 / 4)) (3 / 4)

theorem TrilinearHT.Auto.gevreyPartition_hasCompactSupport : HasCompactSupport gevreyPartition

theorem TrilinearHT.Auto.gevreyPartition_tsupport_subset_open : tsupport gevreyPartition ⊆ Set.Ioo (-1) 1

theorem TrilinearHT.Auto.gevreyPartition_add_shift {x : ℝ} (hx : x ∈ Set.Icc 0 1) : gevreyPartition x + gevreyPartition (x - 1) = 1

The two nonzero possible translates telescope on a fundamental interval.

theorem TrilinearHT.Auto.gevreyPartition_tsum (x : ℝ) : ∑' (k : ℤ), gevreyPartition (x - ↑k) = 1

Blueprint Lemma lem:gevrey: the integer translates sum exactly to one.

theorem TrilinearHT.Auto.iteratedDeriv_affine (n : ℕ) {f : ℝ → ℝ} (hf : ContDiff ℝ (↑n) f) (c a : ℝ) : (iteratedDeriv n fun (x : ℝ) => f (c * x + a)) = fun (x : ℝ) => c ^ n * iteratedDeriv n f (c * x + a)

Affine rescaling multiplies the nth derivative by the nth power of the slope.

theorem TrilinearHT.Auto.iteratedDeriv_gevreyStep_bound (n : ℕ) (x : ℝ) : |iteratedDeriv n gevreyStep x| ≤ max 1 gevreyBumpIntegral⁻¹ * (8 * (↑n + 1)) ^ (8 * (n + 1))

The source's normalized step inherits quantitative derivative bounds.

theorem TrilinearHT.Auto.iteratedDeriv_gevreyPartition_bound (n : ℕ) (x : ℝ) : |iteratedDeriv n gevreyPartition x| ≤ 2 * max 1 gevreyBumpIntegral⁻¹ * (8 * (↑n + 1)) ^ (9 * (n + 1))

Blueprint Lemma lem:gevrey: the partition has one fixed Gevrey order.

noncomputable def TrilinearHT.Auto.gevreyIntervalCutoff (a b c d x : ℝ) : ℝ

Cutoff for [b,c] with support strictly inside (a,d), from the source's step construction.

Equations

• TrilinearHT.Auto.gevreyIntervalCutoff a b c d x = TrilinearHT.Auto.gevreyStep ((2 * x - a - b) / (b - a)) * TrilinearHT.Auto.gevreyStep ((c + d - 2 * x) / (d - c))

theorem TrilinearHT.Auto.gevreyIntervalCutoff_mem_Icc (a b c d x : ℝ) : gevreyIntervalCutoff a b c d x ∈ Set.Icc 0 1

theorem TrilinearHT.Auto.gevreyIntervalCutoff_eq_one {a b c d x : ℝ} (hab : a < b) (hcd : c < d) (hx : x ∈ Set.Icc b c) : gevreyIntervalCutoff a b c d x = 1

theorem TrilinearHT.Auto.gevreyIntervalCutoff_contDiff (n : ℕ) (a b c d : ℝ) : ContDiff ℝ (↑n) (gevreyIntervalCutoff a b c d)

theorem TrilinearHT.Auto.gevreyIntervalCutoff_zero_left {a b c d x : ℝ} (hab : a < b) (hx : x ≤ (a + b) / 2) : gevreyIntervalCutoff a b c d x = 0

theorem TrilinearHT.Auto.gevreyIntervalCutoff_zero_right {a b c d x : ℝ} (hcd : c < d) (hx : (c + d) / 2 ≤ x) : gevreyIntervalCutoff a b c d x = 0

theorem TrilinearHT.Auto.gevreyIntervalCutoff_tsupport_subset {a b c d : ℝ} (hab : a < b) (hcd : c < d) : tsupport (gevreyIntervalCutoff a b c d) ⊆ Set.Icc ((a + b) / 2) ((c + d) / 2)

theorem TrilinearHT.Auto.gevreyIntervalCutoff_hasCompactSupport {a b c d : ℝ} (hab : a < b) (hcd : c < d) : HasCompactSupport (gevreyIntervalCutoff a b c d)

theorem TrilinearHT.Auto.gevreyIntervalCutoff_tsupport_subset_open {a b c d : ℝ} (hab : a < b) (hcd : c < d) : tsupport (gevreyIntervalCutoff a b c d) ⊆ Set.Ioo a d

theorem TrilinearHT.Auto.iteratedDeriv_mul_geometric_bound {n : ℕ} {f g : ℝ → ℝ} {x A B R : ℝ} (hf : ContDiffAt ℝ (↑n) f x) (hg : ContDiffAt ℝ (↑n) g x) (hA : 0 ≤ A) (_hB : 0 ≤ B) (hR : 0 ≤ R) (hfi : ∀ i ≤ n, |iteratedDeriv i f x| ≤ A * R ^ i) (hgi : ∀ i ≤ n, |iteratedDeriv i g x| ≤ B * R ^ i) : |iteratedDeriv n (fun (y : ℝ) => f y * g y) x| ≤ A * B * (2 * R) ^ n

Quantitative Leibniz rule for derivative bounds of geometric form.

theorem TrilinearHT.Auto.iteratedDeriv_affine_step_bound {n i : ℕ} (hi : i ≤ n) (c a x S : ℝ) (hS : 0 ≤ S) (hc : |c| ≤ S) : |iteratedDeriv i (fun (y : ℝ) => gevreyStep (c * y + a)) x| ≤ max 1 gevreyBumpIntegral⁻¹ * (8 * (↑n + 1)) ^ (8 * (n + 1)) * S ^ i

Derivatives of an affine step, uniformly over orders up to a fixed n.

theorem TrilinearHT.Auto.iteratedDeriv_gevreyIntervalCutoff_bound (n : ℕ) (a b c d x : ℝ) : |iteratedDeriv n (gevreyIntervalCutoff a b c d) x| ≤ max 1 gevreyBumpIntegral⁻¹ ^ 2 * (8 * (↑n + 1)) ^ (16 * (n + 1)) * (2 * max |2 / (b - a)| |-2 / (d - c)|) ^ n

Blueprint Lemma lem:gevrey: explicit derivative bound for interval cutoffs. The interval dependence is isolated in the maximum of the two transition slopes.

theorem TrilinearHT.Auto.absorb_gevrey_constants {A R : ℝ} (_hA : 0 ≤ A) (hR : 0 ≤ R) (s : ℕ) : ∃ (C : ℕ), 1 ≤ C ∧ ∀ (n : ℕ), A * R ^ n * (8 * (↑n + 1)) ^ (s * (n + 1)) ≤ (↑C * (↑n + 1)) ^ (C * (n + 1))

Fixed scalar and rescaling factors can be absorbed in one Gevrey constant.

theorem TrilinearHT.Auto.gevreyPartition_exists_derivative_bound : ∃ (C : ℕ), 1 ≤ C ∧ ∀ (n : ℕ) (x : ℝ), |iteratedDeriv n gevreyPartition x| ≤ (↑C * (↑n + 1)) ^ (C * (n + 1))

The precise fixed-order Gevrey assertion for the partition in the blueprint.

theorem TrilinearHT.Auto.gevreyIntervalCutoff_exists_derivative_bound (a b c d : ℝ) : ∃ (C : ℕ), 1 ≤ C ∧ ∀ (n : ℕ) (x : ℝ), |iteratedDeriv n (gevreyIntervalCutoff a b c d) x| ≤ (↑C * (↑n + 1)) ^ (C * (n + 1))

The precise fixed-order Gevrey assertion for arbitrary interval cutoffs.

theorem TrilinearHT.Auto.existsGevreyPartition : ∃ (ρ : ℝ → ℝ), (∀ (n : ℕ), ContDiff ℝ (↑n) ρ) ∧ (∀ (x : ℝ), 0 ≤ ρ x) ∧ HasCompactSupport ρ ∧ tsupport ρ ⊆ Set.Ioo (-1) 1 ∧ (∀ (x : ℝ), ∑' (k : ℤ), ρ (x - ↑k) = 1) ∧ ∃ (C : ℕ), 1 ≤ C ∧ ∀ (n : ℕ) (x : ℝ), |iteratedDeriv n ρ x| ≤ (↑C * (↑n + 1)) ^ (C * (n + 1))

Blueprint Lemma lem:gevrey, partition-of-unity assertion: there is a nonnegative smooth compactly supported function in (-1,1) whose integer translates sum to one and whose derivatives satisfy a single fixed Gevrey bound.

theorem TrilinearHT.Auto.existsGevreyIntervalCutoff {a b c d : ℝ} (hab : a < b) (_hbc : b ≤ c) (hcd : c < d) : ∃ (χ : ℝ → ℝ), (∀ (n : ℕ), ContDiff ℝ (↑n) χ) ∧ (∀ (x : ℝ), χ x ∈ Set.Icc 0 1) ∧ HasCompactSupport χ ∧ tsupport χ ⊆ Set.Ioo a d ∧ (∀ x ∈ Set.Icc b c, χ x = 1) ∧ ∃ (C : ℕ), 1 ≤ C ∧ ∀ (n : ℕ) (x : ℝ), |iteratedDeriv n χ x| ≤ (↑C * (↑n + 1)) ^ (C * (n + 1))

Blueprint Lemma lem:gevrey, interval-cutoff assertion: for a compact interval inside an open interval, a smooth nonnegative cutoff equals one on the compact interval and has compact support in the open interval, with Gevrey bounds.

theorem TrilinearHT.Auto.gevrey_endpoint_cutoff_uniform_derivative {B ε : ℝ} (hB : 8 ≤ B) (hM : max 1 gevreyBumpIntegral⁻¹ ≤ B) (hε : 0 < ε) (hε1 : ε ≤ 1) (n : ℕ) (x : ℝ) : |iteratedDeriv n (gevreyIntervalCutoff 0 ε (1 - ε) 1) x| ≤ (B / ε) ^ (20 * (n + 1)) * (↑n + 1) ^ (20 * (n + 1))

theorem TrilinearHT.Auto.exists_uniform_gevrey_endpoint_cutoffs : ∃ (B : ℝ), 8 ≤ B ∧ ∀ (ε : ℝ), 0 < ε → ε ≤ 1 / 2 → ∃ (η : ℝ → ℝ), ContDiff ℝ (↑⊤) η ∧ (∀ (x : ℝ), η x ∈ Set.Icc 0 1) ∧ HasCompactSupport η ∧ tsupport η ⊆ Set.Ioo 0 1 ∧ (∀ x ∈ Set.Icc ε (1 - ε), η x = 1) ∧ ∀ (n : ℕ) (x : ℝ), |iteratedDeriv n η x| ≤ (B / ε) ^ (20 * (n + 1)) * (↑n + 1) ^ (20 * (n + 1))