Stat.CLT.BerryEsseen
The Berry–Esseen theorem with explicit constant one.
PrawitzKernel 3 core · 0 supporting These explicit functions separate the analytic prerequisites of sharp CDF smoothing from probability laws.
Prawitz's compact spectral smoothing filter
These explicit functions separate the analytic prerequisites of sharp CDF smoothing from probability laws. Frequencies are in radians. The singular value at zero is assigned zero; all later integrals are Lebesgue integrals, so this endpoint convention has no effect on their value.
Reference: Tyurin, arXiv:0912.0726, Prawitz's smoothing inequality and its displayed filter.
The cotangent weight at frequency t is (1 − t)·cot(πt) + 1/π, with the cotangent written as cos(πt)/sin(πt). It is the sine-part weight of Prawitz's approximation to the sign function and is used on 0 < t < 1; at points where sin(πt) vanishes the quotient is assigned zero.
Prawitz's complex spectral filter at frequency t is zero when t = 0 or |t| > 1, and otherwise has real part the triangular weight (1 − |t|)/2 and imaginary part ((1 − |t|)·cot(πt) + sign(t)/π)/2, with cot(πt) written as cos(πt)/sin(πt). At t = ±1, where the sine vanishes, the quotient is assigned zero, so the value there is ±i/(2π).
Prawitz's band-limited approximation to the sign function at a point y is 2·∫ over t in [0, 1] of w(t)·sin(ty), where w(t) = (1 − t)·cot(πt) + 1/π is the cotangent weight. Frequencies are in radians and confined to the unit band.
Definition (Lean source)
PrawitzEnvelopes 3 core · 0 supporting These explicit analytic functions separate numerical budget proofs from probabilistic characteristic-function bounds.
Deterministic envelopes for Prawitz smoothing
These explicit analytic functions separate numerical budget proofs from probabilistic characteristic-function bounds. They contain no convergence or coverage premises. The original envelope definitions are preserved exactly.
The cubic moment envelope at ratio ρ and frequency t is min(1, exp(−t²/2 + ρ|t|³/5)): a cubically damped Gaussian factor truncated at one, the universal modulus bound for a probability characteristic function.
The Fourier discrepancy envelope at ratio ρ and frequency t is the smaller of two quantities: the Taylor product bound (ρ|t|³/6 + ρ²t⁴/8)·exp(−t²/4 + ρ|t|³/10), and the modulus sum, namely the cubic moment envelope min(1, exp(−t²/2 + ρ|t|³/5)) plus the Gaussian modulus exp(−t²/2).
Definition (Lean source)
The deterministic Prawitz smoothing envelope at ratio ρ, inner cutoff U0 and outer cutoff U is the sum of four explicit terms, with K the Prawitz filter: (2/U)·∫ over [0, U0] of |K(t/U)| times the discrepancy envelope at (ρ, t); (2/U)·∫ over [U0, U] of |K(t/U)| times the cubic moment envelope at (ρ, t); 2·∫ over [0, U0] of |K(t/U)/U − i/(2πt)|·exp(−t²/2); and (1/π)·∫ over t > U0 of exp(−t²/2)/t. It is a function of three real numbers only; no probability law enters. The expression is the intended envelope for 0 < U0 ≤ U; outside that range (for instance U = 0, where it divides by zero) it is only a formal value.
Definition (Lean source)
SmoothingKernel 2 core · 3 supporting The fourth power of the sinc function gives a nonnegative density whose Fourier transform is supported on a bounded interval. ★ sinc4Kernel_fourier_eq_zero
A compact-frequency probability smoothing kernel
The fourth power of the sinc function gives a nonnegative density whose Fourier transform is supported on a bounded interval. These analytic facts are the first layer of the quantitative CDF smoothing argument.
The fourth-power sinc kernel at bandwidth T and point x is (3T/(8π))·sinc(Tx/4)⁴. At positive bandwidth it is a probability density whose Fourier transform vanishes outside [−T, T].
For a positive bandwidth T, the Fourier transform of the fourth-power sinc kernel vanishes at every frequency t with |t| ≥ T, that is, outside its bandwidth interval.
Formal statement
Proof (Lean source)
3 supporting declarations (lemmas, instances)
-
sinc4Kernel_nonnegtheorem — The fourth-power sinc kernel is nonnegative at every real argument when its bandwidth is positive.Proof (Lean source)
theorem sinc4Kernel_nonneg (T : ℝ) (hT : 0 < T) (x : ℝ) : 0 ≤ sinc4Kernel T x := by unfold sinc4Kernel positivity -
sinc4Kernel_integrabletheorem — The fourth-power sinc kernel is integrable on the real line at every positive bandwidth.Proof (Lean source)
theorem sinc4Kernel_integrable (T : ℝ) (hT : 0 < T) : Integrable (sinc4Kernel T) volume := by have hsinc : Integrable (fun x : ℝ => sinc x ^ 4) := by apply (integrable_inv_one_add_sq.const_mul (4 : ℝ)).mono · fun_prop · filter_upwards with x rw [Real.norm_eq_abs, abs_of_nonneg (by positivity : 0 ≤ sinc x ^ 4)] rw [Real.norm_eq_abs, abs_of_nonneg (by positivity : 0 ≤ 4 * (1 + x ^ 2)⁻¹)] rw [inv_eq_one_div, mul_one_div] apply (le_div_iff₀ (by positivity : 0 < 1 + x ^ 2)).2 by_cases hx : |x| ≤ 1 · have ha2 : |x| * |x| ≤ 1 * 1 := mul_self_le_mul_self (abs_nonneg x) hx have hx2 : x ^ 2 ≤ 1 := by simpa [sq_abs, pow_two] using ha2 have hs := Real.abs_sinc_le_one x have hsl := neg_abs_le (sinc x) have hsr := le_abs_self (sinc x) have hs2 : sinc x ^ 2 ≤ 1 := by nlinarith have hs4 : sinc x ^ 4 ≤ 1 := by nlinarith [mul_self_le_mul_self (sq_nonneg (sinc x)) hs2] nlinarith · have hxabs : 1 < |x| := lt_of_not_ge hx have hx0 : x ≠ 0 := by intro h subst x norm_num at hxabs rw [Real.sinc_of_ne_zero hx0, div_pow, div_mul_eq_mul_div] apply (div_le_iff₀ (by positivity : 0 < x ^ 4)).2 have habs2 : (1 : ℝ) ^ 2 < |x| ^ 2 := (sq_lt_sq₀ (by positivity) (abs_nonneg x)).2 hxabs have hx2 : 1 < x ^ 2 := by simpa [sq_abs] using habs2 have hs := Real.abs_sin_le_one x have hsl := neg_abs_le (sin x) have hsr := le_abs_self (sin x) have hs2 : sin x ^ 2 ≤ 1 := by nlinarith have hs4 : sin x ^ 4 ≤ 1 := by nlinarith [mul_self_le_mul_self (sq_nonneg (sin x)) hs2] calc sin x ^ 4 * (1 + x ^ 2) ≤ 1 * (1 + x ^ 2) := mul_le_mul_of_nonneg_right hs4 (by positivity) _ ≤ 2 * x ^ 2 := by nlinarith _ ≤ 4 * x ^ 4 := by nlinarith [sq_nonneg (x ^ 2 - 1)] have hscaled : Integrable (fun x : ℝ => sinc (T * x / 4) ^ 4) := by convert hsinc.comp_mul_left' (by positivity : T / 4 ≠ 0) using 1 ext x congr 1 ring_nf exact hscaled.const_mul (3 * T / (8 * pi)) -
sinc4Kernel_integral_eq_onetheorem — The integral of the fourth-power sinc kernel is one at every positive bandwidth, so it defines a probability density.Proof (Lean source)
theorem sinc4Kernel_integral_eq_one (T : ℝ) (hT : 0 < T) : ∫ x : ℝ, sinc4Kernel T x = 1 := by /- Set `t = 0` in `sincFourth_fourier_triangleConvolution`, use `sincTriangle_square_integral` to obtain ∫ sinc(x)^4 dx = 2π/3, then scale x ↦ T*x/4 via `Measure.integral_comp_mul_left`. Since `T > 0`, the Jacobian is `4/T`; the prefactor 3T/(8π) makes the integral one. At zero frequency, rewrite `|0-u|` as `|u|` and the convolution integrand as the square of the triangle. -/ have hfourier := sincFourth_fourier_triangleConvolution 0 have hzero : (∫ x : ℝ, sinc x ^ 4) = 2 * pi / 3 := by have htri : (∫ u : ℝ, (pi * max (1 - |u| / 2) 0) * (pi * max (1 - |(0 : ℝ) - u| / 2) 0)) = 4 * pi ^ 2 / 3 := by convert sincTriangle_square_integral using 1 congr 1 ext u simp only [zero_sub, abs_neg] ring rw [htri] at hfourier simp only [zero_mul, Complex.ofReal_zero, zero_mul, Complex.exp_zero, one_mul, integral_complex_ofReal] at hfourier have hpi : pi ≠ 0 := Real.pi_ne_zero apply Complex.ofReal_injective convert hfourier using 1 <;> push_cast <;> field_simp <;> ring have hscale : (∫ x : ℝ, sinc (T * x / 4) ^ 4) = (4 / T) * (∫ x : ℝ, sinc x ^ 4) := by have h := Measure.integral_comp_mul_left (fun x : ℝ => sinc x ^ 4) (T / 4) convert h using 1 · congr 1; ext x; ring_nf · simp only [smul_eq_mul, abs_inv, abs_of_pos (by positivity : 0 < T / 4)] field_simp unfold sinc4Kernel rw [integral_const_mul, hscale, hzero] have hpi : pi ≠ 0 := Real.pi_ne_zero field_simp ring
PrawitzCompactRationalData 11 core · 0 supporting The parameter grid has ninety cells of width 1/1000 on [1/100,1/10] and one hundred eighty cells of width 1/200 on [1/10,1].
Exact rational grid data for compact Prawitz budgets
The parameter grid has ninety cells of width 1/1000 on [1/100,1/10] and one hundred eighty cells of width 1/200 on [1/10,1]. Low frequency cells have width 1/200, and high cells have width 1/1000 in the kernel variable. All tables are explicit integers. Their entries and finite sums are obligations in the three separate certificate modules, not assumptions.
Sixteen-term reciprocal Taylor bounds replace negative exponentials. Each cell bound is rounded UP to one hundred millionth before summation; this keeps denominators small without relying on approximate arithmetic. The singular low cell [0,1/200] uses its proved polynomial integral bound. The high sum includes every cell from its lower integer index through 999; the analytic comparison at the assigned kernel endpoint is only a.e.
The left endpoint of the j-th parameter cell is (10 + j)/1000 for j < 90 and (20 + (j − 90))/200 for j ≥ 90: the cells have width one thousandth from 1/100 up to 1/10 and width one two hundredth from 1/10 onward.
Definition (Lean source)
The right endpoint of the j-th parameter cell is the left endpoint of cell j + 1, so consecutive cells have no gaps.
Definition (Lean source)
The low-frequency cutoff index of the j-th parameter cell is an integer read from an explicit 270-entry table, with values between 300 and 859; divided by two hundred it is the cell's upper low-frequency grid endpoint. For j outside the 270-cell grid the value is the default 300.
Definition (Lean source)
The high-frequency cutoff index of the j-th parameter cell is an integer read from an explicit 270-entry table, with values between 16 and 620; divided by one thousand it is the lower endpoint, in the rescaled kernel variable, of the cell's high-frequency range. For j outside the 270-cell grid the value is the default 1.
Definition (Lean source)
The integer kernel magnitude entry of the i-th frequency cell is read from an explicit 1000-entry table; divided by one million it serves as the upper bound for the Prawitz filter magnitude on the cell [i/1000, (i + 1)/1000] of the kernel variable, a bound certified separately. The entry at index zero and the default for i ≥ 1000 are zero and bound nothing: the high certificate starts at a positive index.
Definition (Lean source)
The rational squared kernel bound on the i-th grid cell, with a = i/1000, b = (i + 1)/1000 and the decimal bounds p = 3.14159 and q = 3.14160 for π, is (1 − a)²/4 + (((1 − a)·(1 − (pa)²/2 + (qb)⁴/24)/(pa·(1 − (qb)²/6)) + 1/p)/2)² for i < 500 (the lower half-band) and the reflected polynomial (1 − a)²/4 + q²(1 − a)⁴/16 for i ≥ 500. At i = 0 the denominator pa vanishes and the quotient is assigned zero.
Definition (Lean source)
The rational bound for the initial low-frequency interval [0, 1/200] on the j-th parameter cell is (1/p + 5sa/12)·(1/6 + sa/8)·a³/3, with a = 1/200, s the cell's right endpoint and p = 3.14159. This interval contains the filter's removable singularity at zero.
Definition (Lean source)
The rational normalized low-frequency cell bound for the j-th parameter cell and the i-th frequency cell is (1/200)·(1/(pa) + 5s/12) times the smaller of the Taylor branch (b³/6 + sb⁴/8)/T(e/2) and the modulus-sum branch (1/T(e) + 1/T(a²/2))/r. Here r and s are the parameter cell's left and right endpoints, a = i/200, b = (i + 1)/200, p = 3.14159, e is the smaller of a²/2 − sa³/5 and b²/2 − sb³/5, and T is the sixteen-term Taylor polynomial of the exponential. It is meant for positive i; at i = 0 the quotient 1/(pa) is assigned zero.
Definition (Lean source)
The complete normalized rational low-frequency sum for the j-th parameter cell is the initial-interval bound rounded up to a multiple of one hundred millionth, plus the sum over frequency indices i from 1 up to but not including the cell's low cutoff index of the low cell bounds, each rounded up in the same way.
Definition (Lean source)
The rational raw high-frequency cell bound for the j-th parameter cell and the i-th kernel frequency cell is (12/(5r))·(1/1000)·(M/1000000)/T(e). Here r and s are the parameter cell's left and right endpoints, a = i/1000, b = (i + 1)/1000, M is the integer kernel magnitude entry at i, e is the smaller of 72a²/25 − 1728a³/625 and 72b²/25 − 1728b³/625 divided by s², and T is the sixteen-term Taylor polynomial of the exponential. The cell length is rescaled by the bandwidth 12/(5r) at the lower parameter, and the cubic damping is taken at the upper parameter.
Definition (Lean source)
The complete raw rational high-frequency sum for the j-th parameter cell is the sum, over kernel frequency indices i from the cell's high cutoff index through 999, of the high cell bounds, each rounded up to a multiple of one hundred millionth.
Definition (Lean source)
EsseenSignedKernel 2 core · 0 supporting This reflected and shifted kernel is the explicit witness used in the unit-bandwidth one-sided Esseen comparison. ★ esseenSignedSinc4Kernel_integrable_continuous
The signed sinc-fourth comparison kernel
This reflected and shifted kernel is the explicit witness used in the unit-bandwidth one-sided Esseen comparison. Its elementary regularity is separated from its Fourier support and comparison properties.
At a real argument y, the signed comparison kernel is -y/8 times the unit sinc-fourth density evaluated at -y-4.
Definition (Lean source)
The signed sinc-fourth comparison kernel (the reflected, shifted, linearly weighted sinc-fourth kernel) is integrable and continuous on the real line.
Formal statement
Proof (Lean source)
CDFDifferenceFourierKernel 2 core · 0 supporting The signed half-line indicators below have support between their endpoints. ★ orientedFourierKernel_integrable
An integrable oriented interval kernel
The signed half-line indicators below have support between their endpoints. Finite first moments make the resulting Fourier kernel integrable over two independent observations and Lebesgue measure. This is the domination needed for the CDF Fourier Fubini interchange.
The signed Fourier kernel of the interval oriented from a to b is the Fourier exponential times 1_{a ≤ x} - 1_{b ≤ x}. The choice of weak inequality makes averaging over laws with atoms recover their Iic CDFs.
For two probability laws with finite first moments, the oriented interval Fourier kernel is integrable jointly in its two endpoints, drawn independently from the two laws, and the Lebesgue variable.
Formal statement
Proof (Lean source)
PrawitzRationalArithmetic 4 core · 5 supporting Finite Taylor polynomials, outward rounding, and existing bounds for pi turn the analytic cell enclosures into exact rational checks. ★ prawitz_rational_pi_bounds
Rational arithmetic for compact Prawitz certificates
Finite Taylor polynomials, outward rounding, and existing bounds for pi turn the analytic cell enclosures into exact rational checks. No floating point evaluation is used by these definitions or their comparison lemmas. The Taylor degree and rounding scale are fixed for the compact certificates.
The sixteen-term Taylor polynomial at a rational argument is an exactly computable rational approximation to the exponential.
Definition (Lean source)
The rational upper enclosure of the exponential at a rational argument x is the eighth power of the sixteen-term Taylor polynomial at x/8 plus the remainder term (x/8)¹⁶·17/(16!·16). It bounds exp(x) from above only for 0 ≤ x ≤ 8.
Definition (Lean source)
Outward rounding of a rational value is the smallest integer multiple of one hundred millionth that is at least that value, so it preserves an upper bound.
Definition (Lean source)
The rational endpoints 314159/100000 and 314160/100000 used by the compact certificates enclose π. Both inequalities follow from Mathlib's proved decimal bounds.
5 supporting declarations (lemmas, instances)
-
prawitz_le_roundUptheorem — A rational input is no larger than its outward rounding.Proof (Lean source)
theorem prawitz_le_roundUp (x : ℚ) : x ≤ prawitzRoundUp x := by have h := Int.le_ceil (100000000 * x) unfold prawitzRoundUp exact (le_div_iff₀ (by norm_num : (0 : ℚ) < 100000000)).2 (by simpa only [mul_comm] using h) -
prawitzTaylor16_casttheorem — Casting the rational Taylor polynomial gives the real Taylor polynomial with exactly the same terms.hypothesesx :ℚconclusion(prawitzTaylor16 x : ℝ) = ∑ m ∈ range 16, (x : ℝ) ^ m / (m.factorial : ℝ)Proof (Lean source)
theorem prawitzTaylor16_cast (x : ℚ) : (prawitzTaylor16 x : ℝ) = ∑ m ∈ range 16, (x : ℝ) ^ m / (m.factorial : ℝ) := by simp [prawitzTaylor16] -
prawitz_taylor16_pos_le_exptheorem — At a nonnegative real argument, the sixteen-term Taylor polynomial is positive and no larger than the exponential.hypothesesx :ℝhx :0 ≤ xconclusionconclusion 10 < (∑ m ∈ range 16, x ^ m / (m.factorial : ℝ))conclusion 2(∑ m ∈ range 16, x ^ m / (m.factorial : ℝ)) ≤ exp xProof (Lean source)
theorem prawitz_taylor16_pos_le_exp (x : ℝ) (hx : 0 ≤ x) : 0 < (∑ m ∈ range 16, x ^ m / (m.factorial : ℝ)) ∧ (∑ m ∈ range 16, x ^ m / (m.factorial : ℝ)) ≤ exp x := by have hone : (1 : ℝ) ≤ ∑ m ∈ range 16, x ^ m / (m.factorial : ℝ) := by simpa using (single_le_sum (f := fun m : ℕ => x ^ m / (m.factorial : ℝ)) (fun m _ => by positivity) (show 0 ∈ range 16 by decide)) exact ⟨lt_of_lt_of_le (by norm_num) hone, Real.sum_le_exp_of_nonneg hx 16⟩ -
prawitz_exp_neg_le_reciprocal_taylor16theorem — At a nonnegative rational argument, the reciprocal Taylor polynomial encloses the negative exponential.Proof (Lean source)
theorem prawitz_exp_neg_le_reciprocal_taylor16 (x : ℚ) (hx : 0 ≤ x) : exp (-(x : ℝ)) ≤ (1 / prawitzTaylor16 x : ℚ) := by have hx' : (0 : ℝ) ≤ x := by exact_mod_cast hx have h := prawitz_taylor16_pos_le_exp (x : ℝ) hx' rw [Real.exp_neg] push_cast rw [prawitzTaylor16_cast] simpa only [one_div] using one_div_le_one_div_of_le h.1 h.2 -
prawitz_exp_le_upper8theorem — On the nonnegative interval through eight, the rational eighth-power Taylor remainder encloses the exponential.Proof (Lean source)
theorem prawitz_exp_le_upper8 (x : ℚ) (hx : 0 ≤ x) (hx8 : x ≤ 8) : exp (x : ℝ) ≤ (prawitzExpUpper8 x : ℝ) := by have hx' : (0 : ℝ) ≤ x := by exact_mod_cast hx have hx8' : (x : ℝ) ≤ 8 := by exact_mod_cast hx8 have h := Real.exp_bound' (x := (x : ℝ) / 8) (by positivity) (by linarith) (n := 16) (by norm_num) have hp := pow_le_pow_left₀ (Real.exp_nonneg _) h 8 rw [← Real.exp_nat_mul] at hp norm_num only [Nat.cast_ofNat] at hp have heq : 8 * ((x : ℝ) / 8) = x := by ring rw [heq] at hp norm_num [prawitzExpUpper8, prawitzTaylor16_cast] at hp ⊢ exact hp
SincBoxFourier 2 core · 1 supporting The interval density whose Fourier transform is sinc is the first step in computing the squared-sinc transform by convolution and Fourier inversion. ★ sincBox_fourier
Fourier transform of a compact interval density
The interval density whose Fourier transform is sinc is the first step in computing the squared-sinc transform by convolution and Fourier inversion.
The interval density at a real point: the complex number π when the point lies in the half-open interval (−1/(2π), 1/(2π)], and zero otherwise. It integrates to one, and its Fourier transform is the real sinc function.
At every real frequency x, the Fourier transform of the compact interval density equal to π on (−1/(2π), 1/(2π)] is the real sinc function sin(x)/x, viewed as a complex number.
Proof (Lean source)
1 supporting declaration (lemmas, instances)
-
sincBox_integrabletheorem — The compactly supported interval density defining sincBox is Lebesgue integrable.conclusionProof (Lean source)
theorem sincBox_integrable : Integrable sincBox := by unfold sincBox exact (continuous_const.integrableOn_Icc.mono_set Set.Ioc_subset_Icc_self).integrable_indicator measurableSet_Ioc
BerryEsseenCore 1 core · 0 supporting This module isolates the probability-theoretic Berry–Esseen step from the cross-fitting model. ★ iid_real_berry_esseen
Quantitative scalar normal approximation for an iid real law
This module isolates the probability-theoretic Berry–Esseen step from the cross-fitting model. The law is on the real line and the sample has its finite product distribution. The third absolute moment is explicitly integrable; its numerical upper bound alone would not imply integrability in Lean.
For a centered real law with positive variance σ2 and integrable third absolute moment at most M3, and any positive number n of independent draws, the CDF of the sum divided by √n·√σ2 differs from the standard Gaussian CDF at every threshold x by at most M3/((√σ2)³·√n): the scalar Berry–Esseen bound with universal constant one.
Formal statement
Proof (Lean source)
BerryEsseenFourierIntegral 1 core · 0 supporting The pointwise iid product estimate is integrated over its valid frequency window. ★ iid_unit_variance_charFun_interval_integral_bound
Integrated local characteristic-function estimate
The pointwise iid product estimate is integrated over its valid frequency window. This quantitative analytic step is independent of CDF smoothing.
For a centered unit-variance real law with integrable third absolute moment at most M3, where M3 is at least one, and a sample size n of at least two, the integral over the local window |t| ≤ √n/M3 of the distance between the characteristic function of the standardized iid sum and the standard Gaussian characteristic function, divided by |t|, is at most 9·M3/√n.
Formal statement
Proof (Lean source)
BerryEsseenGaussian 1 core · 0 supporting The characteristic function exp(−t²/2) of the standard normal law differs from its second-order Taylor polynomial 1 − t²/2 by at most t⁴/8, for every real t. ★ gaussian_charFun_quadratic_remainder
Quadratic approximation of the Gaussian characteristic function
The characteristic function exp(−t²/2) of the standard normal law differs from its second-order Taylor polynomial 1 − t²/2 by at most t⁴/8, for every real t. This is the Gaussian half of the local characteristic-function comparison in the Berry–Esseen proof: near the origin, both the characteristic function of a standardized law and that of the normal law are compared with the same quadratic.
Main results
* gaussian_charFun_quadratic_remainder — the bound |exp(−t²/2) − (1 − t²/2)| ≤ t⁴/8, deduced
from |exp(−u) − (1 − u)| ≤ u²/2 for u ≥ 0.
The standard Gaussian characteristic function differs from its quadratic Taylor polynomial 1 − t²/2 by at most t⁴/8 at every real frequency t.
Formal statement
Proof (Lean source)
BerryEsseenIIDEnvelopes 1 core · 1 supporting These analytic estimates connect the proved one-observation moment bounds to the deterministic smoothing budget. ★ iid_unit_variance_charFun_prawitz_discrepancy_bound
Iid powers under the explicit Prawitz moment envelopes
These analytic estimates connect the proved one-observation moment bounds to the deterministic smoothing budget. They import neither a CDF smoothing comparison nor any numerical allocation. Both estimates retain sample sizes at least two; the moment lower bound is explicit and can later be discharged by unit_second_moment_third_absolute_moment_ge_one.
For a centered unit-variance probability law with integrable third absolute moment at most a bound M3 no smaller than one, a sample size n of at least two, and a frequency t in the full outer Prawitz band |t| ≤ 12√n/(5·M3), the distance between the characteristic function of the standardized iid sum and the standard Gaussian characteristic function is at most Prawitz's discrepancy envelope at ratio M3/√n.
Formal statement
Proof (Lean source)
1 supporting declaration (lemmas, instances)
-
iid_unit_variance_charFun_prawitz_moment_boundtheorem — For a centered unit-variance probability law with third absolute moment at most a bound no smaller than one, the standardized iid characteristic-function power at every frequency and sample size at least two is bounded by the explicit cubic moment envelope.hypothesesμ :M3 :ℝhM3 :1 ≤ M3hmean_int :Integrable (fun x : ℝ => x) μhmean :∫ x : ℝ, x ∂μ = 0hvar_int :Integrable (fun x : ℝ => x ^ 2) μhvar :∫ x : ℝ, x ^ 2 ∂μ = 1hthird_int :Integrable (fun x : ℝ => |x| ^ 3) μhthird :∫ x : ℝ, |x| ^ 3 ∂μ ≤ M3n :ℕhn :2 ≤ nt :ℝconclusion≤ prawitzMomentEnvelope (M3 / sqrt (n : ℝ)) tProof (Lean source)
theorem iid_unit_variance_charFun_prawitz_moment_bound (μ : Measure ℝ) [IsProbabilityMeasure μ] (M3 : ℝ) (hM3 : 1 ≤ M3) (hmean_int : Integrable (fun x : ℝ => x) μ) (hmean : ∫ x : ℝ, x ∂μ = 0) (hvar_int : Integrable (fun x : ℝ => x ^ 2) μ) (hvar : ∫ x : ℝ, x ^ 2 ∂μ = 1) (hthird_int : Integrable (fun x : ℝ => |x| ^ 3) μ) (hthird : ∫ x : ℝ, |x| ^ 3 ∂μ ≤ M3) (n : ℕ) (hn : 2 ≤ n) (t : ℝ) : ‖(charFun μ (t / sqrt (n : ℝ))) ^ n‖ ≤ prawitzMomentEnvelope (M3 / sqrt (n : ℝ)) t := by /- Put u=t/sqrt(n). The proved squared modulus is bounded by 1-u²+(M3+1)|u|³/5 <= exp(-u²+(M3+1)|u|³/5). Taking square roots and raising to n gives exp(-t²/2+ (M3+1)|t|³/(10*sqrt(n))). Since M3>=1 this is at most exp(-t²/2+rho|t|³/5). Independently norm_charFun_le_one and norm_pow bound the power by one. No frequency restriction is needed. Use Real.add_one_le_exp, Real.exp_nat_mul, and sqrt(n)^2=n. The nonnegative squared modulus justifies taking the square root even when the intermediate polynomial was not separately proved positive. -/ have hnreal : (2 : ℝ) ≤ n := by exact_mod_cast hn have hspos : 0 < sqrt (n : ℝ) := by positivity have hsne := ne_of_gt hspos have hs2 : sqrt (n : ℝ) ^ 2 = n := Real.sq_sqrt (by positivity) have ha := norm_le_exp_cubic_of_sq_bound _ M3 _ hM3 (unit_variance_charFun_norm_sq_cubic_bound μ M3 hmean_int hmean hvar_int hvar hthird_int hthird (t / sqrt (n : ℝ))) rw [prawitzMomentEnvelope, norm_pow] apply le_min · simpa using pow_le_pow_left₀ (norm_nonneg _) (norm_charFun_le_one (μ := μ) (t / sqrt (n : ℝ))) n · calc ‖charFun μ (t / sqrt (n : ℝ))‖ ^ n ≤ (exp ( -((t / sqrt (n : ℝ)) ^ 2 / 2) + M3 * |t / sqrt (n : ℝ)| ^ 3 / 5)) ^ n := pow_le_pow_left₀ (norm_nonneg _) ha n _ = exp (-(t ^ 2 / 2) + (M3 / sqrt (n : ℝ)) * |t| ^ 3 / 5) := by rw [← Real.exp_nat_mul] congr 1 generalize hs : sqrt (n : ℝ) = s at * rw [abs_div, abs_of_pos hspos, div_pow, div_pow, ← hs2] field_simp
BerryEsseenLocalProduct 1 core · 0 supporting The Taylor estimates for one centered draw and for a Gaussian become a frequency-dependent estimate for their powers. ★ iid_unit_variance_charFun_local_product_bound
Local product estimate for a standardized iid characteristic function
The Taylor estimates for one centered draw and for a Gaussian become a frequency-dependent estimate for their powers. The frequency cutoff is the natural third-moment scale used by a scalar Berry–Esseen proof.
For a centered unit-variance real law with integrable third absolute moment at most M3, where M3 is at least one, a sample size n of at least two, and a frequency with |t| ≤ √n/M3, the characteristic function of the standardized iid sum differs from the standard Gaussian characteristic function by at most (7·M3/(24√n))·|t|³·exp(−t²/6), an explicit cubic error with Gaussian decay.
Formal statement
Proof (Lean source)
BerryEsseenMomentLowerBound 1 core · 1 supporting The third absolute moment of a unit-second-moment probability law is at least one. ★ variance_third_absolute_moment_lower_bound
Third absolute moments and the Berry–Esseen endpoint
The third absolute moment of a unit-second-moment probability law is at least one. Scaling gives the corresponding lower bound at arbitrary positive variance, which closes the one-observation case without a normal approximation. This module imports no quantitative central limit or smoothing theorem.
For a centered scalar probability law with positive variance σ2 and integrable third absolute moment at most M3, M3 is at least the cube of the standard deviation √σ2.
Formal statement
Proof (Lean source)
1 supporting declaration (lemmas, instances)
-
unit_second_moment_third_absolute_moment_ge_onetheorem — A real probability law with second moment one and integrable third absolute moment has third absolute moment at least one.hypothesesμ :hsecond_int :Integrable (fun x : ℝ => x ^ 2) μhsecond :∫ x : ℝ, x ^ 2 ∂μ = 1hthird_int :Integrable (fun x : ℝ => |x| ^ 3) μconclusion1 ≤ ∫ x : ℝ, |x| ^ 3 ∂μProof (Lean source)
theorem unit_second_moment_third_absolute_moment_ge_one (μ : Measure ℝ) [IsProbabilityMeasure μ] (hsecond_int : Integrable (fun x : ℝ => x ^ 2) μ) (hsecond : ∫ x : ℝ, x ^ 2 ∂μ = 1) (hthird_int : Integrable (fun x : ℝ => |x| ^ 3) μ) : 1 ≤ ∫ x : ℝ, |x| ^ 3 ∂μ := by /- No general Holder infrastructure is needed here. For r=|x|≥0, (r-1)^2*(2*r+1)≥0 gives (3/2)*x^2-1/2≤|x|^3. Integrate this pointwise inequality using integral_mono, integral_sub, integral_const_mul, and the probability-law normalization. -/ have hpoint (x : ℝ) : (3 / 2 : ℝ) * x ^ 2 - 1 / 2 ≤ |x| ^ 3 := by have hnonneg : 0 ≤ (|x| - 1) ^ 2 * (2 * |x| + 1) := mul_nonneg (sq_nonneg _) (by positivity) have hsquare : |x| ^ 2 = x ^ 2 := sq_abs x nlinarith have hscaled_int := hsecond_int.const_mul (3 / 2 : ℝ) have hconst_int : Integrable (fun _ : ℝ => (1 / 2 : ℝ)) μ := integrable_const _ have hbound := integral_mono (hscaled_int.sub hconst_int) hthird_int hpoint change (∫ x : ℝ, (3 / 2 : ℝ) * x ^ 2 - 1 / 2 ∂μ) ≤ ∫ x : ℝ, |x| ^ 3 ∂μ at hbound rw [integral_sub hscaled_int hconst_int, integral_const_mul, hsecond] at hbound norm_num at hbound exact hbound
BerryEsseenPrawitzBudget 1 core · 0 supporting The unchanged explicit smoothing envelope is bounded by four focused sufficient estimates. ★ prawitz_berry_esseen_budget
A numerical budget for the sharper Berry–Esseen route
The unchanged explicit smoothing envelope is bounded by four focused sufficient estimates. The three integral allocations are 1/4, 3/20, and 3/5 of the ratio, summing to one. Each estimate is proved in its own imported module; this module only combines them.
For a third-moment ratio ρ strictly between zero and one, with inner cutoff U0 = max(3/2, √(4 log(1/ρ))) and outer cutoff U = 12/(5ρ), the inner cutoff is at most the outer cutoff and the full deterministic Prawitz smoothing envelope at these cutoffs is at most ρ.
Formal statement
Proof (Lean source)
BerryEsseenRefinedFourierIntegral 1 core · 0 supporting The refined characteristic-function product estimate is integrated on its half-size frequency window with a useful numerical constant. ★ iid_unit_variance_charFun_refined_interval_integral_bound
Integrated refined local iid Fourier estimate
The refined characteristic-function product estimate is integrated on its half-size frequency window with a useful numerical constant.
For a centered unit-variance real law with integrable third absolute moment at most M3, where M3 is at least one, and a sample size n of at least four, the integral over the refined window |t| ≤ √n/(2·M3) of the distance between the characteristic function of the standardized iid sum and the standard Gaussian characteristic function, divided by |t|, is at most 2·M3/√n.
Formal statement
Proof (Lean source)
BerryEsseenRefinedLocalProduct 1 core · 0 supporting On a smaller frequency window the third-moment Taylor error allows a stronger Gaussian damping factor. ★ iid_unit_variance_charFun_refined_local_product_bound
Refined local characteristic-function product estimate
On a smaller frequency window the third-moment Taylor error allows a stronger Gaussian damping factor. This analytic estimate is separate from the CDF inversion and finite-sample normal approximation steps.
For a centered unit-variance real law with integrable third absolute moment at most M3, where M3 is at least one, a sample size n of at least four, and a frequency in the half-size window |t| ≤ √n/(2·M3), the characteristic function of the standardized iid sum differs from the standard Gaussian characteristic function by at most (M3/(4√n))·|t|³·exp(−t²/4).
Formal statement
Proof (Lean source)
BerryEsseenSinc4Baseline 1 core · 0 supporting The already-proved Fourier and CDF sandwich estimates yield an explicit normal smoothing bound. ★ normal_cdf_smoothing_sinc4_baseline
Baseline normal smoothing via the fourth-power sinc kernel
The already-proved Fourier and CDF sandwich estimates yield an explicit normal smoothing bound. Its Gaussian error constant records exactly what this kernel proves; a sharper inversion step is needed for Esseen's constant.
For a scalar probability law with finite first moment and a positive bandwidth T, its CDF at every threshold x differs from the standard Gaussian CDF by at most 1/π times the integral over [−T, T] of the characteristic-function discrepancy divided by |t|, plus 24/(T√(2π)).
Formal statement
Proof (Lean source)
BerryEsseenSmoothing 1 core · 1 supporting This module states the Fourier-to-CDF estimate needed by a quantitative scalar central limit theorem. ★ normal_cdf_smoothing
Gaussian smoothing bound for distribution functions
This module states the Fourier-to-CDF estimate needed by a quantitative scalar central limit theorem. It is independent of the cross-fitting model and of the iid characteristic-function estimates.
For a real probability law with finite first moment and a positive bandwidth T, its CDF at every threshold x differs from the standard Gaussian CDF by at most 1/π times the integral over [−T, T] of the characteristic-function discrepancy divided by |t|, plus the smoothing error 24/(πT√(2π)). The constant 24/π is the usual Esseen smoothing constant.
Formal statement
Proof (Lean source)
1 supporting declaration (lemmas, instances)
-
charFun_normal_quotient_intervalIntegrabletheorem — With a finite first moment, the characteristic-function difference from the standard Gaussian divided by frequency is locally integrable, including across frequency zero.hypothesesconclusionProof (Lean source)
theorem charFun_normal_quotient_intervalIntegrable (μ : Measure ℝ) [IsProbabilityMeasure μ] (hfirst : Integrable (fun y : ℝ => y) μ) (T : ℝ) : IntervalIntegrable (fun t : ℝ => ‖charFun μ t - charFun (gaussianReal 0 1) t‖ / |t|) volume (-T) T := by have hchar (ν : Measure ℝ) [IsProbabilityMeasure ν] (hν : Integrable (fun y : ℝ => y) ν) (t : ℝ) : ‖charFun ν t - 1‖ ≤ |t| * ∫ y, |y| ∂ν := by have he : Integrable (fun y : ℝ => exp ((t * y : ℝ) * I)) ν := by apply Integrable.of_bound (by fun_prop) 1 filter_upwards [] with y simpa [mul_comm] using (Complex.norm_exp_I_mul_ofReal (t * y)).le have hEq : charFun ν t - 1 = ∫ y, (exp ((t * y : ℝ) * I) - 1) ∂ν := by rw [charFun_apply_real] simp only [← Complex.ofReal_mul] rw [integral_sub he (integrable_const 1)] simp rw [hEq] calc ‖∫ y, (exp ((t * y : ℝ) * I) - 1) ∂ν‖ ≤ ∫ y, |t| * |y| ∂ν := by apply norm_integral_le_of_norm_le (hν.norm.const_mul |t|) filter_upwards [] with y have hp := Real.norm_exp_I_mul_ofReal_sub_one_le (x := t * y) simpa [Real.norm_eq_abs, abs_mul, mul_comm] using hp _ = |t| * ∫ y, |y| ∂ν := by rw [integral_const_mul] have hg : Integrable (fun y : ℝ => y) (gaussianReal 0 1) := by exact memLp_one_iff_integrable.mp (ProbabilityTheory.memLp_id_gaussianReal (μ := 0) (v := 1) 1) have hbound : ∀ t : ℝ, t ≠ 0 → ‖charFun μ t - charFun (gaussianReal 0 1) t‖ / |t| ≤ (∫ y, |y| ∂μ) + (∫ y, |y| ∂(gaussianReal 0 1)) := by intro t ht have htpos : 0 < |t| := abs_pos.mpr ht have hμ := hchar μ hfirst t have hγ := hchar (gaussianReal 0 1) hg t have htri : ‖charFun μ t - charFun (gaussianReal 0 1) t‖ ≤ ‖charFun μ t - 1‖ + ‖charFun (gaussianReal 0 1) t - 1‖ := by convert norm_sub_le (charFun μ t - 1) (charFun (gaussianReal 0 1) t - 1) using 1 ring_nf apply (div_le_iff₀ htpos).2 nlinarith have hmeas : Measurable (fun t : ℝ => ‖charFun μ t - charFun (gaussianReal 0 1) t‖ / |t|) := by fun_prop apply (intervalIntegrable_iff).2 apply IntegrableOn.of_bound (by rw [Real.volume_uIoc]; exact ENNReal.ofReal_lt_top) hmeas.aestronglyMeasurable ((∫ y, |y| ∂μ) + (∫ y, |y| ∂(gaussianReal 0 1))) filter_upwards [] with t by_cases ht : t = 0 · subst t simp only [charFun_zero, probReal_univ, Complex.ofReal_one, sub_self, norm_zero, abs_zero, div_zero] exact add_nonneg (integral_nonneg (fun y => abs_nonneg y)) (integral_nonneg (fun y => abs_nonneg y)) · simpa [Real.norm_eq_abs, abs_of_nonneg (div_nonneg (norm_nonneg _) (abs_nonneg t))] using hbound t ht
BerryEsseenStandardize 1 core · 1 supporting These identities separate variance normalization from the quantitative unit-variance normal approximation. ★ standardized_iid_sum_event
Scaling a scalar iid law to unit variance
These identities separate variance normalization from the quantitative unit-variance normal approximation. They apply to any positive variance.
For a positive scale σ2, the n-fold iid product of a law gives the event "sum divided by √n·√σ2 is at most x" the same probability as the n-fold iid product of the law rescaled by 1/√σ2 gives the event "sum divided by √n is at most x": standardizing each coordinate before summing is the same as standardizing the sum afterward.
Formal statement
Proof (Lean source)
1 supporting declaration (lemmas, instances)
-
standardized_law_momentstheorem — Dividing a centered scalar law by its positive standard deviation gives an integrable law of mean zero and variance one; its third absolute moment is divided by the cube of that standard deviation.hypothesesμ :σ2 M3 :ℝhσ2 :0 < σ2hmean_int :Integrable (fun x : ℝ => x) μhmean :∫ x : ℝ, x ∂μ = 0hvar_int :Integrable (fun x : ℝ => x ^ 2) μhvar :∫ x : ℝ, x ^ 2 ∂μ = σ2hthird_int :Integrable (fun x : ℝ => |x| ^ 3) μhthird :∫ x : ℝ, |x| ^ 3 ∂μ ≤ M3conclusionν :μ.map (fun x : ℝ => x / sqrt σ2)Integrable (fun x : ℝ => x) ν∫ x : ℝ, x ∂ν = 0Integrable (fun x : ℝ => x ^ 2) ν∫ x : ℝ, x ^ 2 ∂ν = 1Integrable (fun x : ℝ => |x| ^ 3) ν∫ x : ℝ, |x| ^ 3 ∂ν ≤ M3 / (sqrt σ2) ^ 3Proof (Lean source)
theorem standardized_law_moments (μ : Measure ℝ) [IsProbabilityMeasure μ] (σ2 M3 : ℝ) (hσ2 : 0 < σ2) (hmean_int : Integrable (fun x : ℝ => x) μ) (hmean : ∫ x : ℝ, x ∂μ = 0) (hvar_int : Integrable (fun x : ℝ => x ^ 2) μ) (hvar : ∫ x : ℝ, x ^ 2 ∂μ = σ2) (hthird_int : Integrable (fun x : ℝ => |x| ^ 3) μ) (hthird : ∫ x : ℝ, |x| ^ 3 ∂μ ≤ M3) : let ν := μ.map (fun x : ℝ => x / sqrt σ2) Integrable (fun x : ℝ => x) ν ∧ (∫ x : ℝ, x ∂ν = 0) ∧ Integrable (fun x : ℝ => x ^ 2) ν ∧ (∫ x : ℝ, x ^ 2 ∂ν = 1) ∧ Integrable (fun x : ℝ => |x| ^ 3) ν ∧ (∫ x : ℝ, |x| ^ 3 ∂ν ≤ M3 / (sqrt σ2) ^ 3) := by have hr : 0 < sqrt σ2 := Real.sqrt_pos.2 hσ2 have h2 : ∀ y : ℝ, (y / sqrt σ2) ^ 2 = y ^ 2 / (sqrt σ2) ^ 2 := fun y => div_pow y (sqrt σ2) 2 have h3 : ∀ y : ℝ, |y / sqrt σ2| ^ 3 = |y| ^ 3 / (sqrt σ2) ^ 3 := by intro y rw [abs_div, abs_of_pos hr, div_pow] change Integrable (fun x : ℝ => x) (μ.map (fun y => y / sqrt σ2)) ∧ (∫ x : ℝ, x ∂μ.map (fun y => y / sqrt σ2)) = 0 ∧ Integrable (fun x : ℝ => x ^ 2) (μ.map (fun y => y / sqrt σ2)) ∧ (∫ x : ℝ, x ^ 2 ∂μ.map (fun y => y / sqrt σ2)) = 1 ∧ Integrable (fun x : ℝ => |x| ^ 3) (μ.map (fun y => y / sqrt σ2)) ∧ (∫ x : ℝ, |x| ^ 3 ∂μ.map (fun y => y / sqrt σ2)) ≤ M3 / (sqrt σ2) ^ 3 refine ⟨?_, ?_, ?_, ?_, ?_, ?_⟩ · exact (integrable_map_measure (by fun_prop) (by fun_prop)).2 (by simpa [Function.comp_def] using hmean_int.div_const (sqrt σ2)) · rw [integral_map (by fun_prop) (by fun_prop), integral_div, hmean, zero_div] · exact (integrable_map_measure (by fun_prop) (by fun_prop)).2 (by simpa only [Function.comp_def, h2] using hvar_int.div_const ((sqrt σ2) ^ 2)) · rw [integral_map (by fun_prop) (by fun_prop)] simp_rw [h2] rw [integral_div, hvar, Real.sq_sqrt (le_of_lt hσ2), div_self (ne_of_gt hσ2)] · exact (integrable_map_measure (by fun_prop) (by fun_prop)).2 (by simpa only [Function.comp_def, h3] using hthird_int.div_const ((sqrt σ2) ^ 3)) · rw [integral_map (by fun_prop) (by fun_prop)] simp_rw [h3] rw [integral_div] exact (div_le_div_iff_of_pos_right (pow_pos hr 3)).2 hthird
BerryEsseenTaylor 1 core · 1 supporting This module isolates the local analytic estimate needed for a quantitative scalar central limit theorem. ★ centered_charFun_quadratic_remainder
The third-order characteristic-function estimate
This module isolates the local analytic estimate needed for a quantitative scalar central limit theorem. The bound is for an arbitrary real frequency and does not assume a limiting normal approximation.
For a centered real probability law with integrable second moment σ2 and integrable third absolute moment at most M3, the characteristic function at every real frequency t lies within M3·|t|³/6 of the variance quadratic 1 − σ2·t²/2.
Formal statement
Proof (Lean source)
1 supporting declaration (lemmas, instances)
-
exp_imag_quadratic_remaindertheorem — For a real argument, the complex exponential on the imaginary axis differs from its quadratic Taylor polynomial by at most one sixth of the cubed absolute argument.hypothesesu :ℝProof (Lean source)
theorem exp_imag_quadratic_remainder (u : ℝ) : ‖Complex.exp ((u : ℂ) * I) - (1 + (u : ℂ) * I + ((u : ℂ) * I) ^ 2 / 2)‖ ≤ |u| ^ 3 / 6 := by let f : ℝ → ℂ := fun t => exp ((t : ℂ) * I) have hc : ContDiff ℝ ⊤ (fun t : ℝ => (t : ℂ)) := by convert (Complex.ofRealCLM.contDiff : ContDiff ℝ ⊤ (Complex.ofRealCLM : ℝ → ℂ)) using 1 funext t rfl have hf : ContDiff ℝ ⊤ f := by have hm : ContDiff ℝ ⊤ (fun t : ℝ => (t : ℂ) * I) := hc.mul contDiff_const exact Complex.contDiff_exp.comp hm have hd (t : ℝ) : HasDerivAt f (I * f t) t := by dsimp [f] convert ((Complex.hasDerivAt_exp ((t : ℂ) * I)).comp (t : ℂ) (hasDerivAt_mul_const I)).comp_ofReal using 1 · funext s simp [mul_comm] · ring have hn (n : ℕ) (t : ℝ) : iteratedDeriv n f t = I ^ n * f t := by induction n with | zero => simp [iteratedDeriv_zero] | succ n ih => rw [iteratedDeriv_succ'] have hfun : deriv f = fun x => I * f x := funext fun x => (hd x).deriv rw [hfun] rw [iteratedDeriv_const_mul I (hf.contDiffAt.of_le (by simp))] rw [ih] ring by_cases hu : u = 0 · subst u norm_num [f] have hs : UniqueDiffOn ℝ (uIcc 0 u) := uniqueDiffOn_uIcc (Ne.symm hu) have hi (n : ℕ) (t : ℝ) (ht : t ∈ uIcc 0 u) : iteratedDerivWithin n f (uIcc 0 u) t = I ^ n * f t := by rw [iteratedDerivWithin_eq_iteratedDeriv hs (hf.contDiffAt.of_le (by simp)) ht, hn] have hz : (0 : ℝ) ∈ uIcc 0 u := Set.left_mem_uIcc have htaylor : taylorWithinEval f 2 (uIcc 0 u) 0 u = 1 + (u : ℂ) * I + ((u : ℂ) * I) ^ 2 / 2 := by have hzero (n : ℕ) : iteratedDerivWithin n f (uIcc 0 u) 0 = I ^ n := by rw [hi n 0 hz] simp [f] rw [taylor_within_apply] simp [Finset.sum_range_succ, hzero] rw [mul_pow, Complex.I_sq] ring have hrem := taylor_integral_remainder (f := f) (x := u) (x₀ := 0) (n := 2) (hf.contDiffOn.of_le (by simp)) rw [htaylor] at hrem have hpoint (t : ℝ) (ht : t ∈ uIcc 0 u) : ‖((u - t) ^ 2 / (2 : ℝ)) • iteratedDerivWithin 3 f (uIcc 0 u) t‖ ≤ (u - t) ^ 2 / 2 := by rw [hi 3 t ht, norm_smul, norm_mul, norm_pow, Complex.norm_I] simp [f, Complex.norm_exp_ofReal_mul_I] calc ‖Complex.exp ((u : ℂ) * I) - (1 + (u : ℂ) * I + ((u : ℂ) * I) ^ 2 / 2)‖ = ‖∫ t : ℝ in 0..u, ((u - t) ^ 2 / (2 : ℝ)) • iteratedDerivWithin 3 f (uIcc 0 u) t‖ := by simpa [f] using congrArg norm hrem _ ≤ |∫ t : ℝ in 0..u, (u - t) ^ 2 / 2| := by apply intervalIntegral.norm_integral_le_abs_of_norm_le · filter_upwards [ae_restrict_mem measurableSet_uIoc] with t ht exact hpoint t (Set.uIoc_subset_uIcc ht) · exact (by fun_prop : Continuous (fun t : ℝ => (u - t) ^ 2 / 2)).intervalIntegrable 0 u _ = |u| ^ 3 / 6 := by have h := intervalIntegral.integral_comp_sub_left (fun x : ℝ => x ^ 2 / 2) u (a := 0) (b := u) simp only [sub_self, sub_zero] at h rw [h, intervalIntegral.integral_div, integral_pow] norm_num [abs_div, abs_pow] ring
BerryEsseenUnit 1 core · 0 supporting The constant-one scalar probability bound is isolated at unit variance, leaving rescaling and the one-observation endpoint to the general theorem. ★ iid_unit_variance_berry_esseen
Unit-variance iid Berry–Esseen inequality
The constant-one scalar probability bound is isolated at unit variance, leaving rescaling and the one-observation endpoint to the general theorem. The standardized sum's pushforward law transfers the iid Fourier envelopes to the Prawitz smoothing inequality and its deterministic budget.
For a centered unit-variance scalar law with integrable third absolute moment at most M3 and any sample size n of at least two, the CDF of the iid sum divided by √n differs from the standard Gaussian CDF at every threshold x by at most M3/√n.
Formal statement
Proof (Lean source)
BerryEsseenWideCharFun 1 core · 0 supporting Prawitz's cubic modulus estimate is isolated for one centered unit-variance law. ★ unit_variance_charFun_norm_sq_cubic_bound
Wide-window scalar characteristic-function damping
Prawitz's cubic modulus estimate is isolated for one centered unit-variance law. Unlike a Taylor triangle bound on a small frequency window, it gives useful damping up to frequencies of order the inverse third moment.
Reference: Tyurin, arXiv:0912.0726, Lemma 1 (pervoe) and the displayed definition of b(t,γ). The optimal cosine-remainder coefficient is below 0.1, so replacing it by 1/10 yields the conservative polynomial below.
For a centered unit-variance law with integrable third absolute moment at most M3, the squared modulus of the characteristic function at every real frequency t is at most 1 − t² + (M3 + 1)·|t|³/5.
Formal statement
Proof (Lean source)
CDFDifferenceFourier 1 core · 0 supporting The Fourier transform of the difference of two CDFs is identified with the difference of their characteristic functions away from frequency zero. ★ cdf_difference_fourier_identity
Fourier transform of a difference of distribution functions
The Fourier transform of the difference of two CDFs is identified with the difference of their characteristic functions away from frequency zero. Finite first moments supply the integrability needed for the identity.
For two probability laws μ and ν with finite first moments and a nonzero frequency t, t times the Fourier integral of the difference of their CDFs equals i times the difference of their characteristic functions at t; that is, the Fourier integral is (i/t)(φ_μ(t) − φ_ν(t)), written so as to avoid division at zero.
Formal statement
Proof (Lean source)
CDFDifferenceFourierEndpoint 1 core · 0 supporting This module evaluates the oriented interval kernel after averaging its two endpoints over independent probability laws. ★ orientedFourierKernel_endpoint_integral
Endpoint average of the oriented Fourier kernel
This module evaluates the oriented interval kernel after averaging its two endpoints over independent probability laws. It is one input to Fubini.
For two probability laws μ and ν on the real line, averaging the oriented Fourier kernel at frequency t and point x over independent draws a from μ and b from ν gives the Fourier exponential exp(itx) times the difference of the two CDFs at x. The weak endpoint inequalities preserve this identity at atoms.
Formal statement
Proof (Lean source)
CDFDifferenceFourierFubini 1 core · 1 supporting An oriented interval between two observations has signed indicator equal to the difference of their lower-half-line indicators. ★ cdf_difference_fourier_fubini
A Fubini bridge for Fourier transforms of CDF differences
An oriented interval between two observations has signed indicator equal to the difference of their lower-half-line indicators. Integrating this identity against two probability laws is the measure-theoretic step in the Fourier identity for their CDF difference.
For two probability laws μ and ν with finite first moments, the Fourier integral at frequency t of the difference of their CDFs equals the average, over independent draws a from μ and b from ν, of the oriented integral of the Fourier exponential from a to b.
Formal statement
Proof (Lean source)
1 supporting declaration (lemmas, instances)
-
fourier_oriented_interval_identitytheorem — For a nonzero frequency, the oriented integral of the complex exponential between two real points equals the difference of their endpoint exponentials divided by the frequency, with the Fourier sign convention used here.hypothesesa b t :ℝht :t ≠ 0Proof (Lean source)
theorem fourier_oriented_interval_identity (a b t : ℝ) (ht : t ≠ 0) : (t : ℂ) * (∫ x in a..b, exp (((t * x : ℝ) : ℂ) * I)) = I * (exp (((t * a : ℝ) : ℂ) * I) - exp (((t * b : ℝ) : ℂ) * I)) := by have hc : (t : ℂ) * I ≠ 0 := mul_ne_zero (by exact_mod_cast ht) Complex.I_ne_zero have he : (fun x : ℝ => exp (((t * x : ℝ) : ℂ) * I)) = (fun x : ℝ => exp (((t : ℂ) * I) * x)) := by funext x congr 1 push_cast ring rw [he, integral_exp_mul_complex hc] push_cast have htC : (t : ℂ) ≠ 0 := by exact_mod_cast ht field_simp [htC] rw [Complex.I_sq] ring
CDFDifferenceFourierInterval 1 core · 0 supporting This module evaluates the oriented interval kernel in its Lebesgue variable. ★ orientedFourierKernel_interval_integral
Lebesgue integral of the oriented Fourier kernel
This module evaluates the oriented interval kernel in its Lebesgue variable. It is the other input to the CDF Fourier Fubini interchange.
Integrating the oriented Fourier kernel over the real line gives the oriented interval integral of the Fourier exponential exp(itx) from a to b.
Formal statement
Proof (Lean source)
CDFDifferenceFourierQuotient 1 core · 0 supporting The nonzero-frequency CDF Fourier identity becomes an equality of truncated real magnitude integrals. ★ cdf_difference_fourier_magnitude_integral
Weighted Fourier magnitude of a CDF difference
The nonzero-frequency CDF Fourier identity becomes an equality of truncated real magnitude integrals. Frequency zero is a null singleton for Lebesgue measure, so no atomlessness of either probability law is required.
For two probability laws with finite first moments, the integral over [−T, T] of the magnitude of the Fourier transform of their CDF difference equals the integral over [−T, T] of their characteristic-function discrepancy divided by |t|.
Formal statement
Proof (Lean source)
CDFDifferenceFourierShift 1 core · 0 supporting Reflection around a fixed point converts the spatial integral arising from convolution into the ordinary Fourier transform of a CDF difference. ★ cdf_difference_fourier_shift
Translation of a CDF difference Fourier integral
Reflection around a fixed point converts the spatial integral arising from convolution into the ordinary Fourier transform of a CDF difference.
For two probability laws with finite first moments, the integral of exp(−ity) times their CDF difference evaluated at z − y equals the phase exp(−itz) times the Fourier integral at frequency t of their CDF difference: reflecting the argument about z extracts that phase.
Formal statement
Proof (Lean source)
CDFDifferenceIntegrable 1 core · 0 supporting Finite first moments control the positive and negative CDF tails of two probability laws. ★ integrable_cdf_difference_of_first_moments
Integrability of a difference of distribution functions
Finite first moments control the positive and negative CDF tails of two probability laws. Their CDF difference is therefore Lebesgue integrable.
For two real probability laws with finite first moments, the difference of their cumulative distribution functions is Lebesgue integrable.
Formal statement
Proof (Lean source)
CDFDifferenceModulus 1 core · 0 supporting An interval-mass bound on a reference law controls how far the difference of two cumulative distribution functions can fall as its argument increases. ★ cdf_difference_one_sided_modulus
One-sided modulus of a difference of distribution functions
An interval-mass bound on a reference law controls how far the difference of two cumulative distribution functions can fall as its argument increases. This is the pointwise order estimate used before integrating a smoothing kernel.
If ν assigns every interval at most L times its length, then for any points a ≤ b the CDF difference Fμ − Fν at a is at most its value at b plus L·(b − a).
Formal statement
Proof (Lean source)
CDFGeneralSandwich 1 core · 0 supporting This comparison isolates the concentration needed from a smoothing kernel. ★ cdf_general_kernel_sandwich
CDF smoothing with an abstract probability kernel
This comparison isolates the concentration needed from a smoothing kernel. It permits a sharper band-limited kernel in the Gaussian smoothing theorem.
Let K be an integrable nonnegative probability density that puts mass at most q outside the open interval (−a, a), where a ≥ 0 and q < 1/2. If the reference law ν assigns every interval at most L times its length, for a nonnegative constant L and the CDF difference of μ and ν, convolved with K, is bounded in absolute value at every point by a constant B, then the unsmoothed CDF difference is bounded in absolute value by (B + 2aL)/(1 − 2q) at every point.
Formal statement
Proof (Lean source)
CDFReflection 1 core · 2 supporting Reflection preserves first moments and characteristic-function discrepancies. ★ reflected_reference_interval_and_cdf
Reflection of scalar CDF comparisons
Reflection preserves first moments and characteristic-function discrepancies. For a reference law with bounded interval mass, its absence of atoms supplies the endpoint correction needed to turn an upper CDF bound into a lower bound. These facts do not depend on an Esseen or Berry–Esseen theorem.
If a probability reference law ν assigns every interval at most L times its length, then its reflection y ↦ −y satisfies the same interval bound, and the lower CDF discrepancy Fν(x) − Fμ(x) is at most the upper discrepancy of the reflected laws at −x, even when μ has an atom at x.
Formal statement
Proof (Lean source)
2 supporting declarations (lemmas, instances)
-
reflected_first_moment_integrabletheorem — A scalar law with an integrable first moment retains that property after reflection through the origin.hypothesesμ :Measure ℝhfirst :Integrable (fun y : ℝ => y) μconclusionIntegrable (fun y : ℝ => y) (μ.map (fun y : ℝ => -y))Proof (Lean source)
theorem reflected_first_moment_integrable (μ : Measure ℝ) (hfirst : Integrable (fun y : ℝ => y) μ) : Integrable (fun y : ℝ => y) (μ.map (fun y : ℝ => -y)) := by exact (integrable_map_measure (by fun_prop) (by fun_prop)).2 hfirst.neg -
reflected_charFun_discrepancytheorem — Reflecting two finite scalar laws leaves the magnitude of their characteristic-function difference unchanged at each frequency.hypothesesμ ν :t :ℝProof (Lean source)
theorem reflected_charFun_discrepancy (μ ν : Measure ℝ) [IsFiniteMeasure μ] [IsFiniteMeasure ν] (t : ℝ) : ‖charFun (μ.map (fun y : ℝ => -y)) t - charFun (ν.map (fun y : ℝ => -y)) t‖ = ‖charFun μ t - charFun ν t‖ := by have hm (ρ : Measure ℝ) : charFun (ρ.map (fun y : ℝ => -y)) t = charFun ρ (-t) := by simpa only [neg_one_mul] using (charFun_map_mul (μ := ρ) (-1) t) rw [hm μ, hm ν, charFun_neg, charFun_neg, ← map_sub] exact Complex.norm_conj _
CDFSandwich 1 core · 2 supporting This module isolates the order-theoretic part of the Esseen smoothing argument. ★ standardGaussian_interval_mass_le
A distribution-function sandwich for sinc smoothing
This module isolates the order-theoretic part of the Esseen smoothing argument. A probability kernel with a controlled tail compares an original CDF difference with its smoothed version against a Lipschitz reference CDF.
For real endpoints a ≤ b, the standard Gaussian gives the interval (a, b] probability at most (b − a)/√(2π), the interval length times the maximum of the Gaussian density.
Formal statement
Proof (Lean source)
2 supporting declarations (lemmas, instances)
-
kernel_sandwich_steptheorem — A probability kernel transfers a one-sided comparison outside a tail set to an integral comparison, with tail loss controlled by the uniform bound.hypothesesK G :ℝ → ℝs :Set ℝhs :hK :hG :∀ z, Integrable (fun y => G (z - y) * K y)hkn :∀ y, 0 ≤ K yhki :∫ y, K y = 1q :ℝht :∫ y in s, K y ≤ qD c :ℝhD :0 ≤ Dhc :0 ≤ chGb :∀ y, |G y| ≤ Dx z :ℝhp :∀ y ∉ s, G x ≤ G (z - y) + cconclusionG x ≤ (∫ y, G (z - y) * K y) + c + 2 * q * DProof (Lean source)
theorem kernel_sandwich_step (K G : ℝ → ℝ) (s : Set ℝ) (hs : MeasurableSet s) (hK : Integrable K) (hG : ∀ z, Integrable (fun y => G (z - y) * K y)) (hkn : ∀ y, 0 ≤ K y) (hki : ∫ y, K y = 1) (q : ℝ) (ht : ∫ y in s, K y ≤ q) (D c : ℝ) (hD : 0 ≤ D) (hc : 0 ≤ c) (hGb : ∀ y, |G y| ≤ D) (x z : ℝ) (hp : ∀ y ∉ s, G x ≤ G (z - y) + c) : G x ≤ (∫ y, G (z - y) * K y) + c + 2 * q * D := by have hi : Integrable (s.indicator (fun y => 2 * D * K y)) := (hK.const_mul (2 * D)).integrableOn.integrable_indicator hs have hpt (y : ℝ) : G x * K y ≤ (G (z - y) + c) * K y + s.indicator (fun y => 2 * D * K y) y := by by_cases hy : y ∈ s · rw [Set.indicator_of_mem hy] have h1 := le_abs_self (G x) have h2 := neg_abs_le (G (z - y)) have h3 := hGb x have h4 := hGb (z - y) nlinarith [hkn y] · rw [Set.indicator_of_notMem hy] nlinarith [hp y hy, hkn y] have hl : Integrable (fun y => G x * K y) := hK.const_mul _ have hmidint : Integrable (fun y => (G (z - y) + c) * K y) := by have heq : (fun y => (G (z - y) + c) * K y) = (fun y => G (z - y) * K y) + (fun y => c * K y) := by funext y simp only [Pi.add_apply, add_mul] rw [heq] exact (hG z).add (hK.const_mul c) have hr := hmidint.add hi have hm := integral_mono hl hr hpt have htail : (∫ y, s.indicator (fun y => 2 * D * K y) y) ≤ 2 * q * D := by rw [integral_indicator hs, integral_const_mul] nlinarith [mul_le_mul_of_nonneg_left ht (by positivity : 0 ≤ 2 * D)] have hmiddle : (∫ y, (G (z - y) + c) * K y) = (∫ y, G (z - y) * K y) + c := by calc _ = ∫ y, G (z - y) * K y + c * K y := by congr 1 ext y ring _ = (∫ y, G (z - y) * K y) + ∫ y, c * K y := integral_add (hG z) (hK.const_mul c) _ = _ := by rw [integral_const_mul, hki, mul_one] have hsplit : (∫ y, (G (z - y) + c) * K y + s.indicator (fun y => 2 * D * K y) y) = (∫ y, (G (z - y) + c) * K y) + ∫ y, s.indicator (fun y => 2 * D * K y) y := integral_add hmidint hi have hm' : (∫ y, G x * K y) ≤ (∫ y, (G (z - y) + c) * K y) + ∫ y, s.indicator (fun y => 2 * D * K y) y := by simpa only [Pi.add_apply, hsplit] using hm rw [integral_const_mul, hki, mul_one, hmiddle] at hm' linarith -
sinc4_cdf_sandwichtheorem — If the reference law assigns every interval at most its length times L, and the sinc-smoothed CDF discrepancy is everywhere at most B, then the unsmoothed CDF discrepancy is at most 2 B + 24 L / T.hypothesesμ ν :T L B :ℝhT :0 < ThL :0 ≤ Lhsmooth :x :ℝProof (Lean source)
theorem sinc4_cdf_sandwich (μ ν : Measure ℝ) [IsProbabilityMeasure μ] [IsProbabilityMeasure ν] (T L B : ℝ) (hT : 0 < T) (hL : 0 ≤ L) (hν : ∀ a b : ℝ, a ≤ b → (ν (Ioc a b)).toReal ≤ L * (b - a)) (hsmooth : ∀ z : ℝ, |∫ y : ℝ, ((μ (Iic (z - y))).toReal - (ν (Iic (z - y))).toReal) * sinc4Kernel T y| ≤ B) (x : ℝ) : |(μ (Iic x)).toReal - (ν (Iic x)).toReal| ≤ 2 * B + 24 * L / T := by let H : ℝ → ℝ := fun z => (μ (Iic z)).toReal - (ν (Iic z)).toReal let K : ℝ → ℝ := sinc4Kernel T let a : ℝ := 6 / T let s : Set ℝ := {y | a ≤ |y|} let D : ℝ := sSup (Set.range fun z : ℝ => |H z|) have ha : 0 ≤ a := by dsimp [a]; positivity have hs : MeasurableSet s := measurableSet_le measurable_const measurable_abs have hK : Integrable K := sinc4Kernel_integrable T hT have hkn : ∀ y, 0 ≤ K y := sinc4Kernel_nonneg T hT have hki : ∫ y, K y = 1 := sinc4Kernel_integral_eq_one T hT have ht : ∫ y in s, K y ≤ (1 / 4 : ℝ) := sinc4Kernel_tail_le_quarter T hT have hCDF (ρ : Measure ℝ) [IsProbabilityMeasure ρ] : Measurable (fun z : ℝ => (ρ (Iic z)).toReal) := by have hm := (ProbabilityTheory.monotone_cdf ρ).measurable convert hm using 1 ext z exact (ProbabilityTheory.cdf_eq_real ρ z).symm have hHm : Measurable H := (hCDF μ).sub (hCDF ν) have hHone (z : ℝ) : |H z| ≤ 1 := by have hμ0 : 0 ≤ (μ (Iic z)).toReal := ENNReal.toReal_nonneg have hν0 : 0 ≤ (ν (Iic z)).toReal := ENNReal.toReal_nonneg have hμ1 : (μ (Iic z)).toReal ≤ 1 := by have h := ENNReal.toReal_mono (measure_ne_top μ _) (measure_mono (Set.subset_univ (Iic z))) simpa using h have hν1 : (ν (Iic z)).toReal ≤ 1 := by have h := ENNReal.toReal_mono (measure_ne_top ν _) (measure_mono (Set.subset_univ (Iic z))) simpa using h dsimp [H] rw [abs_le] constructor <;> linarith have hbdd : BddAbove (Set.range fun z : ℝ => |H z|) := by refine ⟨1, ?_⟩ rintro _ ⟨z, rfl⟩ exact hHone z have hD : 0 ≤ D := by have h := le_csSup hbdd (Set.mem_range_self x) exact le_trans (abs_nonneg _) h have hDb (z : ℝ) : |H z| ≤ D := le_csSup hbdd (Set.mem_range_self z) have hD1 : D ≤ 1 := csSup_le (Set.range_nonempty _) (by rintro _ ⟨z, rfl⟩; exact hHone z) have hHint (z : ℝ) : Integrable (fun y => H (z - y) * K y) := by have hm : AEStronglyMeasurable (fun y => H (z - y)) volume := (hHm.comp (measurable_const.sub measurable_id)).aestronglyMeasurable have hb : ∀ᵐ y : ℝ ∂volume, ‖H (z - y)‖ ≤ (1 : ℝ) := by filter_upwards with y simpa only [Real.norm_eq_abs] using hHone (z - y) have heq : (fun y => H (z - y) * K y) = (fun y => K y * H (z - y)) := by funext y ring rw [heq] exact hK.mul_bdd hm hb have hNint (z : ℝ) : Integrable (fun y => (-H (z - y)) * K y) := by have heq : (fun y => (-H (z - y)) * K y) = -(fun y => H (z - y) * K y) := by funext y simp only [Pi.neg_apply, neg_mul] rw [heq] exact (hHint z).neg have hc : 0 ≤ 2 * a * L := by positivity have hpos (z : ℝ) : H z ≤ B + 2 * a * L + D / 2 := by have hp (y : ℝ) (hy : y ∉ s) : H z ≤ H ((z + a) - y) + 2 * a * L := by have hy' : |y| < a := lt_of_not_ge hy have hzy : z ≤ (z + a) - y := by linarith [le_abs_self y] have hd : ((z + a) - y) - z ≤ 2 * a := by linarith [neg_abs_le y] have hm := cdf_difference_one_sided_modulus μ ν L hν z ((z + a) - y) hzy have hmul := mul_le_mul_of_nonneg_left hd hL dsimp [H] linarith have h := kernel_sandwich_step K H s hs hK hHint hkn hki (1 / 4) ht D (2 * a * L) hD hc hDb z (z + a) hp have hb := (le_abs_self (∫ y, H ((z + a) - y) * K y)).trans (hsmooth (z + a)) dsimp [H, K] at hb linarith have hneg (z : ℝ) : -H z ≤ B + 2 * a * L + D / 2 := by have hp (y : ℝ) (hy : y ∉ s) : -H z ≤ -H ((z - a) - y) + 2 * a * L := by have hy' : |y| < a := lt_of_not_ge hy have hzy : (z - a) - y ≤ z := by linarith [neg_abs_le y] have hd : z - ((z - a) - y) ≤ 2 * a := by linarith [le_abs_self y] have hm := cdf_difference_one_sided_modulus μ ν L hν ((z - a) - y) z hzy have hmul := mul_le_mul_of_nonneg_left hd hL dsimp [H] linarith have hnb (w : ℝ) : |(-H w)| ≤ D := by simpa using hDb w have h := kernel_sandwich_step K (fun w => -H w) s hs hK hNint hkn hki (1 / 4) ht D (2 * a * L) hD hc hnb z (z - a) hp have hni : (∫ y, (-H ((z - a) - y)) * K y) = -(∫ y, H ((z - a) - y) * K y) := by rw [← integral_neg] congr 1 ext y ring rw [hni] at h have hb := (neg_le_abs (∫ y, H ((z - a) - y) * K y)).trans (hsmooth (z - a)) dsimp [H, K] at hb linarith have hDtwo : D ≤ B + 2 * a * L + D / 2 := by apply csSup_le (Set.range_nonempty _) rintro _ ⟨z, rfl⟩ exact abs_le.mpr ⟨by linarith [hneg z], by linarith [hpos z]⟩ have hx := hDb x have hfinal : D ≤ 2 * B + 4 * a * L := by linarith dsimp [H] at hx have hconst : 4 * a * L = 24 * L / T := by dsimp [a] field_simp ring rw [← hconst] exact hx.trans hfinal
CosineCubic 1 core · 1 supporting This deterministic leaf isolates the analytic ingredient of the wide characteristic-function estimate and a reusable quartic Taylor enclosure. ★ cos_le_quadratic_add_cubic
Global cubic and quartic cosine remainder bounds
This deterministic leaf isolates the analytic ingredient of the wide characteristic-function estimate and a reusable quartic Taylor enclosure. The cubic coefficient is conservatively rounded up from Tyurin's extremal cosine-remainder constant, approximately 0.099162 (Tyurin, arXiv:0912.0726, the constant defined before Theorem 5).
The cosine of any real argument is bounded above by its quadratic Taylor polynomial 1 − u²/2 plus one tenth of the absolute cube |u|³.
Formal statement
Proof (Lean source)
1 supporting declaration (lemmas, instances)
-
cos_le_quadratic_add_quartictheorem — The cosine of any real argument is bounded above by its quartic Taylor polynomial.Proof (Lean source)
theorem cos_le_quadratic_add_quartic (u : ℝ) : cos u ≤ 1 - u ^ 2 / 2 + u ^ 4 / 24 := by have hd (x : ℝ) : deriv (fun x : ℝ => (1 - x ^ 2 / 2 + x ^ 4 / 24) - cos x) x = sin x - (x - x ^ 3 / 6) := by simp (disch := fun_prop) ring have hm : MonotoneOn (fun x : ℝ => (1 - x ^ 2 / 2 + x ^ 4 / 24) - cos x) (Ici 0) := by apply monotoneOn_of_deriv_nonneg (convex_Ici 0) (by fun_prop) (by fun_prop) intro x hx rw [hd] exact sub_nonneg.mpr (Real.sin_ge_sub_cube (le_of_lt (by simpa using hx))) have h := hm (by simp) (abs_nonneg u) (abs_nonneg u) norm_num [Real.cos_abs, pow_abs, abs_of_nonneg (show 0 ≤ u ^ 2 by positivity), abs_of_nonneg (show 0 ≤ u ^ 4 by positivity)] at h linarith only [h]
CscSquaredSeries 1 core · 0 supporting This real boundary identity is the squared-cosecant companion of Mathlib's cotangent expansion. ★ csc_squared_reciprocal_series
Reciprocal-square partial fractions on the real line
This real boundary identity is the squared-cosecant companion of Mathlib's cotangent expansion. It is independent of Abel integration and probability.
Both reciprocal-square terms belong to each summand of the symmetric series.
At a real argument x away from the integer zeros of sin(πx), the symmetric shifted reciprocal-square series Σ_{n≥1} (1/(x−n)² + 1/(x+n)²) is summable, and (sin(πx)/π)² times its sum plus the central term 1/x² equals one.
Formal statement
Proof (Lean source)
CscSquaredUpperHalfPlane 1 core · 0 supporting This derivative calculation specializes Mathlib's cotangent partial-fraction theorem to order one. ★ csc_squared_integer_series_upperHalfPlane
Squared-cosecant partial fractions above the real axis
This derivative calculation specializes Mathlib's cotangent partial-fraction
theorem to order one. It is separate from continuity of the reciprocal series
at the real boundary. Together with ShiftedReciprocalSquareRegularity, it
provides the real symmetric squared-cosecant identity without a new axiom.
At a complex argument z above the real axis, the integer reciprocal-square series Σ_{m∈ℤ} 1/(z+m)² multiplied by the squared sine factor (sin(πz)/π)² equals one.
Formal statement
Proof (Lean source)
EsseenAnalyticOneSided 1 core · 0 supporting This separates the band-limited comparison with constant 24/π for an integrable real function from the measure-specific CDF and characteristic-function identities. ★ integrable_one_sided_esseen_fourier_bound
Analytic one-sided Esseen inequality
This separates the band-limited comparison with constant 24/π for an integrable real function from the measure-specific CDF and characteristic-function identities.
For an integrable real function H whose downward increments are bounded by a nonnegative constant L times the distance and a positive bandwidth T, the value of H at every point is at most 1/π times the integral over [−T, T] of the magnitude of its Fourier transform, plus the one-sided Esseen smoothing error 24L/(πT).
Formal statement
Proof (Lean source)
EsseenConvolutionDilation 1 core · 0 supporting This elementary integral identity transfers a normalized, translated unit-bandwidth convolution to the original function and bandwidth. ★ spectral_convolution_dilation
Spatial change of variables for spectral comparison
This elementary integral identity transfers a normalized, translated unit-bandwidth convolution to the original function and bandwidth.
For a positive amplitude a and a positive dilation T, if the translated, amplitude-normalized product u ↦ H(x − u/T)/a · K(u) is integrable, then the dilated convolution integrand y ↦ H(x − y)·T·K(Ty) is integrable and its integral is a times the integral of the normalized product.
Formal statement
Proof (Lean source)
EsseenConvolutionTransfer 1 core · 0 supporting This is the Fourier inversion and Fubini step of one-sided Esseen smoothing. ★ bandlimited_convolution_fourier_bound
Fourier bound for a band-limited convolution
This is the Fourier inversion and Fubini step of one-sided Esseen smoothing. The kernel is supplied separately, so the one-sided comparison can be studied without repeating the frequency-domain argument.
For an integrable real function H and a continuous integrable kernel K whose Fourier transform is integrable, vanishes outside (−T, T) for a positive bandwidth T, and has magnitude at most one, the convolution of H with K at x is bounded in absolute value by 1/(2π) times the integral over [−T, T] of the magnitude of the Fourier transform of H.
Formal statement
Proof (Lean source)
EsseenInversion 1 core · 0 supporting This module isolates the analytic CDF smoothing inequality from Gaussian moments and iid sampling. ★ cdf_esseen_inversion_lipschitz
Scalar Esseen inversion inequality
This module isolates the analytic CDF smoothing inequality from Gaussian moments and iid sampling. The reference law has a globally Lipschitz CDF.
When two scalar probability laws μ and ν have finite first moments, the reference law ν assigns every interval at most L times its length, for a nonnegative constant L, and the bandwidth T is positive, their CDF discrepancy at every point is at most 1/π times the integral over [−T, T] of the characteristic-function discrepancy divided by |t|, plus the Esseen smoothing error 24L/(πT).
Formal statement
Proof (Lean source)
EsseenKernelDilation 1 core · 1 supporting The change of variables taking a unit-bandwidth kernel to bandwidth T is isolated here. ★ spectral_kernel_dilation_properties
Dilation of one-sided spectral kernels
The change of variables taking a unit-bandwidth kernel to bandwidth T is isolated here. These lemmas concern arbitrary kernels and do not assume a CDF bound or a normal approximation.
For an integrable continuous kernel K whose Fourier transform vanishes outside (−1, 1) and has magnitude at most one, and a positive dilation T, the dilated kernel y ↦ T·K(Ty) is integrable and continuous, has an integrable Fourier transform that vanishes outside (−T, T), and keeps Fourier magnitude at most one.
Formal statement
Proof (Lean source)
1 supporting declaration (lemmas, instances)
-
spectral_kernel_dilation_fouriertheorem — Dilating a real kernel by a positive bandwidth and multiplying by that bandwidth divides the frequency in its Fourier integral by the bandwidth.hypothesesK :ℝ → ℝT :ℝhT :0 < Tt :ℝProof (Lean source)
theorem spectral_kernel_dilation_fourier (K : ℝ → ℝ) (T : ℝ) (hT : 0 < T) (t : ℝ) : (∫ y : ℝ, exp (((t * y : ℝ) : ℂ) * I) * ((T * K (T * y) : ℝ) : ℂ)) = ∫ u : ℝ, exp ((((t / T) * u : ℝ) : ℂ) * I) * (K u : ℂ) := by /- Rewrite the integrand as T times f(T*y), where f(u) = exp(i*(t/T)*u)*K(u). Apply Measure.integral_comp_mul_left and integral_const_mul; positivity cancels T*|T⁻¹|. This substitution identity is valid even for a nonintegrable K because both Bochner integrals then obey the same change-of-variables theorem. -/ let f : ℝ → ℂ := fun u => exp ((((t / T) * u : ℝ) : ℂ) * I) * (K u : ℂ) have hscale (y : ℝ) : (t / T) * (T * y) = t * y := by field_simp have heq : (fun y : ℝ => exp (((t * y : ℝ) : ℂ) * I) * ((T * K (T * y) : ℝ) : ℂ)) = fun y => (T : ℂ) * f (T * y) := by funext y dsimp only [f] rw [hscale] simp only [Complex.ofReal_mul] ring rw [heq, integral_const_mul, Measure.integral_comp_mul_left] rw [abs_of_pos (inv_pos.mpr hT)] simp only [Complex.real_smul, ← mul_assoc, ← Complex.ofReal_mul, mul_inv_cancel₀ hT.ne', Complex.ofReal_one, one_mul] rfl
EsseenOneSided 1 core · 0 supporting This isolates the upper CDF comparison in the Esseen inversion step with constant 24/π. ★ cdf_esseen_inversion_one_sided
One-sided scalar Esseen comparison
This isolates the upper CDF comparison in the Esseen inversion step with constant 24/π. The lower comparison can be obtained by reflecting both laws; the reference interval-mass condition is preserved by reflection.
When two scalar probability laws μ and ν have finite first moments, the reference law ν assigns every interval at most L times its length, for a nonnegative constant L, and the bandwidth T is positive, the CDF of μ exceeds the CDF of ν at every point by at most 1/π times the integral over [−T, T] of the characteristic-function discrepancy divided by |t|, plus the Esseen smoothing error 24L/(πT).
Formal statement
Proof (Lean source)
EsseenSignedKernelComparison 1 core · 0 supporting The one-sided increment condition is integrated against a positive linearly weighted sinc-fourth density. ★ esseenSignedSinc4Kernel_comparison
Spatial comparison for the signed sinc-fourth kernel
The one-sided increment condition is integrated against a positive linearly weighted sinc-fourth density. The first two exact moments fix the numerical comparison error at seven.
If H has downward increments at most the distance between its arguments and the product of the reflected function H(−y) with the signed sinc-fourth comparison kernel is integrable, then the value of H at zero is at most twice the absolute value of that convolution integral plus seven.
Formal statement
Proof (Lean source)
EsseenSignedKernelFourier 1 core · 0 supporting The frequency support of this weighted kernel comes from differentiation of the compactly supported transform of the unweighted sinc-fourth density. ★ esseenSignedSinc4Kernel_fourier_eq_zero
Fourier properties of the signed sinc-fourth kernel
The frequency support of this weighted kernel comes from differentiation of the compactly supported transform of the unweighted sinc-fourth density.
The Fourier integral of the signed sinc-fourth comparison kernel vanishes at every frequency t with |t| at least one.
Formal statement
Proof (Lean source)
EsseenSignedKernelFourierNorm 1 core · 0 supporting The signed comparison kernel k(y) = −(y/8)·q(−y − 4), where q is the unit sinc-fourth probability density, has Fourier transform bounded by one in absolute value at every real frequency. ★ esseenSignedSinc4Kernel_fourier_norm_le_one
Fourier norm bound for the signed sinc-fourth kernel
The signed comparison kernel k(y) = −(y/8)·q(−y − 4), where q is the unit sinc-fourth probability density, has Fourier transform bounded by one in absolute value at every real frequency. The proof bounds the transform by the L¹ norm of k, uses |y|/8 ≤ (y² + 16)/64, and evaluates the resulting integral from the moments of q (mass one, first moment zero, second moment twelve), which gives an L¹ norm of at most 44/64. The bound is used in the one-sided Esseen comparison of distribution functions.
Main results
esseenSignedSinc4Kernel_fourier_norm_le_one— |∫ exp(i t y) k(y) dy| ≤ 1 for all real t.
The Fourier integral of the signed sinc-fourth comparison kernel has magnitude at most one at every real frequency.
Formal statement
Proof (Lean source)
EsseenSinc4FirstMoment 1 core · 0 supporting The unit-bandwidth sinc-fourth kernel is even. ★ sinc4Kernel_unit_first_moment
First moment of the unit-bandwidth sinc-fourth density
The unit-bandwidth sinc-fourth kernel is even. Its absolute first moment is finite, and its signed first moment vanishes. These facts are used to shift the kernel in the one-sided Esseen comparison.
The first-moment density x·K(x) of the unit-bandwidth sinc-fourth kernel K is integrable, and its integral is zero.
Formal statement
Proof (Lean source)
EsseenSinc4SecondMoment 1 core · 0 supporting The exact second moment of this compact-frequency density controls the spatial error of a signed, shifted kernel used in Esseen's comparison. ★ sinc4Kernel_unit_second_moment
Second moment of the unit-bandwidth sinc-fourth density
The exact second moment of this compact-frequency density controls the spatial error of a signed, shifted kernel used in Esseen's comparison.
The second-moment density x²·K(x) of the unit-bandwidth sinc-fourth kernel K is integrable, and its integral equals twelve.
Formal statement
Proof (Lean source)
EsseenSpectralComparison 1 core · 0 supporting This module isolates the kernel construction in Esseen's one-sided smoothing argument. ★ exists_esseen_one_sided_spectral_comparator
One-sided spectral comparison with constant 24/π
This module isolates the kernel construction in Esseen's one-sided smoothing
argument. The Fourier estimate for a supplied kernel is proved separately in
EsseenConvolutionTransfer.
For an integrable real function H whose downward increments are bounded by a nonnegative constant L times the distance, a positive bandwidth T, any point x, and a positive tolerance ε, there is a continuous integrable kernel K with integrable Fourier transform that vanishes outside (−T, T) and has magnitude at most one, whose convolution with H at x is integrable and satisfies H(x) ≤ 2·|convolution at x| + 24L/(πT) + ε.
Formal statement
Proof (Lean source)
EsseenUnitRawWitness 1 core · 0 supporting This isolates the genuine one-sided approximation step. ★ exists_esseen_unit_raw_spectral_witness
Sharp unit-bandwidth spectral witness
This isolates the genuine one-sided approximation step. Kernel regularity
consequences of spectral support are supplied by EsseenUnitRegularity.
For an integrable real function H whose downward increments are at most the distance between its arguments and any positive tolerance ε, there is a continuous integrable kernel K whose Fourier transform vanishes outside (−1, 1) and has magnitude at most one, such that H(0) is at most twice the absolute value of the integral of H(−y)·K(y) plus 24/π + ε.
Formal statement
Proof (Lean source)
EsseenUnitRegularity 1 core · 1 supporting For an integrable real kernel whose Fourier transform vanishes outside the unit interval and has magnitude at most one, the Fourier transform is integrable (integrable_unit_supported_kernel_fourier) and the product of th ★ integrable_reflected_mul_unit_supported_kernel
Regularity consequences of a unit-bandlimited kernel
For an integrable real kernel whose Fourier transform vanishes outside the
unit interval and has magnitude at most one, the Fourier transform is
integrable (integrable_unit_supported_kernel_fourier) and the product of
the kernel with a reflected factor is integrable
(integrable_reflected_mul_unit_supported_kernel). These are the two
integrability facts used by the one-sided spectral comparison.
For an integrable function H and an integrable continuous kernel K whose Fourier transform vanishes outside (−1, 1) and has magnitude at most one, the product y ↦ H(−y)·K(y) is integrable.
Formal statement
Proof (Lean source)
1 supporting declaration (lemmas, instances)
-
integrable_unit_supported_kernel_fouriertheorem — The Fourier transform of an integrable real kernel is integrable when it vanishes outside the unit interval and has magnitude at most one.hypothesesK :ℝ → ℝhK :conclusionProof (Lean source)
theorem integrable_unit_supported_kernel_fourier (K : ℝ → ℝ) (hK : Integrable K volume) (hsupp : ∀ t : ℝ, 1 ≤ |t| → (∫ y : ℝ, exp (((t * y : ℝ) : ℂ) * I) * (K y : ℂ)) = 0) (hnorm : ∀ t : ℝ, ‖∫ y : ℝ, exp (((t * y : ℝ) : ℂ) * I) * (K y : ℂ)‖ ≤ 1) : Integrable (fun t : ℝ => ∫ y : ℝ, exp (((t * y : ℝ) : ℂ) * I) * (K y : ℂ)) volume := by let f : ℝ → ℂ := fun y => (K y : ℂ) let F : ℝ → ℂ := fun t => ∫ y : ℝ, exp (((t * y : ℝ) : ℂ) * I) * f y have hf : Integrable f := hK.ofReal have hFfourier (w : ℝ) : fourier f w = F ((-2 * pi) * w) := by rw [Real.fourier_eq'] apply integral_congr_ae filter_upwards with y simp only [smul_eq_mul, f, RCLike.inner_apply', starRingEnd_apply, star_trivial] congr 2 push_cast ring have hFcont : Continuous F := by have hc : Continuous (fourier f) := VectorFourier.fourierIntegral_continuous Real.continuous_fourierChar (innerSL ℝ).continuous₂ hf have heq : F = fun t : ℝ => fourier f (t / (-2 * pi)) := by funext t rw [hFfourier] congr 1 field_simp rw [heq] fun_prop have hsupport : support F ⊆ Icc (-1 : ℝ) 1 := by intro t ht by_contra hn have ht' : 1 ≤ |t| := by simp only [Set.mem_Icc, not_and_or, not_le] at hn rcases hn with hn | hn · rw [abs_of_nonpos (by linarith)] linarith · rw [abs_of_nonneg (by linarith)] linarith exact ht (hsupp t ht') have hmajor : Integrable ((Icc (-1 : ℝ) 1).indicator (fun _ : ℝ => (1 : ℝ))) volume := (continuous_const.integrableOn_Icc).integrable_indicator measurableSet_Icc apply Integrable.mono' hmajor hFcont.aestronglyMeasurable filter_upwards with t by_cases ht : t ∈ Icc (-1 : ℝ) 1 · rw [Set.indicator_of_mem ht] exact hnorm t · rw [Set.indicator_of_notMem ht] have hzero : F t = 0 := by by_contra hn exact ht (hsupport hn) simp [hzero]
EsseenUnitSpectralComparison 1 core · 0 supporting This module isolates the sharp analytic kernel construction at bandwidth one, unit downward slope, and the origin. ★ exists_esseen_unit_spectral_comparator
Unit-bandwidth one-sided spectral comparison
This module isolates the sharp analytic kernel construction at bandwidth one, unit downward slope, and the origin. Translation and rescaling belong to the general spectral comparison module.
For an integrable real function H whose downward increments are at most the distance between its arguments and any positive tolerance ε, there is a continuous integrable kernel K with integrable Fourier transform that vanishes outside (−1, 1) and has magnitude at most one, such that y ↦ H(−y)·K(y) is integrable and H(0) is at most twice the absolute value of its integral plus 24/π + ε.
Formal statement
Proof (Lean source)
GaussianSineInversion 1 core · 1 supporting This Gaussian-only identity is independent of Prawitz filters and probability comparison inequalities. ★ gaussian_cdf_sine_inversion
Sine inversion of the standard Gaussian distribution function
This Gaussian-only identity is independent of Prawitz filters and probability comparison inequalities. The frequency integrand has a removable singularity at zero, with its Lebesgue endpoint value assigned by real division.
At every real threshold x, the standard Gaussian probability of the half-line (−∞, x] equals one half plus 1/π times the integral over t > 0 of exp(−t²/2)·sin(tx)/t.
Formal statement
Proof (Lean source)
1 supporting declaration (lemmas, instances)
-
gaussian_sine_quotient_integrabletheorem — At any real threshold, the Gaussian sine quotient is integrable on the positive frequency half-line.hypothesesx :ℝconclusionProof (Lean source)
theorem gaussian_sine_quotient_integrable (x : ℝ) : IntegrableOn (fun t : ℝ => exp (-(t ^ 2 / 2)) * sin (t * x) / t) (Ioi 0) := by have hg : Integrable (fun t : ℝ => exp (-(t ^ 2 / 2))) := by simpa only [div_eq_mul_inv, one_mul, neg_mul, mul_neg, mul_comm] using (integrable_exp_neg_mul_sq (by norm_num : (0 : ℝ) < 1 / 2)) have hm : Measurable (fun t : ℝ => exp (-(t ^ 2 / 2)) * sin (t * x) / t) := by fun_prop apply (hg.integrableOn.const_mul |x|).mono' hm.aestronglyMeasurable filter_upwards [ae_restrict_mem measurableSet_Ioi] with t ht have ht0 : 0 < t := ht have hs : |sin (t * x)| / t ≤ |x| := by apply (div_le_iff₀ ht0).mpr simpa only [abs_mul, abs_of_pos ht0, mul_comm] using (Real.abs_sin_le_abs (x := t * x)) rw [Real.norm_eq_abs, abs_div, abs_mul, abs_of_pos (Real.exp_pos _), abs_of_pos ht0] calc _ = exp (-(t ^ 2 / 2)) * (|sin (t * x)| / t) := by ring _ ≤ exp (-(t ^ 2 / 2)) * |x| := mul_le_mul_of_nonneg_left hs (Real.exp_nonneg _) _ = _ := by ring
GaussianWeightedTail 1 core · 0 supporting This real probability-independent tail estimate integrates the reciprocal and constant weights appearing in a scaled spectral-kernel bound. ★ gaussian_reciprocal_linear_tail_bound
Weighted Gaussian upper tails
This real probability-independent tail estimate integrates the reciprocal and constant weights appearing in a scaled spectral-kernel bound. It isolates the improper-integral calculation from Prawitz's parameter-dependent cutoffs.
For a positive lower endpoint a and damping rate b and a nonnegative constant weight c, the integral over t > a of (1/(πt) + c)·exp(−bt²) is at most (1/(2πba²) + c/(2ba))·exp(−ba²).
Formal statement
Proof (Lean source)
IIDCharFunProduct 1 core · 0 supporting This module isolates the finite-product identity used by the scalar Berry–Esseen argument. ★ iid_sum_charFun_product
Characteristic function of an iid finite sum
This module isolates the finite-product identity used by the scalar Berry–Esseen argument. No moment bound or asymptotic assertion is needed.
Under the n-fold product of a real probability law, the characteristic function of the coordinate sum at frequency t is the n-th power of the one-coordinate characteristic function at t.
Formal statement
Proof (Lean source)
PrawitzAbelLimit 1 core · 0 supporting A nonsingular rational sine kernel converges to cotangent inside the unit interval. ★ prawitz_abel_weighted_integral_tendsto
Abel convergence of the weighted cotangent integral
A nonsingular rational sine kernel converges to cotangent inside the unit interval. Its multiplier relative to cotangent lies between zero and one, which supplies an integrable majorant after multiplication by the sine wave.
For any real spatial frequency x, as the damping ratio r increases to one, the triangularly weighted integrals over [0, 1] of the rational Abel kernel 2r·sin(2πt)/(1 − 2r·cos(2πt) + r²) against sin(2πxt) converge to the weighted integral of the cotangent cot(πt) against sin(2πxt).
Formal statement
Proof (Lean source)
PrawitzAbelSeries 1 core · 0 supporting Inside the open unit disk the geometric sine series is uniformly absolutely convergent. ★ prawitz_abel_weighted_integral_series
Termwise integration of a damped cotangent sine series
Inside the open unit disk the geometric sine series is uniformly absolutely convergent. This leaf handles that exchange separately from the boundary limit and separately from evaluation of its elementary Fourier coefficients.
For a damping ratio r strictly between zero and one and any real frequency x, the damped triangularly weighted sine coefficients r^(n+1)·∫₀¹ (1 − t)·sin(2π(n+1)t)·sin(2πxt) dt are summable, and twice their sum equals the weighted integral of the rational Abel kernel 2r·sin(2πt)/(1 − 2r·cos(2πt) + r²) against sin(2πxt).
Formal statement
Proof (Lean source)
PrawitzBudgetCutoffs 1 core · 0 supporting One independent sufficient estimate in the deterministic Prawitz budget. ★ prawitz_budget_cutoffs
PrawitzBudgetCutoffs
One independent sufficient estimate in the deterministic Prawitz budget. The full budget retains its original cutoffs and constant; the three integral allocations add to one and introduce no probability hypotheses.
For a moment ratio ρ strictly between zero and one, the inner cutoff U0 = max(3/2, √(4 log(1/ρ))) is positive and no larger than the outer cutoff U = 12/(5ρ).
Formal statement
Proof (Lean source)
PrawitzBudgetGaussian 1 core · 0 supporting One independent sufficient estimate in the deterministic Prawitz budget. ★ prawitz_budget_gaussian
PrawitzBudgetGaussian
One independent sufficient estimate in the deterministic Prawitz budget. The full budget retains its original cutoffs and constant; the three integral allocations add to one and introduce no probability hypotheses.
For a moment ratio ρ strictly between zero and one, with cutoffs U0 = max(3/2, √(4 log(1/ρ))) and U = 12/(5ρ) and K the Prawitz filter, the Gaussian principal correction 2·∫ over [0, U0] of |K(t/U)/U − i/(2πt)|·exp(−t²/2), plus the omitted Gaussian tail (1/π)·∫ over t > U0 of exp(−t²/2)/t, is at most three fifths of ρ.
Formal statement
Proof (Lean source)
PrawitzBudgetHigh 1 core · 0 supporting One independent sufficient estimate in the deterministic Prawitz budget. ★ prawitz_budget_high
PrawitzBudgetHigh
One independent sufficient estimate in the deterministic Prawitz budget. The full budget retains its original cutoffs and constant; the three integral allocations add to one and introduce no probability hypotheses.
For a moment ratio ρ strictly between zero and one, with cutoffs U0 = max(3/2, √(4 log(1/ρ))) and U = 12/(5ρ), the high-frequency contribution (2/U)·∫ over [U0, U] of the Prawitz filter magnitude at t/U times the characteristic-function moment envelope is at most three twentieths of ρ.
Formal statement
Proof (Lean source)
PrawitzBudgetHighCompact 1 core · 0 supporting This independent deterministic certificate keeps the cubic damping and the actual kernel above ratio one hundredth. ★ prawitz_budget_high_compact
High-frequency Prawitz allocation on the complementary ratio interval
This independent deterministic certificate keeps the cubic damping and the actual kernel above ratio one hundredth. Combining it with the small-ratio assembly proves the unchanged full high-frequency allocation.
For a moment ratio ρ above one hundredth and below one, with cutoffs U0 = max(3/2, √(4 log(1/ρ))) and U = 12/(5ρ), the high-frequency Prawitz contribution (2/U)·∫ over [U0, U] of the Prawitz filter magnitude at t/U times the moment envelope is at most three twentieths of ρ.
Formal statement
Proof (Lean source)
PrawitzBudgetHighSmall 1 core · 0 supporting This assembly lemma splits at the reciprocal-ratio cutoff and applies the two independently proved weighted Gaussian tails. ★ prawitz_budget_high_small
High-frequency Prawitz allocation at small moment ratios
This assembly lemma splits at the reciprocal-ratio cutoff and applies the two independently proved weighted Gaussian tails. The complementary ratio interval and the unchanged full high-frequency budget are separate modules.
For a positive moment ratio ρ at most one hundredth, with the logarithmic inner cutoff U0 = max(3/2, √(4 log(1/ρ))) and the reciprocal outer cutoff U = 12/(5ρ), the high-frequency Prawitz contribution (2/U)·∫ over [U0, U] of the Prawitz filter magnitude at t/U times the moment envelope is at most three twentieths of ρ.
Formal statement
Proof (Lean source)
PrawitzBudgetLow 1 core · 0 supporting One independent sufficient estimate in the deterministic Prawitz budget. ★ prawitz_budget_low
PrawitzBudgetLow
One independent sufficient estimate in the deterministic Prawitz budget. The full budget retains its original cutoffs and constant; the three integral allocations add to one and introduce no probability hypotheses.
For a moment ratio ρ strictly between zero and one, with cutoffs U0 = max(3/2, √(4 log(1/ρ))) and U = 12/(5ρ), the low-frequency Fourier discrepancy contribution (2/U)·∫ over [0, U0] of the Prawitz filter magnitude at t/U times the discrepancy envelope is at most one quarter of ρ.
Formal statement
Proof (Lean source)
PrawitzBudgetLowCompact 1 core · 3 supporting This independent deterministic certificate retains the actual minimum discrepancy envelope and kernel on ratios above one hundredth. ★ prawitz_budget_low_compact
Low-frequency Prawitz allocation on the complementary ratio interval
This independent deterministic certificate retains the actual minimum discrepancy envelope and kernel on ratios above one hundredth. Together with the small-ratio assembly it proves the unchanged full low-frequency budget.
For a moment ratio ρ above one hundredth and below one, with cutoffs U0 = max(3/2, √(4 log(1/ρ))) and U = 12/(5ρ), the low-frequency Prawitz contribution (2/U)·∫ over [0, U0] of the Prawitz filter magnitude at t/U times the minimum discrepancy envelope is at most one quarter of ρ.
Formal statement
Proof (Lean source)
3 supporting declarations (lemmas, instances)
-
prawitz_low_compact_cell_boundtheorem — On a positive parameter cell and a positive frequency cell inside the original kernel band, the normalized low-frequency integrand is bounded by the better of the Taylor and modulus-sum cell bounds.hypothesesρ r s t a b :ℝhr :0 < rhrρ :r ≤ ρhρs :ρ ≤ sha :0 < ahat :a ≤ thtb :t ≤ bhtU :t ≤ 12 / (5 * ρ)Proof (Lean source)
theorem prawitz_low_compact_cell_bound (ρ r s t a b : ℝ) (hr : 0 < r) (hrρ : r ≤ ρ) (hρs : ρ ≤ s) (ha : 0 < a) (hat : a ≤ t) (htb : t ≤ b) (htU : t ≤ 12 / (5 * ρ)) : (5 / 6 : ℝ) * ‖prawitzKernel (t / (12 / (5 * ρ)))‖ * prawitzDiscrepancyEnvelope ρ t ≤ (1 / (pi * a) + 5 * s / 12) * min ((b ^ 3 / 6 + s * b ^ 4 / 8) * exp (-(a ^ 2 / 4) + s * b ^ 3 / 10)) ((min 1 (exp (-(a ^ 2 / 2) + s * b ^ 3 / 5)) + exp (-(a ^ 2 / 2))) / r) := by have hρ : 0 < ρ := hr.trans_le hrρ have hs : 0 < s := hρ.trans_le hρs have ht : 0 < t := ha.trans_le hat have hb : 0 < b := ht.trans_le htb have hU : 0 < 12 / (5 * ρ) := by positivity have hfreq : 0 < t / (12 / (5 * ρ)) := div_pos ht hU have hfreq1 : t / (12 / (5 * ρ)) ≤ 1 := (div_le_one hU).2 htU have hk := prawitzKernel_norm_le (t / (12 / (5 * ρ))) (by simpa only [abs_of_pos hfreq] using hfreq) (by simpa only [abs_of_pos hfreq] using hfreq1) rw [abs_of_pos hfreq] at hk have hk' : (5 / 6 : ℝ) * ‖prawitzKernel (t / (12 / (5 * ρ)))‖ * ρ ≤ 1 / (pi * a) + 5 * s / 12 := by calc _ ≤ (5 / 6 : ℝ) * (1 / (2 * pi * (t / (12 / (5 * ρ)))) + 1 / 2) * ρ := by gcongr _ = 1 / (pi * t) + 5 * ρ / 12 := by field_simp; norm_num _ ≤ _ := by gcongr let T := (b ^ 3 / 6 + s * b ^ 4 / 8) * exp (-(a ^ 2 / 4) + s * b ^ 3 / 10) let S := (min 1 (exp (-(a ^ 2 / 2) + s * b ^ 3 / 5)) + exp (-(a ^ 2 / 2))) / r have hT : (t ^ 3 / 6 + ρ * t ^ 4 / 8) * exp (-(t ^ 2 / 4) + ρ * t ^ 3 / 10) ≤ T := by dsimp [T] gcongr have hM : prawitzMomentEnvelope ρ t + exp (-(t ^ 2 / 2)) ≤ min 1 (exp (-(a ^ 2 / 2) + s * b ^ 3 / 5)) + exp (-(a ^ 2 / 2)) := by unfold prawitzMomentEnvelope rw [abs_of_pos ht] gcongr have hd : prawitzDiscrepancyEnvelope ρ t / ρ ≤ min T S := by apply le_min · apply (div_le_iff₀ hρ).2 calc _ ≤ (ρ * t ^ 3 / 6 + ρ ^ 2 * t ^ 4 / 8) * exp (-(t ^ 2 / 4) + ρ * t ^ 3 / 10) := by unfold prawitzDiscrepancyEnvelope rw [abs_of_pos ht] exact min_le_left _ _ _ = ((t ^ 3 / 6 + ρ * t ^ 4 / 8) * exp (-(t ^ 2 / 4) + ρ * t ^ 3 / 10)) * ρ := by ring _ ≤ T * ρ := mul_le_mul_of_nonneg_right hT hρ.le · calc _ ≤ (prawitzMomentEnvelope ρ t + exp (-(t ^ 2 / 2))) / ρ := div_le_div_of_nonneg_right (min_le_right _ _) hρ.le _ ≤ S := by dsimp [S]; gcongr have hd0 : 0 ≤ prawitzDiscrepancyEnvelope ρ t / ρ := by unfold prawitzDiscrepancyEnvelope prawitzMomentEnvelope positivity calc _ = ((5 / 6 : ℝ) * ‖prawitzKernel (t / (12 / (5 * ρ)))‖ * ρ) * (prawitzDiscrepancyEnvelope ρ t / ρ) := by field_simp _ ≤ (1 / (pi * a) + 5 * s / 12) * min T S := mul_le_mul hk' hd hd0 (by positivity) -
prawitz_low_compact_initial_integral_boundtheorem — On an initial frequency interval inside the kernel band and a positive parameter cell with nonpositive Taylor exponent, the normalized integral has a polynomial bound at its singular endpoint.hypothesesρ s a :ℝhρ :0 < ρhρs :ρ ≤ sha :0 ≤ ahaU :a ≤ 12 / (5 * ρ)hsa :s * a ≤ 5 / 2conclusion(5 / 6 : ℝ) * (∫ t in (0 : ℝ)..a, ‖prawitzKernel (t / (12 / (5 * ρ)))‖ * prawitzDiscrepancyEnvelope ρ t)≤ (1 / pi + 5 * s * a / 12) * (1 / 6 + s * a / 8) * a ^ 3 / 3Proof (Lean source)
theorem prawitz_low_compact_initial_integral_bound (ρ s a : ℝ) (hρ : 0 < ρ) (hρs : ρ ≤ s) (ha : 0 ≤ a) (haU : a ≤ 12 / (5 * ρ)) (hsa : s * a ≤ 5 / 2) : (5 / 6 : ℝ) * (∫ t in (0 : ℝ)..a, ‖prawitzKernel (t / (12 / (5 * ρ)))‖ * prawitzDiscrepancyEnvelope ρ t) ≤ (1 / pi + 5 * s * a / 12) * (1 / 6 + s * a / 8) * a ^ 3 / 3 := by have hs : 0 ≤ s := hρ.le.trans hρs have hU : 0 < 12 / (5 * ρ) := by positivity let C : ℝ := (1 / pi + 5 * s * a / 12) * (1 / 6 + s * a / 8) have hi := prawitz_low_compact_intervalIntegrable ρ (12 / (5 * ρ)) a hρ.le hU ha haU have hpoly : IntervalIntegrable (fun t : ℝ => C * t ^ 2) volume 0 a := (by fun_prop : Continuous (fun t : ℝ => C * t ^ 2)).intervalIntegrable 0 a rw [← intervalIntegral.integral_const_mul] calc _ ≤ ∫ t in (0 : ℝ)..a, C * t ^ 2 := by apply intervalIntegral.integral_mono_on_of_le_Ioo ha (hi.const_mul _) hpoly intro t ht have ht0 : 0 < t := ht.1 have hta : t ≤ a := ht.2.le have htU : t ≤ 12 / (5 * ρ) := hta.trans haU have hf : 0 < t / (12 / (5 * ρ)) := div_pos ht0 hU have hf1 : t / (12 / (5 * ρ)) ≤ 1 := (div_le_one hU).2 htU have hk := prawitzKernel_norm_le (t / (12 / (5 * ρ))) (by simpa only [abs_of_pos hf] using hf) (by simpa only [abs_of_pos hf] using hf1) rw [abs_of_pos hf] at hk have hρt : ρ * t ≤ 5 / 2 := (mul_le_mul hρs hta ht0.le hs).trans hsa have he : exp (-(t ^ 2 / 4) + ρ * t ^ 3 / 10) ≤ 1 := by apply Real.exp_le_one_iff.mpr have hp := mul_nonneg (sq_nonneg t) (sub_nonneg.mpr hρt) nlinarith have hd0 : 0 ≤ prawitzDiscrepancyEnvelope ρ t := by unfold prawitzDiscrepancyEnvelope prawitzMomentEnvelope positivity have hd : prawitzDiscrepancyEnvelope ρ t ≤ ρ * t ^ 3 / 6 + ρ ^ 2 * t ^ 4 / 8 := by calc _ ≤ (ρ * t ^ 3 / 6 + ρ ^ 2 * t ^ 4 / 8) * exp (-(t ^ 2 / 4) + ρ * t ^ 3 / 10) := by simpa only [prawitzDiscrepancyEnvelope, abs_of_pos ht0] using min_le_left ((ρ * |t| ^ 3 / 6 + ρ ^ 2 * t ^ 4 / 8) * exp (-(t ^ 2 / 4) + ρ * |t| ^ 3 / 10)) (prawitzMomentEnvelope ρ t + exp (-(t ^ 2 / 2))) _ ≤ _ := mul_le_of_le_one_right (by positivity) he calc _ ≤ (5 / 6 : ℝ) * (1 / (2 * pi * (t / (12 / (5 * ρ)))) + 1 / 2) * (ρ * t ^ 3 / 6 + ρ ^ 2 * t ^ 4 / 8) := by simpa only [mul_assoc] using mul_le_mul (mul_le_mul_of_nonneg_left hk (by norm_num : (0 : ℝ) ≤ 5 / 6)) hd hd0 (by positivity) _ = (1 / pi + 5 * ρ * t / 12) * (1 / 6 + ρ * t / 8) * t ^ 2 := by field_simp ring _ ≤ C * t ^ 2 := by dsimp [C]; gcongr _ = _ := by rw [intervalIntegral.integral_const_mul, integral_pow] dsimp [C] norm_num ring -
prawitz_low_compact_cell_integral_boundtheorem — On positive parameter and frequency cells inside the kernel band, the normalized cell integral is bounded using the better envelope branch.hypothesesρ r s a b :ℝhr :0 < rhrρ :r ≤ ρhρs :ρ ≤ sha :0 < ahab :a ≤ bhbU :b ≤ 12 / (5 * ρ)Proof (Lean source)
theorem prawitz_low_compact_cell_integral_bound (ρ r s a b : ℝ) (hr : 0 < r) (hrρ : r ≤ ρ) (hρs : ρ ≤ s) (ha : 0 < a) (hab : a ≤ b) (hbU : b ≤ 12 / (5 * ρ)) : (5 / 6 : ℝ) * (∫ t in a..b, ‖prawitzKernel (t / (12 / (5 * ρ)))‖ * prawitzDiscrepancyEnvelope ρ t) ≤ (b - a) * (1 / (pi * a) + 5 * s / 12) * min ((b ^ 3 / 6 + s * b ^ 4 / 8) * exp (-(a ^ 2 / 4) + s * b ^ 3 / 10)) ((min 1 (exp (-(a ^ 2 / 2) + s * b ^ 3 / 5)) + exp (-(a ^ 2 / 2))) / r) := by have hρ : 0 < ρ := hr.trans_le hrρ have hU : 0 < 12 / (5 * ρ) := by positivity have hib := prawitz_low_compact_intervalIntegrable ρ (12 / (5 * ρ)) b hρ.le hU (ha.le.trans hab) hbU have hia := prawitz_low_compact_intervalIntegrable ρ (12 / (5 * ρ)) a hρ.le hU ha.le (hab.trans hbU) have hi := hia.symm.trans hib rw [← intervalIntegral.integral_const_mul] calc _ ≤ ∫ _t in a..b, (1 / (pi * a) + 5 * s / 12) * min ((b ^ 3 / 6 + s * b ^ 4 / 8) * exp (-(a ^ 2 / 4) + s * b ^ 3 / 10)) ((min 1 (exp (-(a ^ 2 / 2) + s * b ^ 3 / 5)) + exp (-(a ^ 2 / 2))) / r) := by apply intervalIntegral.integral_mono_on hab (hi.const_mul _) intervalIntegrable_const intro t ht simpa only [mul_assoc] using prawitz_low_compact_cell_bound ρ r s t a b hr hrρ hρs ha ht.1 ht.2 (ht.2.trans hbU) _ = _ := by rw [intervalIntegral.integral_const]; ring
PrawitzBudgetLowSmall 1 core · 0 supporting This assembly lemma connects the spectral kernel and discrepancy envelope to the independently proved polynomial Gaussian moment bound. ★ prawitz_budget_low_small
Low-frequency Prawitz allocation at small moment ratios
This assembly lemma connects the spectral kernel and discrepancy envelope to the independently proved polynomial Gaussian moment bound. The complementary ratio interval is handled separately; the full budget retains all ratios.
For a positive moment ratio ρ at most one hundredth, with the logarithmic inner cutoff U0 = max(3/2, √(4 log(1/ρ))) and the reciprocal outer cutoff U = 12/(5ρ), the low-frequency Prawitz contribution (2/U)·∫ over [0, U0] of the Prawitz filter magnitude at t/U times the discrepancy envelope is at most one quarter of ρ.
Formal statement
Proof (Lean source)
PrawitzCompactCellIntegrals 1 core · 2 supporting These cell inequalities retain the cubic exponent's endpoint maximum and the quartic/reflected kernel bounds. ★ prawitz_high_compact_upper_cell_integral_bound
Endpoint integral enclosures for compact Prawitz certificates
These cell inequalities retain the cubic exponent's endpoint maximum and the quartic/reflected kernel bounds. Their imports are proved, including integrability at zero and at the assigned upper endpoint. They do not assert either compact allocation. Subsequent certificates must choose explicit parameter and frequency partitions and certify finite sums of these bounds.
On a positive parameter cell r ≤ ρ ≤ s and a positive frequency cell a ≤ b inside the outer band b ≤ 12/(5ρ) whose rescaled lower endpoint α = 5ra/12 is at least one half, the integral over [a, b] of the Prawitz filter magnitude at t/(12/(5ρ)) times the moment envelope is at most (b − a)·√Q·min(1, exp E), where Q = (1 − α)²/4 + π²(1 − α)⁴/16 is a reflected quartic bound on the filter and E is the larger endpoint value of −t²/2 + s·t³/5, so the bound decays at the outer endpoint.
Formal statement
Proof (Lean source)
2 supporting declarations (lemmas, instances)
-
prawitz_low_compact_endpoint_cell_integral_boundtheorem — On positive parameter and frequency cells inside the original kernel band, the normalized low-frequency integral is enclosed by the better branch using the sharp endpoint cubic exponent.hypothesesρ r s a b :ℝhr :0 < rhrρ :r ≤ ρhρs :ρ ≤ sha :0 < ahab :a ≤ bhbU :b ≤ 12 / (5 * ρ)conclusionE :max (-(a ^ 2 / 2) + s * a ^ 3 / 5) (-(b ^ 2 / 2) + s * b ^ 3 / 5)Proof (Lean source)
theorem prawitz_low_compact_endpoint_cell_integral_bound (ρ r s a b : ℝ) (hr : 0 < r) (hrρ : r ≤ ρ) (hρs : ρ ≤ s) (ha : 0 < a) (hab : a ≤ b) (hbU : b ≤ 12 / (5 * ρ)) : let E := max (-(a ^ 2 / 2) + s * a ^ 3 / 5) (-(b ^ 2 / 2) + s * b ^ 3 / 5) (5 / 6 : ℝ) * (∫ t in a..b, ‖prawitzKernel (t / (12 / (5 * ρ)))‖ * prawitzDiscrepancyEnvelope ρ t) ≤ (b - a) * (1 / (pi * a) + 5 * s / 12) * min ((b ^ 3 / 6 + s * b ^ 4 / 8) * exp (E / 2)) ((min 1 (exp E) + exp (-(a ^ 2 / 2))) / r) := by /- Reproduce the normalized algebra of the proved, older low cell bound, but use prawitz_envelope_cell_bounds instead of independent exponent endpoints. The two polynomial factors are monotone on positive cells. Bound the discrepancy divided by rho by each branch; combine with the triangle kernel estimate. Integrate using extracted low integrability. This leaf imports neither compact budget and changes neither headline. It is a cell enclosure, not the still-missing total <=3/10 certificate. -/ dsimp only let E := max (-(a ^ 2 / 2) + s * a ^ 3 / 5) (-(b ^ 2 / 2) + s * b ^ 3 / 5) have hρ : 0 < ρ := hr.trans_le hrρ have hU : 0 < 12 / (5 * ρ) := by positivity have hib := prawitz_low_compact_intervalIntegrable ρ (12 / (5 * ρ)) b hρ.le hU (ha.le.trans hab) hbU have hia := prawitz_low_compact_intervalIntegrable ρ (12 / (5 * ρ)) a hρ.le hU ha.le (hab.trans hbU) have hi := hia.symm.trans hib rw [← intervalIntegral.integral_const_mul] calc _ ≤ ∫ _t in a..b, (1 / (pi * a) + 5 * s / 12) * min ((b ^ 3 / 6 + s * b ^ 4 / 8) * exp (E / 2)) ((min 1 (exp E) + exp (-(a ^ 2 / 2))) / r) := by apply intervalIntegral.integral_mono_on hab (hi.const_mul _) intervalIntegrable_const intro t htcell have hat := htcell.1 have htb := htcell.2 have htU := htb.trans hbU change (5 / 6 : ℝ) * (_ * _) ≤ _ rw [← mul_assoc] have hρ : 0 < ρ := hr.trans_le hrρ have hs : 0 < s := hρ.trans_le hρs have ht : 0 < t := ha.trans_le hat have hb : 0 < b := ht.trans_le htb have hU : 0 < 12 / (5 * ρ) := by positivity have hfreq : 0 < t / (12 / (5 * ρ)) := div_pos ht hU have hfreq1 : t / (12 / (5 * ρ)) ≤ 1 := (div_le_one hU).2 htU have hk := prawitzKernel_norm_le (t / (12 / (5 * ρ))) (by simpa only [abs_of_pos hfreq] using hfreq) (by simpa only [abs_of_pos hfreq] using hfreq1) rw [abs_of_pos hfreq] at hk have hk' : (5 / 6 : ℝ) * ‖prawitzKernel (t / (12 / (5 * ρ)))‖ * ρ ≤ 1 / (pi * a) + 5 * s / 12 := by calc _ ≤ (5 / 6 : ℝ) * (1 / (2 * pi * (t / (12 / (5 * ρ)))) + 1 / 2) * ρ := by gcongr _ = 1 / (pi * t) + 5 * ρ / 12 := by field_simp; norm_num _ ≤ _ := by gcongr have he := prawitz_envelope_cell_bounds ρ s t a b hρ.le hρs ha.le hat htb let T := (b ^ 3 / 6 + s * b ^ 4 / 8) * exp (E / 2) let S := (min 1 (exp E) + exp (-(a ^ 2 / 2))) / r have hT : (t ^ 3 / 6 + ρ * t ^ 4 / 8) * exp (-(t ^ 2 / 4) + ρ * t ^ 3 / 10) ≤ T := by dsimp [T] exact mul_le_mul (by gcongr) (by simpa only [abs_of_pos ht] using he.2) (by positivity) (by positivity) have hM : prawitzMomentEnvelope ρ t + exp (-(t ^ 2 / 2)) ≤ min 1 (exp E) + exp (-(a ^ 2 / 2)) := by exact add_le_add he.1 (Real.exp_le_exp.mpr (by have hsq := pow_le_pow_left₀ ha.le hat 2 linarith)) have hd : prawitzDiscrepancyEnvelope ρ t / ρ ≤ min T S := by apply le_min · apply (div_le_iff₀ hρ).2 calc _ ≤ (ρ * t ^ 3 / 6 + ρ ^ 2 * t ^ 4 / 8) * exp (-(t ^ 2 / 4) + ρ * t ^ 3 / 10) := by unfold prawitzDiscrepancyEnvelope rw [abs_of_pos ht] exact min_le_left _ _ _ = ((t ^ 3 / 6 + ρ * t ^ 4 / 8) * exp (-(t ^ 2 / 4) + ρ * t ^ 3 / 10)) * ρ := by ring _ ≤ T * ρ := mul_le_mul_of_nonneg_right hT hρ.le · calc _ ≤ (prawitzMomentEnvelope ρ t + exp (-(t ^ 2 / 2))) / ρ := div_le_div_of_nonneg_right (min_le_right _ _) hρ.le _ ≤ S := by dsimp [S]; gcongr have hd0 : 0 ≤ prawitzDiscrepancyEnvelope ρ t / ρ := by unfold prawitzDiscrepancyEnvelope prawitzMomentEnvelope positivity calc _ = ((5 / 6 : ℝ) * ‖prawitzKernel (t / (12 / (5 * ρ)))‖ * ρ) * (prawitzDiscrepancyEnvelope ρ t / ρ) := by field_simp _ ≤ (1 / (pi * a) + 5 * s / 12) * min T S := mul_le_mul hk' hd hd0 (by positivity) _ = _ := by rw [intervalIntegral.integral_const]; ring -
prawitz_high_compact_lower_cell_integral_boundtheorem — On positive parameter and frequency cells inside the lower half of every kernel band, the high-frequency cell integral is bounded by the quartic kernel enclosure times the cubic moment envelope.hypothesesρ r s a b :ℝhr :0 < rhrρ :r ≤ ρhρs :ρ ≤ sha :0 < ahab :a ≤ bhbU :b ≤ 12 / (5 * ρ)hhalf :5 * s * b / 12 ≤ 1 / 2conclusionα :5 * r * a / 12β :5 * s * b / 12Q :E :max (-(a ^ 2 / 2) + s * a ^ 3 / 5) (-(b ^ 2 / 2) + s * b ^ 3 / 5)(∫ t in a..b, ‖prawitzKernel (t / (12 / (5 * ρ)))‖ * prawitzMomentEnvelope ρ t)Proof (Lean source)
theorem prawitz_high_compact_lower_cell_integral_bound (ρ r s a b : ℝ) (hr : 0 < r) (hrρ : r ≤ ρ) (hρs : ρ ≤ s) (ha : 0 < a) (hab : a ≤ b) (hbU : b ≤ 12 / (5 * ρ)) (hhalf : 5 * s * b / 12 ≤ 1 / 2) : let α := 5 * r * a / 12 let β := 5 * s * b / 12 let Q := (1 - α) ^ 2 / 4 + (((1 - α) * (1 - (pi * α) ^ 2 / 2 + (pi * β) ^ 4 / 24) / (pi * α * (1 - (pi * β) ^ 2 / 6)) + 1 / pi) / 2) ^ 2 let E := max (-(a ^ 2 / 2) + s * a ^ 3 / 5) (-(b ^ 2 / 2) + s * b ^ 3 / 5) (∫ t in a..b, ‖prawitzKernel (t / (12 / (5 * ρ)))‖ * prawitzMomentEnvelope ρ t) ≤ (b - a) * sqrt Q * min 1 (exp E) := by /- For t in [a,b], t/U=5*rho*t/12 lies in [alpha,beta]. Apply the proved lower-cell Taylor squared norm bound, then Real.le_sqrt_of_sq_le. Apply prawitz_envelope_cell_bounds and integrate the constant majorant using prawitz_high_compact_intervalIntegrable. The resulting finite integral sums still require certified arithmetic; no allocation is assumed by this lemma. -/ dsimp only let α := 5 * r * a / 12 let β := 5 * s * b / 12 let Q := (1 - α) ^ 2 / 4 + (((1 - α) * (1 - (pi * α) ^ 2 / 2 + (pi * β) ^ 4 / 24) / (pi * α * (1 - (pi * β) ^ 2 / 6)) + 1 / pi) / 2) ^ 2 let E := max (-(a ^ 2 / 2) + s * a ^ 3 / 5) (-(b ^ 2 / 2) + s * b ^ 3 / 5) have hρ : 0 < ρ := hr.trans_le hrρ have hs : 0 < s := hρ.trans_le hρs have hU : 0 < 12 / (5 * ρ) := by positivity have hi := prawitz_high_compact_intervalIntegrable ρ (12 / (5 * ρ)) a b hU ha hab hbU calc _ ≤ ∫ _t in a..b, sqrt Q * min 1 (exp E) := by apply intervalIntegral.integral_mono_on hab hi intervalIntegrable_const intro t ht have ht0 : 0 < t := ha.trans_le ht.1 have heq : t / (12 / (5 * ρ)) = 5 * ρ * t / 12 := by field_simp have hα : α ≤ t / (12 / (5 * ρ)) := by rw [heq] dsimp [α] gcongr exact ht.1 have hβ : t / (12 / (5 * ρ)) ≤ β := by rw [heq] dsimp [β] gcongr exact ht.2 have hk : ‖prawitzKernel (t / (12 / (5 * ρ)))‖ ≤ sqrt Q := Real.le_sqrt_of_sq_le (prawitzKernel_lower_cell_taylor_sq_bound _ α β (by dsimp [α]; positivity) hα hβ hhalf) have he := (prawitz_envelope_cell_bounds ρ s t a b hρ.le hρs ha.le ht.1 ht.2).1 exact mul_le_mul hk he (by unfold prawitzMomentEnvelope; positivity) (Real.sqrt_nonneg _) _ = _ := by rw [intervalIntegral.integral_const]; ring
PrawitzCompactEnvelopeCells 1 core · 2 supporting These deterministic helpers split the complementary Prawitz certificates into parameter geometry, endpoint exponent bounds, and later finite-sum arithmetic. ★ prawitz_envelope_cell_bounds
Cutoff geometry and cubic envelope enclosures on parameter cells
These deterministic helpers split the complementary Prawitz certificates into parameter geometry, endpoint exponent bounds, and later finite-sum arithmetic. They assert no budget or Gaussian approximation as a hypothesis. For rational negative exponent endpoints, reuse Real.sum_le_exp_of_nonneg followed by Real.exp_neg to obtain rational reciprocal-polynomial upper bounds. For the logarithmic cutoff, certify endpoint exponentials and use Real.log_le_iff_le_exp. Mathlib's sum_integral_adjacent_intervals provides partition integration; it must be combined with the existing low/high interval-integrability results.
For a frequency t in a nonnegative cell [a, b] and a nonnegative ratio ρ at most s, with E the larger of the endpoint exponents −a²/2 + s·a³/5 and −b²/2 + s·b³/5, the moment envelope at ratio ρ and frequency t is at most min(1, exp E), and the Taylor exponential exp(−t²/4 + ρ|t|³/10) is at most exp(E/2).
Formal statement
Proof (Lean source)
2 supporting declarations (lemmas, instances)
-
prawitz_compact_cutoff_cell_boundstheorem — On a positive parameter cell, the inner logarithmic cutoff lies between the cutoffs at the cell endpoints, and the outer cutoff lies between the reciprocal endpoints.hypothesesρ r s :ℝhr :0 < rhrρ :r ≤ ρhρs :ρ ≤ sProof (Lean source)
theorem prawitz_compact_cutoff_cell_bounds (ρ r s : ℝ) (hr : 0 < r) (hrρ : r ≤ ρ) (hρs : ρ ≤ s) : max (3 / 2 : ℝ) (sqrt (4 * log (1 / s))) ≤ max (3 / 2 : ℝ) (sqrt (4 * log (1 / ρ))) ∧ max (3 / 2 : ℝ) (sqrt (4 * log (1 / ρ))) ≤ max (3 / 2 : ℝ) (sqrt (4 * log (1 / r))) ∧ 12 / (5 * s) ≤ 12 / (5 * ρ) ∧ 12 / (5 * ρ) ≤ 12 / (5 * r) := by have hρ : 0 < ρ := hr.trans_le hrρ have hs : 0 < s := hρ.trans_le hρs have hleft : 1 / s ≤ 1 / ρ := div_le_div_of_nonneg_left (by norm_num) hρ hρs have hright : 1 / ρ ≤ 1 / r := div_le_div_of_nonneg_left (by norm_num) hr hrρ have hl : log (1 / s) ≤ log (1 / ρ) := Real.log_le_log (by positivity) hleft have hu : log (1 / ρ) ≤ log (1 / r) := Real.log_le_log (by positivity) hright refine ⟨?_, ?_, ?_, ?_⟩ · gcongr · gcongr · gcongr · gcongr -
prawitz_cubic_exponent_cell_boundtheorem — Throughout a nonnegative frequency cell and a nonnegative parameter cell, the cubic Gaussian exponent is bounded by its two endpoint values at the upper parameter.hypothesesρ s t a b :ℝhρ :0 ≤ ρhρs :ρ ≤ sha :0 ≤ ahat :a ≤ thtb :t ≤ bconclusion-(t ^ 2 / 2) + ρ * t ^ 3 / 5≤ max (-(a ^ 2 / 2) + s * a ^ 3 / 5) (-(b ^ 2 / 2) + s * b ^ 3 / 5)Proof (Lean source)
theorem prawitz_cubic_exponent_cell_bound (ρ s t a b : ℝ) (hρ : 0 ≤ ρ) (hρs : ρ ≤ s) (ha : 0 ≤ a) (hat : a ≤ t) (htb : t ≤ b) : -(t ^ 2 / 2) + ρ * t ^ 3 / 5 ≤ max (-(a ^ 2 / 2) + s * a ^ 3 / 5) (-(b ^ 2 / 2) + s * b ^ 3 / 5) := by /- Smallest open exponent obligation; do not dispatch a compact budget. First replace ρ by s using t≥0. At s=0 the exponent is decreasing. At s>0 its derivative is t*(-1+3*s*t/5), so the exponent decreases up to 5/(3*s) and increases afterwards. Split according to which side contains t, and compare to a or b on the corresponding interval using monotoneOn/antitoneOn_of_deriv_nonneg/nonpos. The critical point is a minimum, so endpoint maxima enclose every cell including cells crossing it. This preserves the cubic damping; -a²/2+s*b³/5 is an unnecessarily loose independent-term bound. The Taylor discrepancy exponent is exactly half this exponent and can use the same enclosure. Certify later endpoint exponentials with Mathlib's finite Taylor bounds, never floating-point scans. The eventual normalized totals remain ≤1/4 and ≤3/20 for low/high contributions (equivalently raw integrals ≤3/10 and ≤9/50); this lemma supplies no such total as an assumption. -/ have hs : 0 ≤ s := hρ.trans hρs have ht : 0 ≤ t := ha.trans hat have hparam : -(t ^ 2 / 2) + ρ * t ^ 3 / 5 ≤ -(t ^ 2 / 2) + s * t ^ 3 / 5 := by gcongr have hd (x : ℝ) : deriv (fun x : ℝ => -(x ^ 2 / 2) + s * x ^ 3 / 5) x = x * (-1 + 3 * s * x / 5) := by simp (disch := fun_prop) ring -- The sign test includes s = 0, when the decreasing branch always applies. by_cases hturn : 3 * s * t ≤ 5 · have hm : AntitoneOn (fun x : ℝ => -(x ^ 2 / 2) + s * x ^ 3 / 5) (Icc a t) := by apply antitoneOn_of_deriv_nonpos (convex_Icc a t) (by fun_prop) (by fun_prop) intro x hx have hxcell : x ∈ Icc a t := interior_subset hx have hx : 0 ≤ x := ha.trans hxcell.1 have hxt : 3 * s * x ≤ 3 * s * t := mul_le_mul_of_nonneg_left hxcell.2 (by positivity) rw [hd] exact mul_nonpos_of_nonneg_of_nonpos hx (by linarith) exact hparam.trans ((hm ⟨le_rfl, hat⟩ ⟨hat, le_rfl⟩ hat).trans (le_max_left _ _)) · have hm : MonotoneOn (fun x : ℝ => -(x ^ 2 / 2) + s * x ^ 3 / 5) (Icc t b) := by apply monotoneOn_of_deriv_nonneg (convex_Icc t b) (by fun_prop) (by fun_prop) intro x hx have hxcell : x ∈ Icc t b := interior_subset hx have hx : 0 ≤ x := ht.trans hxcell.1 have htx : 3 * s * t ≤ 3 * s * x := mul_le_mul_of_nonneg_left hxcell.1 (by positivity) rw [hd] exact mul_nonneg hx (by linarith) exact hparam.trans ((hm ⟨le_rfl, htb⟩ ⟨htb, le_rfl⟩ htb).trans (le_max_right _ _))
PrawitzCompactIntegrability 1 core · 1 supporting The low-frequency discrepancy cancels the singularity of the filter at zero. ★ prawitz_high_compact_intervalIntegrable
Integrability for deterministic Prawitz compact certificates
The low-frequency discrepancy cancels the singularity of the filter at zero. The high-frequency moment factor is integrable on every positive subinterval of the kernel band. These unchanged proofs are extracted from the compact budget files so cell certificates have no admitted import dependency.
On a positive frequency interval [a, b] inside the kernel band of positive width U, the product of the Prawitz filter magnitude at t/U and the cubic moment envelope is interval integrable on [a, b] for any ratio ρ. The statement covers the assigned value of the filter at the upper endpoint.
Formal statement
Proof (Lean source)
1 supporting declaration (lemmas, instances)
-
prawitz_low_compact_intervalIntegrabletheorem — For a nonnegative ratio and an interval contained in a positive kernel band, the low-frequency discrepancy integrand is interval integrable, including at zero.hypothesesρ U a :ℝhρ :0 ≤ ρhU :0 < Uha :0 ≤ ahaU :a ≤ UconclusionIntervalIntegrable (fun t : ℝ => ‖prawitzKernel (t / U)‖ * prawitzDiscrepancyEnvelope ρ t) volume 0 aProof (Lean source)
theorem prawitz_low_compact_intervalIntegrable (ρ U a : ℝ) (hρ : 0 ≤ ρ) (hU : 0 < U) (ha : 0 ≤ a) (haU : a ≤ U) : IntervalIntegrable (fun t : ℝ => ‖prawitzKernel (t / U)‖ * prawitzDiscrepancyEnvelope ρ t) volume 0 a := by let G : ℝ → ℝ := fun t => (U / (2 * pi) * (ρ * t ^ 2 / 6 + ρ ^ 2 * t ^ 3 / 8) + (ρ * t ^ 3 / 6 + ρ ^ 2 * t ^ 4 / 8) / 2) * exp (-(t ^ 2 / 4) + ρ * t ^ 3 / 10) have hG : Continuous G := by dsimp [G]; fun_prop have hK : Measurable prawitzKernel := by unfold prawitzKernel sign apply Measurable.ite · exact (measurableSet_eq_fun measurable_id measurable_const).union (measurableSet_lt measurable_const continuous_abs.measurable) · exact measurable_const · apply add · exact Complex.measurable_ofReal.comp (by fun_prop) · apply mul _ measurable_const apply Complex.measurable_ofReal.comp apply Measurable.div_const apply add · fun_prop · apply Measurable.div_const apply Measurable.ite (measurableSet_lt measurable_id measurable_const) measurable_const exact Measurable.ite (measurableSet_lt measurable_const measurable_id) measurable_const measurable_const have hD : Continuous (prawitzDiscrepancyEnvelope ρ) := by unfold prawitzDiscrepancyEnvelope prawitzMomentEnvelope fun_prop have hm : Measurable (fun t : ℝ => ‖prawitzKernel (t / U)‖ * prawitzDiscrepancyEnvelope ρ t) := ((hK.comp (measurable_id.div_const U)).norm).mul hD.measurable apply (hG.intervalIntegrable 0 a).mono_fun' hm.aestronglyMeasurable rw [Set.uIoc_of_le ha] filter_upwards [ae_restrict_mem measurableSet_Ioc] with t ht have ht0 : 0 < t := ht.1 have htU : t ≤ U := ht.2.trans haU have hs : 0 < t / U := div_pos ht0 hU have hs1 : t / U ≤ 1 := (div_le_one hU).2 htU have hk := prawitzKernel_norm_le (t / U) (by simpa only [abs_of_pos hs] using hs) (by simpa only [abs_of_pos hs] using hs1) rw [abs_of_pos hs] at hk have hd0 : 0 ≤ prawitzDiscrepancyEnvelope ρ t := by unfold prawitzDiscrepancyEnvelope prawitzMomentEnvelope positivity have hd : prawitzDiscrepancyEnvelope ρ t ≤ (ρ * t ^ 3 / 6 + ρ ^ 2 * t ^ 4 / 8) * exp (-(t ^ 2 / 4) + ρ * t ^ 3 / 10) := by simpa only [prawitzDiscrepancyEnvelope, abs_of_pos ht0] using (min_le_left ((ρ * |t| ^ 3 / 6 + ρ ^ 2 * t ^ 4 / 8) * exp (-(t ^ 2 / 4) + ρ * |t| ^ 3 / 10)) (prawitzMomentEnvelope ρ t + exp (-(t ^ 2 / 2)))) rw [Real.norm_eq_abs, abs_of_nonneg (mul_nonneg (norm_nonneg _) hd0)] calc _ ≤ (1 / (2 * pi * (t / U)) + 1 / 2) * ((ρ * t ^ 3 / 6 + ρ ^ 2 * t ^ 4 / 8) * exp (-(t ^ 2 / 4) + ρ * t ^ 3 / 10)) := mul_le_mul hk hd hd0 (by positivity) _ = G t := by dsimp [G] field_simp
PrawitzCompactKernelCells 1 core · 2 supporting These deterministic bounds remove cotangent from frequency-cell certificates. ★ prawitzKernel_lower_cell_taylor_sq_bound
Polynomial cell enclosures for the Prawitz filter
These deterministic bounds remove cotangent from frequency-cell certificates. The reflected upper-band and Jordan lower-band estimates are extracted from PrawitzBudgetHighCompact without changing their statements or proofs. The quartic lower-band cell enclosure is the remaining analytic leaf; it uses only the endpoints of a cell, and retains the full positive half-band.
On a frequency u in a positive cell [a, b] of the lower half-band b ≤ 1/2, the squared Prawitz filter norm at u is at most (1 − a)²/4 + (((1 − a)·(1 − (πa)²/2 + (πb)⁴/24)/(πa·(1 − (πb)²/6)) + 1/π)/2)², a bound that involves only the cell endpoints and π.
Formal statement
Proof (Lean source)
2 supporting declarations (lemmas, instances)
-
prawitz_high_compact_kernel_sq_uppertheorem — On the upper half of the open kernel band, reflection about π gives a polynomial bound for the squared filter norm. The assigned endpoint value is excluded.hypothesess :ℝhs :1 / 2 ≤ shs1 :s < 1conclusion‖prawitzKernel s‖ ^ 2 ≤ (1 - s) ^ 2 / 4 + pi ^ 2 * (1 - s) ^ 4 / 16Proof (Lean source)
theorem prawitz_high_compact_kernel_sq_upper (s : ℝ) (hs : 1 / 2 ≤ s) (hs1 : s < 1) : ‖prawitzKernel s‖ ^ 2 ≤ (1 - s) ^ 2 / 4 + pi ^ 2 * (1 - s) ^ 4 / 16 := by have hs0 : 0 < s := by linarith let y := pi * (1 - s) have hy : 0 < y := by dsimp [y]; positivity have hyhalf : y ≤ pi / 2 := by dsimp [y]; nlinarith [Real.pi_pos] have hypi : y < pi := by linarith [Real.pi_pos] have hsin : 0 < sin y := Real.sin_pos_of_mem_Ioo ⟨hy, hypi⟩ have hcos : 0 ≤ cos y := Real.cos_nonneg_of_mem_Icc ⟨by linarith [Real.pi_pos], hyhalf⟩ have hmul : y * cos y ≤ sin y := by rcases hyhalf.eq_or_lt with he | hlt · rw [he, Real.cos_pi_div_two, Real.sin_pi_div_two] norm_num · have hcpos : 0 < cos y := Real.cos_pos_of_mem_Ioo ⟨by linarith [Real.pi_pos], hlt⟩ have htan := Real.le_tan hy.le hlt rw [Real.tan_eq_sin_div_cos] at htan exact (le_div_iff₀ hcpos).mp htan have hcot : 1 / y - y / 2 ≤ cos y / sin y := by have hr : cos y / y ≤ cos y / sin y := div_le_div_of_nonneg_left hcos hsin (Real.sin_le hy.le) apply le_trans _ hr apply (le_div_iff₀ hy).mpr have ht := Real.one_sub_sq_div_two_le_cos (x := y) field_simp nlinarith let q := (1 / pi - (1 - s) * cos y / sin y) / 2 have hq0 : 0 ≤ q := by dsimp [q] apply div_nonneg _ (by norm_num) apply sub_nonneg.mpr apply (div_le_iff₀ hsin).mpr have hp : 0 < pi := Real.pi_pos rw [one_div_mul_eq_div] apply (le_div_iff₀ hp).mpr dsimp [y] at hmul nlinarith have hqupper : q ≤ pi * (1 - s) ^ 2 / 4 := by have h := mul_le_mul_of_nonneg_left hcot (show 0 ≤ 1 - s by linarith) have he : (1 - s) * (1 / y - y / 2) = 1 / pi - pi * (1 - s) ^ 2 / 2 := by dsimp [y] field_simp [sub_ne_zero.mpr hs1.ne', Real.pi_ne_zero] rw [he] at h dsimp [q] simp only [← mul_div_assoc] at h nlinarith have hne : ¬(s = 0 ∨ 1 < |s|) := by simp only [abs_of_pos hs0, not_or, not_lt] exact ⟨hs0.ne', hs1.le⟩ have hre : (prawitzKernel s).re = (1 - s) / 2 := by rw [prawitzKernel, if_neg hne] simp only [abs_of_pos hs0, Complex.add_re, Complex.mul_re, Complex.ofReal_re, Complex.ofReal_im, Complex.I_re, Complex.I_im] ring have him : (prawitzKernel s).im = q := by rw [prawitzKernel, if_neg hne] dsimp [q, y] rw [mul_sub, mul_one, Real.cos_pi_sub, Real.sin_pi_sub] simp only [abs_of_pos hs0, Real.sign_of_pos hs0, Complex.ofReal_im, Complex.mul_im, Complex.ofReal_re, Complex.I_im, Complex.I_re] ring have hsq := pow_le_pow_left₀ hq0 hqupper 2 rw [Complex.sq_norm, Complex.normSq_apply, hre, him] nlinarith -
prawitz_high_compact_kernel_sq_lowertheorem — On the positive lower half of the kernel band, Jordan's inequality and reflection about π/2 give a squared filter bound without a trigonometric denominator.hypothesess :ℝhs :0 < shsHalf :s ≤ 1 / 2Proof (Lean source)
theorem prawitz_high_compact_kernel_sq_lower (s : ℝ) (hs : 0 < s) (hsHalf : s ≤ 1 / 2) : ‖prawitzKernel s‖ ^ 2 ≤ (1 - s) ^ 2 / 4 + (((1 - s) * pi * (1 / 2 - s) / (2 * s) + 1 / pi) / 2) ^ 2 := by have hp : 0 < pi * s := mul_pos Real.pi_pos hs have hhalf : pi * s ≤ pi / 2 := by nlinarith [Real.pi_pos] have hsin : 0 < sin (pi * s) := Real.sin_pos_of_mem_Ioo ⟨hp, by nlinarith [Real.pi_pos]⟩ have hcos : 0 ≤ cos (pi * s) := Real.cos_nonneg_of_mem_Icc ⟨by linarith [Real.pi_pos], hhalf⟩ have hsinLower : 2 * s ≤ sin (pi * s) := by have h := Real.mul_le_sin hp.le hhalf convert h using 1 field_simp have hcosUpper : cos (pi * s) ≤ pi * (1 / 2 - s) := by have h := Real.sin_le (show 0 ≤ pi / 2 - pi * s by linarith) rw [Real.sin_pi_div_two_sub] at h nlinarith have hcot : cos (pi * s) / sin (pi * s) ≤ pi * (1 / 2 - s) / (2 * s) := by calc _ ≤ cos (pi * s) / (2 * s) := div_le_div_of_nonneg_left hcos (by positivity) hsinLower _ ≤ _ := div_le_div_of_nonneg_right hcosUpper (by positivity) let q := ((1 - s) * cos (pi * s) / sin (pi * s) + 1 / pi) / 2 have hq0 : 0 ≤ q := by have h1s : 0 ≤ 1 - s := by linarith dsimp [q] positivity have hqUpper : q ≤ ((1 - s) * pi * (1 / 2 - s) / (2 * s) + 1 / pi) / 2 := by have h := mul_le_mul_of_nonneg_left hcot (show 0 ≤ 1 - s by linarith) simp only [← mul_div_assoc] at h rw [← mul_assoc] at h dsimp [q] nlinarith have hne : ¬(s = 0 ∨ 1 < |s|) := by simp only [abs_of_pos hs, not_or, not_lt] exact ⟨hs.ne', by linarith⟩ have hre : (prawitzKernel s).re = (1 - s) / 2 := by rw [prawitzKernel, if_neg hne] simp only [abs_of_pos hs, Complex.add_re, Complex.mul_re, Complex.ofReal_re, Complex.ofReal_im, Complex.I_re, Complex.I_im] ring have him : (prawitzKernel s).im = q := by rw [prawitzKernel, if_neg hne] simp only [abs_of_pos hs, Real.sign_of_pos hs, Complex.add_im, Complex.ofReal_im, Complex.mul_im, Complex.ofReal_re, Complex.I_im, Complex.I_re] dsimp [q] ring have hsq := pow_le_pow_left₀ hq0 hqUpper 2 rw [Complex.sq_norm, Complex.normSq_apply, hre, him] nlinarith
PrawitzCompactRealCutoffs 1 core · 1 supporting The finite rational cutoff certificate is already proved. ★ prawitz_compact_real_cutoff_enclosures
Real cutoff adapters for the certified compact parameter grid
The finite rational cutoff certificate is already proved. This module bridges its Taylor inequalities to the original logarithmic cutoffs over entire real parameter cells. It also locates every compact ratio in the explicit grid. Neither integral budget is imported or assumed.
Throughout the j-th certified parameter cell, for every ratio ρ between the cell's left and right endpoints, with B the cell's low grid endpoint (its low cutoff index over 200), A its high grid endpoint (its high cutoff index over 1000), inner cutoff U0 = max(3/2, √(4 log(1/ρ))) and outer cutoff U = 12/(5ρ), the inner cutoff U0 is at most B, B is at most the outer cutoff U, and the rescaled high endpoint U·A is at most U0.
Formal statement
Proof (Lean source)
1 supporting declaration (lemmas, instances)
-
prawitz_compact_parameter_cell_existstheorem — Every real ratio in the closed compact range belongs to one of the 270 adjacent rational parameter cells.hypothesesρ :ℝhρ0 :1 / 100 ≤ ρhρ1 :ρ ≤ 1conclusion∃ j : Fin 270,conclusion 1(prawitzCompactLeft j.val : ℝ) ≤ ρconclusion 2ρ ≤ (prawitzCompactRight j.val : ℝ)Proof (Lean source)
theorem prawitz_compact_parameter_cell_exists (ρ : ℝ) (hρ0 : 1 / 100 ≤ ρ) (hρ1 : ρ ≤ 1) : ∃ j : Fin 270, (prawitzCompactLeft j.val : ℝ) ≤ ρ ∧ ρ ≤ (prawitzCompactRight j.val : ℝ) := by by_cases heq : ρ = 1 · refine ⟨269, ?_, ?_⟩ <;> norm_num [heq, prawitzCompactLeft, prawitzCompactRight] · have hlast : (prawitzCompactLeft 270 : ℝ) = 1 := by norm_num [prawitzCompactLeft] have hfirst : (prawitzCompactLeft 0 : ℝ) = 1 / 100 := by norm_num [prawitzCompactLeft] have hmem : ρ ∈ Ico (prawitzCompactLeft 0 : ℝ) (prawitzCompactLeft 270 : ℝ) := by rw [hfirst, hlast] exact ⟨hρ0, lt_of_le_of_ne hρ1 heq⟩ have hcover := Ico_subset_biUnion_Ico 270 (fun i => (prawitzCompactLeft i : ℝ)) hmem rcases Set.mem_iUnion.mp hcover with ⟨i, hi⟩ rcases Set.mem_iUnion.mp hi with ⟨hi, hcell⟩ exact ⟨⟨i, Finset.mem_range.mp hi⟩, hcell.1, hcell.2.le⟩
PrawitzCutoffRationalCertificate 1 core · 0 supporting This is a finite arithmetic obligation, independent of either integral budget. ★ prawitz_compact_cutoff_rational_certificate
Finite rational certificates for the moving Prawitz cutoffs
This is a finite arithmetic obligation, independent of either integral budget. The low table certifies exp(B²/4) ≥ 1/r using a lower Taylor polynomial. The high table certifies C ≤ 3/2 or exp(C²/4) ≤ 1/s using the proved eighth-power exponential enclosure. Thus B bounds the actual inner cutoff from above, and the rescaled high index bounds it from below on the WHOLE parameter cell [r,s]. No sampled log/sqrt value is a premise.
At every cell j of the explicit 270-cell compact parameter grid, with r and s the cell's left and right endpoints, B its low cutoff index over 200, A its high cutoff index over 1000 and C = 12A/(5r), the endpoints satisfy 0 < r < s ≤ 1, the low cutoff index lies between 300 and 859 and the high cutoff index between 1 and 999, B is at most 12/(5s), the low certificate 1 ≤ r·T(B²/4) holds, and either C ≤ 3/2 or both 0 ≤ C²/4 ≤ 8 and s·E(C²/4) ≤ 1. Here T is the sixteen-term Taylor polynomial of the exponential and E the rational eighth-power upper enclosure of the exponential.
Formal statement
Proof (Lean source)
PrawitzFarGaussianTail 1 core · 0 supporting This bounded real integral handles the far part of the high-frequency budget using the coarse global damping bound. ★ prawitz_far_gaussian_tail_budget
Far-frequency Gaussian allocation for small Prawitz ratios
This bounded real integral handles the far part of the high-frequency budget using the coarse global damping bound. The reciprocal weight is nonsingular throughout this interval. The full high-frequency budget remains a separate theorem over all ratios strictly between zero and one.
For a positive ratio ρ at most one hundredth, the integral from the reciprocal-ratio cutoff 1/(2ρ) to the fixed outer cutoff 12/(5ρ) of (1/(πt) + 5ρ/12)·exp(−t²/50) is at most one twentieth of ρ.
Formal statement
Proof (Lean source)
PrawitzHighRealEnclosures 1 core · 1 supporting The lower-half Taylor kernel and upper-half reflected polynomial use the actual real pi here. ★ prawitz_high_real_exponential_enclosure
Analytic adapters for the rational high-frequency cells
The lower-half Taylor kernel and upper-half reflected polynomial use the actual real pi here. The first adapter compares their squared enclosures with the rational pi interval; the second compares the rescaled cubic exponential with the reciprocal Taylor entry. These are pointwise scalar inequalities, not integral allocations. They import no open budget or real cutoff adapter. At the outer kernel endpoint the later integral comparison must still be made only almost everywhere, as in PrawitzRescaledCells.
On the j-th certified compact parameter cell and the i-th positive high-frequency grid cell [i/1000, (i+1)/1000], for i from 1 to 999, with s the parameter cell's right endpoint and E the larger of the values of (−72x²/25 + 1728x³/625)/s² at the two grid endpoints x = i/1000 and x = (i+1)/1000, the exponential of E is at most 1/T(−E), where T is the sixteen-term Taylor polynomial of the exponential and −E is the matching rational exponent from the high table.
Formal statement
Proof (Lean source)
1 supporting declaration (lemmas, instances)
-
prawitz_high_real_kernel_square_enclosuretheorem — On every positive high grid cell, the squared analytic kernel enclosure with real pi is bounded by the rational pi enclosure used by the kernel magnitude certificate.hypothesesi :ℕhi :i ∈ Ico 1 1000Proof (Lean source)
theorem prawitz_high_real_kernel_square_enclosure (i : ℕ) (hi : i ∈ Ico 1 1000) : let a := (i : ℝ) / 1000 let b := ((i + 1 : ℕ) : ℝ) / 1000 let Q := if i < 500 then (1 - a) ^ 2 / 4 + (((1 - a) * (1 - (pi * a) ^ 2 / 2 + (pi * b) ^ 4 / 24) / (pi * a * (1 - (pi * b) ^ 2 / 6)) + 1 / pi) / 2) ^ 2 else (1 - a) ^ 2 / 4 + pi ^ 2 * (1 - a) ^ 4 / 16 Q ≤ (prawitzRationalKernelSq i : ℝ) := by /- Round 8 lowest analytic kernel layer. Let p=314159/100000 and q=314160/100000; use the CLOSED rational pi bounds. If i<500, 0<a<=b<=1/2. Compare 1-(pi*a)²/2+(pi*b)^4/24 with 1-(p*a)²/2+(q*b)^4/24, and pi*a*(1-(pi*b)²/6) with p*a*(1-(q*b)²/6)>0. The denominator factor is positive since q<4 and b<=1/2. Establish numerator nonnegativity before division and squaring (the proved cosine quartic estimate at pi*a supplies it, since b>=a and cos(pi*a)>=0). Use 1/pi<=1/p. In the upper branch only pi²<=q² and (1-a)^4>=0 are needed. After push_cast, the result is exactly prawitzRationalKernelSq. This is NOT a bound on the assigned kernel value at u=1, which remains excluded a.e. -/ dsimp only let a : ℝ := i / 1000 let b : ℝ := (i + 1 : ℕ) / 1000 let p : ℝ := 314159 / 100000 let q : ℝ := 314160 / 100000 have hpi := prawitz_rational_pi_bounds have hp : 0 < p := by norm_num [p] have hq : q < 4 := by norm_num [q] have hpaPi : p ≤ pi := hpi.1 have hpiq : pi ≤ q := hpi.2 have ha : 0 < a := by dsimp [a] exact div_pos (by exact_mod_cast (mem_Ico.mp hi).1) (by norm_num) have hab : a ≤ b := by dsimp [a, b]; push_cast; linarith have haOne : 0 ≤ 1 - a := by have h := (mem_Ico.mp hi).2 have h' : (i : ℝ) < 1000 := by exact_mod_cast h dsimp [a] linarith unfold prawitzRationalKernelSq split_ifs with h · have hb : b ≤ 1 / 2 := by have h' : (i : ℝ) + 1 ≤ 500 := by exact_mod_cast (by omega : i + 1 ≤ 500) dsimp [b] push_cast linarith have hpb : 0 ≤ pi * b := mul_nonneg Real.pi_pos.le (ha.le.trans hab) have hqb : 0 ≤ q * b := mul_nonneg (by norm_num [q]) (ha.le.trans hab) have hqbTwo : q * b < 2 := by nlinarith [ha.le.trans hab] have hqbSq : (q * b) ^ 2 < 4 := by nlinarith have hfactor : 0 < 1 - (q * b) ^ 2 / 6 := by apply sub_pos.mpr exact (div_lt_one (by norm_num)).2 (hqbSq.trans (by norm_num)) have hpbqb : pi * b ≤ q * b := mul_le_mul_of_nonneg_right hpiq (ha.le.trans hab) have hsqb := pow_le_pow_left₀ hpb hpbqb 2 have hfourb := pow_le_pow_left₀ hpb hpbqb 4 have hsqa := pow_le_pow_left₀ (mul_nonneg hp.le ha.le) (mul_le_mul_of_nonneg_right hpaPi ha.le) 2 let c := 1 - (pi * a) ^ 2 / 2 + (pi * b) ^ 4 / 24 let C := 1 - (p * a) ^ 2 / 2 + (q * b) ^ 4 / 24 let d := pi * a * (1 - (pi * b) ^ 2 / 6) let D := p * a * (1 - (q * b) ^ 2 / 6) have hc : 0 ≤ c := by have hcos : 0 ≤ cos (pi * a) := Real.cos_nonneg_of_mem_Icc ⟨by nlinarith [Real.pi_pos], by nlinarith [Real.pi_pos]⟩ have ht := cos_le_quadratic_add_quartic (pi * a) have hfour := pow_le_pow_left₀ (mul_nonneg Real.pi_pos.le ha.le) (mul_le_mul_of_nonneg_left hab Real.pi_pos.le) 4 dsimp [c] linarith have hcC : c ≤ C := add_le_add (sub_le_sub_left (div_le_div_of_nonneg_right hsqa (by norm_num)) 1) (div_le_div_of_nonneg_right hfourb (by norm_num)) have hD : 0 < D := mul_pos (mul_pos hp ha) hfactor have hDd : D ≤ d := by exact mul_le_mul (mul_le_mul_of_nonneg_right hpaPi ha.le) (sub_le_sub_left (div_le_div_of_nonneg_right hsqb (by norm_num)) 1) hfactor.le (mul_nonneg Real.pi_pos.le ha.le) have hfrac : (1 - a) * c / d ≤ (1 - a) * C / D := by calc _ ≤ (1 - a) * c / D := div_le_div_of_nonneg_left (mul_nonneg haOne hc) hD hDd _ ≤ _ := div_le_div_of_nonneg_right (mul_le_mul_of_nonneg_left hcC haOne) hD.le have hinv : 1 / pi ≤ 1 / p := one_div_le_one_div_of_le hp hpaPi have hnonneg : 0 ≤ ((1 - a) * c / d + 1 / pi) / 2 := by have hd := hD.trans_le hDd positivity have hsq := pow_le_pow_left₀ hnonneg (show ((1 - a) * c / d + 1 / pi) / 2 ≤ ((1 - a) * C / D + 1 / p) / 2 by linarith) 2 push_cast simpa only [a, b, p, q, c, C, d, D, Nat.cast_add, Nat.cast_one] using add_le_add (le_refl ((1 - a) ^ 2 / 4)) hsq · have hsq := pow_le_pow_left₀ Real.pi_pos.le hpiq 2 have hmul := mul_le_mul_of_nonneg_right hsq (pow_nonneg haOne 4) push_cast change (1 - a) ^ 2 / 4 + pi ^ 2 * (1 - a) ^ 4 / 16 ≤ (1 - a) ^ 2 / 4 + q ^ 2 * (1 - a) ^ 4 / 16 exact add_le_add le_rfl (div_le_div_of_nonneg_right hmul (by norm_num))
PrawitzKernelBounds 1 core · 1 supporting The difference from the singular Fourier transform of a half-line is uniformly bounded. ★ prawitzKernel_norm_le
Bounds on Prawitz's principal spectral correction
The difference from the singular Fourier transform of a half-line is uniformly bounded. Its bound supplies an integrable Gaussian smoothing penalty, with much smaller constants than baseline Esseen smoothing.
At a nonzero frequency t in the unit band |t| ≤ 1, Prawitz's filter magnitude is at most the reciprocal principal frequency term 1/(2π|t|) plus one half.
Formal statement
Proof (Lean source)
1 supporting declaration (lemmas, instances)
-
prawitzKernel_principal_correction_norm_letheorem — At each nonzero frequency in the unit band, Prawitz's spectral filter differs from the half-line principal term by at most one half.hypothesest :ℝht :0 < |t|hband :|t| ≤ 1Proof (Lean source)
theorem prawitzKernel_principal_correction_norm_le (t : ℝ) (ht : 0 < |t|) (hband : |t| ≤ 1) : ‖prawitzKernel t - I / ((2 * pi * t : ℝ) : ℂ)‖ ≤ 1 / 2 := by have hpos (u : ℝ) (hu : 0 < u) (hub : u ≤ 1) : ‖prawitzKernel u - I / ((2 * pi * u : ℝ) : ℂ)‖ ≤ 1 / 2 := by have hne : ¬(u = 0 ∨ 1 < |u|) := by simp only [abs_of_pos hu, not_or, not_lt] exact ⟨hu.ne', hub⟩ let z := prawitzKernel u - I / ((2 * pi * u : ℝ) : ℂ) have hre : z.re = (1 - u) / 2 := by dsimp only [z] rw [prawitzKernel, if_neg hne] simp only [abs_of_pos hu, Complex.sub_re, Complex.add_re, Complex.mul_re, Complex.ofReal_re, Complex.ofReal_im, Complex.I_re, Complex.I_im, Complex.div_ofReal_re] ring have him : z.im = -((1 - u) * (1 / (pi * u) - cos (pi * u) / sin (pi * u))) / 2 := by dsimp only [z] rw [prawitzKernel, if_neg hne] simp only [abs_of_pos hu, Real.sign_of_pos hu, Complex.sub_im, Complex.add_im, Complex.mul_im, Complex.ofReal_re, Complex.ofReal_im, Complex.I_re, Complex.I_im, Complex.div_ofReal_im] simp only [zero_add, zero_mul, add_zero, mul_one] field_simp ring have hsq := correction_sq_le u hu hub have hnorm : ‖z‖ ^ 2 ≤ (1 / 2 : ℝ) ^ 2 := by rw [Complex.sq_norm, Complex.normSq_apply, hre, him] nlinarith dsimp [z] at hnorm nlinarith [norm_nonneg (prawitzKernel u - I / ((2 * pi * u : ℝ) : ℂ))] rcases lt_or_gt_of_ne (show t ≠ 0 from by simpa using ne_of_gt ht) with hneg | hpositive · have hu : 0 < -t := neg_pos.mpr hneg have heq : prawitzKernel t - I / ((2 * pi * t : ℝ) : ℂ) = star (prawitzKernel (-t) - I / ((2 * pi * (-t) : ℝ) : ℂ)) := by have hne : ¬(t = 0 ∨ 1 < |t|) := not_or.mpr ⟨hneg.ne, not_lt.mpr hband⟩ have hne' : ¬(-t = 0 ∨ 1 < |-t|) := by simpa using hne rw [prawitzKernel, if_neg hne, prawitzKernel, if_neg hne'] apply Complex.ext <;> simp only [Real.sign_of_neg hneg, Real.sign_of_pos hu, abs_neg, Real.sin_neg, Real.cos_neg, mul_neg, Complex.sub_re, Complex.sub_im, Complex.add_re, Complex.add_im, Complex.mul_re, Complex.mul_im, Complex.ofReal_re, Complex.ofReal_im, Complex.I_re, Complex.I_im, Complex.div_ofReal_re, Complex.div_ofReal_im, Complex.star_def, Complex.conj_re, Complex.conj_im] <;> ring rw [heq, norm_star] exact hpos (-t) hu (by simpa [abs_of_neg hneg] using hband) · exact hpos t hpositive (by simpa [abs_of_pos hpositive] using hband)
PrawitzLowGaussianMoments 1 core · 0 supporting This elementary real integral controls a polynomial Gaussian majorant of the low-frequency Prawitz contribution when the moment ratio is at most one hundredth. ★ prawitz_low_gaussian_moment_budget
Gaussian moment allocation for small Prawitz ratios
This elementary real integral controls a polynomial Gaussian majorant of the low-frequency Prawitz contribution when the moment ratio is at most one hundredth. It is a helper case, not a replacement for the full budget. No characteristic-function or smoothing theorem is a premise.
For a positive ratio ρ at most one hundredth, the integral over t > 0 of the polynomial Gaussian low-frequency majorant (ρt²/(6π) + ρ²t³/(8π) + 5ρ²t³/72 + 5ρ³t⁴/96)·exp(−23t²/100) is at most one quarter of ρ.
Formal statement
Proof (Lean source)
PrawitzLowRealEnclosures 1 core · 1 supporting These inequalities compare the proved analytic integral majorants with the unchanged rational table terms. ★ prawitz_low_real_cell_enclosure
Analytic adapters for the rational low-frequency cells
These inequalities compare the proved analytic integral majorants with the unchanged rational table terms. They are independent of the real cutoff adapter, the finite low sum certificate, and both integral budgets. The positive grid cells stay inside the band by the rational cutoff certificate, so their cubic endpoint damping is nonnegative before reciprocal Taylor bounds are used. No numerical integral allocation is a premise.
On the j-th certified parameter cell, with rational endpoints r < s, and the i-th positive low grid cell [a, b] = [i/200, (i+1)/200] below the cell's low cutoff index, the analytic cell majorant (b − a)·(1/(πa) + 5s/12)·min((b³/6 + s·b⁴/8)·exp(E/2), (min(1, exp E) + exp(−a²/2))/r), where E is the larger of the two endpoint exponents −a²/2 + s·a³/5 and −b²/2 + s·b³/5, is at most the cell's rational table entry.
Formal statement
Proof (Lean source)
1 supporting declaration (lemmas, instances)
-
prawitz_low_real_initial_enclosuretheorem — On each certified parameter cell, the analytic polynomial enclosure of the singular initial low interval is bounded by its rational table entry.hypothesesj :Fin 270conclusions :(prawitzCompactRight j.val : ℝ)a :(1 / 200 : ℝ)(1 / pi + 5 * s * a / 12) * (1 / 6 + s * a / 8) * a ^ 3 / 3≤ (prawitzRationalLowInitial j.val : ℝ)Proof (Lean source)
theorem prawitz_low_real_initial_enclosure (j : Fin 270) : let s := (prawitzCompactRight j.val : ℝ) let a := (1 / 200 : ℝ) (1 / pi + 5 * s * a / 12) * (1 / 6 + s * a / 8) * a ^ 3 / 3 ≤ (prawitzRationalLowInitial j.val : ℝ) := by /- Use positive s from the CLOSED cutoff certificate. Replace only 1/pi by 1/(314159/100000), using prawitz_rational_pi_bounds. All other nonnegative factors are identical after push_cast. This corresponds exactly to prawitz_low_compact_initial_integral_bound in PrawitzBudgetLowCompact; no integral proof needs to be copied. -/ dsimp only have hc := prawitz_compact_cutoff_rational_certificate j dsimp only at hc have hs : 0 ≤ (prawitzCompactRight j.val : ℝ) := by exact_mod_cast (hc.1.trans hc.2.1).le have hp := prawitz_rational_pi_bounds unfold prawitzRationalLowInitial push_cast gcongr exact hp.1
PrawitzRescaledCells 1 core · 2 supporting The frequency endpoints in these enclosures are fixed fractions of the actual outer cutoff. ★ prawitz_high_rescaled_upper_cell_integral_bound
High-frequency certificates with cells proportional to the bandwidth
The frequency endpoints in these enclosures are fixed fractions of the actual outer cutoff. This avoids extending a frequency cell beyond that cutoff as the moment ratio varies. On such cells the cubic exponent is a negative polynomial divided by the squared moment ratio. Its upper bound uses only the upper parameter endpoint, while the interval length uses the lower endpoint. These are analytic cell bounds, not numerical budgets.
The file proves three bounds: the moment envelope at a rescaled frequency
is dominated by the two endpoint cubic exponents at the upper parameter
(prawitz_rescaled_moment_cell_bound), and the lower-half and upper-half
cell integrals of the high-frequency integrand are bounded by the cell
length times an explicit polynomial bound on the filter times the endpoint
exponential envelope (prawitz_high_rescaled_lower_cell_integral_bound,
prawitz_high_rescaled_upper_cell_integral_bound). Summing these cell
bounds over a rational grid into the numerical high-frequency budget is
done downstream in PrawitzBudgetHighCompact, not here.
On a positive parameter cell r ≤ ρ ≤ s and an upper-half kernel cell 1/2 ≤ a ≤ b ≤ 1, with outer cutoff U = 12/(5ρ), the integral over the moving frequency cell [Ua, Ub] of the Prawitz filter magnitude at t/U times the moment envelope is at most (12/(5r))·(b − a)·√Q·min(1, exp E), where Q = (1 − a)²/4 + π²(1 − a)⁴/16 is a reflected polynomial bound on the filter and E is the larger of the two rescaled endpoint exponents (−72c²/25 + 1728c³/625)/s² at c = a and c = b; this includes cells ending at the outer cutoff.
Formal statement
Proof (Lean source)
2 supporting declarations (lemmas, instances)
-
prawitz_rescaled_moment_cell_boundtheorem — Within a positive parameter cell and a nonnegative cell of the kernel band, the moment envelope at the rescaled frequency is bounded by the two endpoint cubic exponents at the upper parameter.hypothesesρ s u a b :ℝhρ :0 < ρhρs :ρ ≤ sha :0 ≤ ahau :a ≤ uhub :u ≤ bhb :b ≤ 1conclusionprawitzMomentEnvelope ρ ((12 / (5 * ρ)) * u)Proof (Lean source)
theorem prawitz_rescaled_moment_cell_bound (ρ s u a b : ℝ) (hρ : 0 < ρ) (hρs : ρ ≤ s) (ha : 0 ≤ a) (hau : a ≤ u) (hub : u ≤ b) (hb : b ≤ 1) : prawitzMomentEnvelope ρ ((12 / (5 * ρ)) * u) ≤ min 1 (exp (max ((-72 * a ^ 2 / 25 + 1728 * a ^ 3 / 625) / s ^ 2) ((-72 * b ^ 2 / 25 + 1728 * b ^ 3 / 625) / s ^ 2))) := by have hs : 0 < s := hρ.trans_le hρs have hu : 0 ≤ u := ha.trans hau have hu1 : u ≤ 1 := hub.trans hb let C : ℝ := -72 * u ^ 2 / 25 + 1728 * u ^ 3 / 625 have hC : C ≤ 0 := by have h := mul_nonneg (sq_nonneg u) (sub_nonneg.mpr hu1) dsimp [C] nlinarith [sq_nonneg u] have hsq : ρ ^ 2 ≤ s ^ 2 := pow_le_pow_left₀ hρ.le hρs 2 have hdiv : C / ρ ^ 2 ≤ C / s ^ 2 := by apply (div_le_div_iff₀ (sq_pos_of_pos hρ) (sq_pos_of_pos hs)).mpr have h := mul_nonpos_of_nonpos_of_nonneg hC (sub_nonneg.mpr hsq) nlinarith have he := prawitz_cubic_exponent_cell_bound s s ((12 / (5 * s)) * u) ((12 / (5 * s)) * a) ((12 / (5 * s)) * b) hs.le le_rfl (by positivity) (mul_le_mul_of_nonneg_left hau (by positivity)) (mul_le_mul_of_nonneg_left hub (by positivity)) have heq (z : ℝ) : -(((12 / (5 * s)) * z) ^ 2 / 2) + s * ((12 / (5 * s)) * z) ^ 3 / 5 = (-72 * z ^ 2 / 25 + 1728 * z ^ 3 / 625) / s ^ 2 := by field_simp ring rw [heq u, heq a, heq b] at he unfold prawitzMomentEnvelope apply min_le_min_left 1 apply Real.exp_le_exp.mpr have hfreq : 0 ≤ (12 / (5 * ρ)) * u := by positivity rw [abs_of_nonneg hfreq] have hreal : -(((12 / (5 * ρ)) * u) ^ 2 / 2) + ρ * ((12 / (5 * ρ)) * u) ^ 3 / 5 = C / ρ ^ 2 := by dsimp [C] field_simp ring rw [hreal] exact hdiv.trans he -
prawitz_high_rescaled_lower_cell_integral_boundtheorem — On a positive parameter cell and a positive lower-half kernel cell, the high-frequency integral over the corresponding moving frequency cell has an explicit endpoint enclosure.hypothesesρ r s a b :ℝhr :0 < rhrρ :r ≤ ρhρs :ρ ≤ sha :0 < ahab :a ≤ bhb :b ≤ 1 / 2conclusionU :12 / (5 * ρ)Q :E :max ((-72 * a ^ 2 / 25 + 1728 * a ^ 3 / 625) / s ^ 2) ((-72 * b ^ 2 / 25 + 1728 * b ^ 3 / 625) / s ^ 2)(∫ t in (U * a)..(U * b), ‖prawitzKernel (t / U)‖ * prawitzMomentEnvelope ρ t)Proof (Lean source)
theorem prawitz_high_rescaled_lower_cell_integral_bound (ρ r s a b : ℝ) (hr : 0 < r) (hrρ : r ≤ ρ) (hρs : ρ ≤ s) (ha : 0 < a) (hab : a ≤ b) (hb : b ≤ 1 / 2) : let U := 12 / (5 * ρ) let Q := (1 - a) ^ 2 / 4 + (((1 - a) * (1 - (pi * a) ^ 2 / 2 + (pi * b) ^ 4 / 24) / (pi * a * (1 - (pi * b) ^ 2 / 6)) + 1 / pi) / 2) ^ 2 let E := max ((-72 * a ^ 2 / 25 + 1728 * a ^ 3 / 625) / s ^ 2) ((-72 * b ^ 2 / 25 + 1728 * b ^ 3 / 625) / s ^ 2) (∫ t in (U * a)..(U * b), ‖prawitzKernel (t / U)‖ * prawitzMomentEnvelope ρ t) ≤ (12 / (5 * r)) * (b - a) * sqrt Q * min 1 (exp E) := by /- Apply the proved high interval-integrability helper on [U*a,U*b]. For interior t set u=t/U in [a,b]. The proved Taylor squared norm enclosure uses these FIXED kernel endpoints, independent of rho. Apply prawitz_rescaled_moment_cell_bound and U*(t/U)=t, then integrate the constant bound. Finally U<=12/(5*r) and all factors are nonnegative. No substitution theorem or cutoff/log certificate is needed for this leaf. -/ dsimp only let U := 12 / (5 * ρ) let Q := (1 - a) ^ 2 / 4 + (((1 - a) * (1 - (pi * a) ^ 2 / 2 + (pi * b) ^ 4 / 24) / (pi * a * (1 - (pi * b) ^ 2 / 6)) + 1 / pi) / 2) ^ 2 let E := max ((-72 * a ^ 2 / 25 + 1728 * a ^ 3 / 625) / s ^ 2) ((-72 * b ^ 2 / 25 + 1728 * b ^ 3 / 625) / s ^ 2) have hρ : 0 < ρ := hr.trans_le hrρ have hU : 0 < U := by dsimp [U]; positivity have ha0 : 0 < a := ha have hb1 : b ≤ 1 := by linarith have hcell : U * a ≤ U * b := mul_le_mul_of_nonneg_left hab hU.le have hbU : U * b ≤ U := by simpa using mul_le_mul_of_nonneg_left hb1 hU.le have hi := prawitz_high_compact_intervalIntegrable ρ U (U * a) (U * b) hU (mul_pos hU ha0) hcell hbU have hUr : U ≤ 12 / (5 * r) := by dsimp [U] exact div_le_div_of_nonneg_left (by norm_num) (by positivity) (mul_le_mul_of_nonneg_left hrρ (by norm_num)) calc _ ≤ ∫ _t in (U * a)..(U * b), sqrt Q * min 1 (exp E) := by apply intervalIntegral.integral_mono_on hcell hi intervalIntegrable_const intro t ht have hau : a ≤ t / U := (le_div_iff₀ hU).2 (by simpa [mul_comm] using ht.1) have hub : t / U ≤ b := (div_le_iff₀ hU).2 (by simpa [mul_comm] using ht.2) have hk : ‖prawitzKernel (t / U)‖ ≤ sqrt Q := Real.le_sqrt_of_sq_le (prawitzKernel_lower_cell_taylor_sq_bound _ a b ha hau hub hb) have heq : U * (t / U) = t := by field_simp have he := prawitz_rescaled_moment_cell_bound ρ s (t / U) a b hρ hρs ha0.le hau hub hb1 change prawitzMomentEnvelope ρ (U * (t / U)) ≤ min 1 (exp E) at he rw [heq] at he exact mul_le_mul hk he (by unfold prawitzMomentEnvelope; positivity) (Real.sqrt_nonneg _) _ = U * (b - a) * sqrt Q * min 1 (exp E) := by rw [intervalIntegral.integral_const] ring _ ≤ _ := by apply mul_le_mul_of_nonneg_right _ (by positivity) apply mul_le_mul_of_nonneg_right _ (Real.sqrt_nonneg _) exact mul_le_mul_of_nonneg_right hUr (sub_nonneg.mpr hab)
PrawitzSignComparison 1 core · 2 supporting The cotangent sine approximation has a squared-sinc error majorant. ★ prawitzSignApprox_integrable_and_error
Pointwise half-line comparison for Prawitz smoothing
The cotangent sine approximation has a squared-sinc error majorant. This is a deterministic spatial inequality, not an assumed probability bound. It includes the discontinuity at zero, so later CDF bounds allow atoms.
At every real point y, the sine integrand defining Prawitz's sign approximation is integrable on [0, 1], and the error between the sign of y and Prawitz's sign approximation at y is at most sinc(y/2)².
Formal statement
Proof (Lean source)
2 supporting declarations (lemmas, instances)
-
prawitzSignApprox_zerotheorem — The Prawitz sign approximation is zero at zero.conclusionprawitzSignApprox 0 = 0Proof (Lean source)
theorem prawitzSignApprox_zero : prawitzSignApprox 0 = 0 := by simp [prawitzSignApprox] -
prawitzSignApprox_negtheorem — Reversing the spatial argument reverses the sign of the Prawitz approximation.Proof (Lean source)
theorem prawitzSignApprox_neg (y : ℝ) : prawitzSignApprox (-y) = -prawitzSignApprox y := by simp only [prawitzSignApprox, mul_neg, Real.sin_neg, intervalIntegral.integral_neg]
PrawitzSignIntegrability 1 core · 0 supporting The compact-interval sine integrand has removable endpoint singularities. ★ prawitz_sine_intervalIntegrable
Endpoint regularity of the Prawitz sine integral
The compact-interval sine integrand has removable endpoint singularities. This regularity task is independent of the Beurling partial-fraction identity and the pointwise approximation inequality.
For any real spatial argument y, the Prawitz sine integrand, the cotangent weight at t times sin(ty), is integrable on the unit interval.
Formal statement
Proof (Lean source)
PrawitzSignSeries 1 core · 0 supporting This exact deterministic identity isolates the harmonic-analysis bridge from the endpoint integrability and the elementary reciprocal-tail bounds. ★ prawitzSignApprox_reciprocal_sq_identity
The Prawitz sine integral as a reciprocal-square series
This exact deterministic identity isolates the harmonic-analysis bridge from the endpoint integrability and the elementary reciprocal-tail bounds. It uses radians y=2πx, and includes positive integer x without an exclusion.
For a positive spatial coordinate x, the Prawitz sign approximation error, one minus the approximation at 2πx, equals (sin(πx)/π)² times the reciprocal-square series correction 1/x² + 2·Σ_{n≥0} 1/(x+n+1)² − 2/x.
Formal statement
Proof (Lean source)
PrawitzSineCoefficient 1 core · 0 supporting This exact coefficient evaluation supplies the algebraic part of the Prawitz Abel-series assembly. ★ triangular_sine_product_integral
Triangular sine-product coefficients
This exact coefficient evaluation supplies the algebraic part of the Prawitz Abel-series assembly. The sinc formulation includes coincident frequencies, so the coefficient at an integer spatial coordinate needs no limiting argument.
At any two real frequencies a and b, the triangularly weighted integral over [0, 1] of (1 − t)·sin(2πat)·sin(2πbt) equals one quarter of the difference sinc(π(a − b))² − sinc(π(a + b))².
Formal statement
Proof (Lean source)
PrawitzSmoothing 1 core · 0 supporting This four-term Fourier inequality separates low-frequency approximation, high-frequency damping, the bounded principal correction, and the Gaussian tail. ★ normal_cdf_prawitz_smoothing
Prawitz's Gaussian CDF smoothing inequality
This four-term Fourier inequality separates low-frequency approximation, high-frequency damping, the bounded principal correction, and the Gaussian tail. It is the analytic transfer needed by a constant-one Berry–Esseen proof.
For a scalar probability law with finite first moment, positive cutoffs U0 ≤ U, and any threshold x, the CDF of the law at x differs from the standard Gaussian CDF at x by at most the sum of four Prawitz Fourier terms, (2/U)·∫₀^{U0} |K(t/U)|·|φ_μ(t) − φ_γ(t)| dt + (2/U)·∫_{U0}^{U} |K(t/U)|·|φ_μ(t)| dt + 2·∫₀^{U0} |K(t/U)/U − i/(2πt)|·exp(−t²/2) dt + (1/π)·∫_{U0}^{∞} exp(−t²/2)/t dt. Here K is the Prawitz spectral filter, φ_μ the characteristic function of the law, and φ_γ that of the standard Gaussian. The four terms are the filtered low-frequency characteristic-function discrepancy, the filtered high-frequency characteristic-function modulus, the Gaussian principal correction, and the Gaussian tail beyond U0.
Formal statement
Proof (Lean source)
PrawitzSpatialFourier 1 core · 10 supporting These atomic half-line sandwiches, integrability results, Fubini identities, and CDF reduction are proved independently of Gaussian sine inversion and the signed spectral comparison, which are proved in separate modules. ★ prawitz_cdf_error_of_spectral_bound
Spatial and Fourier ingredients for Prawitz smoothing
These atomic half-line sandwiches, integrability results, Fubini identities, and CDF reduction are proved independently of Gaussian sine inversion and the signed spectral comparison, which are proved in separate modules.
For a probability law μ, a positive bandwidth U, a threshold x, and a reference value q and error R, if the distance between one plus the expected Prawitz sign approximation at U(x − y) and 2q, plus the expected squared sinc of U(x − y)/2, is at most 2R, then the CDF of μ at x is within R of q. This isolates the remaining spectral comparison from the atomic endpoint step.
Formal statement
Proof (Lean source)
10 supporting declarations (lemmas, instances)
-
measurable_prawitzSignApproxtheorem — The Prawitz sign approximation is measurable, including its assigned endpoint values.conclusionProof (Lean source)
@[fun_prop] theorem measurable_prawitzSignApprox : Measurable prawitzSignApprox := by have hm : Measurable (fun p : ℝ × ℝ => prawitzSineWeight p.2 * sin (p.2 * p.1)) := by unfold prawitzSineWeight fun_prop have hi := hm.stronglyMeasurable.integral_prod_right' (ν := volume.restrict (Ioc (0 : ℝ) 1)) unfold prawitzSignApprox simpa only [intervalIntegral.integral_of_le (by norm_num : (0 : ℝ) ≤ 1)] using hi.measurable.const_mul 2 -
prawitzSignApprox_abs_le_twotheorem — At every spatial argument, the sign approximation has absolute value at most two.Proof (Lean source)
theorem prawitzSignApprox_abs_le_two (y : ℝ) : |prawitzSignApprox y| ≤ 2 := by have he := (prawitzSignApprox_integrable_and_error y).2 have hs : sinc (y / 2) ^ 2 ≤ 1 := by have h := Real.abs_sinc_le_one (y / 2) nlinarith [le_abs_self (sinc (y / 2)), neg_abs_le (sinc (y / 2))] have hsign : |sign y| ≤ 1 := by rcases lt_trichotomy y 0 with h | h | h · simp [Real.sign_of_neg h] · simp [h] · simp [Real.sign_of_pos h] have ht := abs_sub_le (prawitzSignApprox y) (sign y) 0 rw [sub_zero, sub_zero, abs_sub_comm (prawitzSignApprox y)] at ht linarith -
prawitz_halfLine_indicator_boundstheorem — At positive bandwidth, the closed-half-line indicator at the threshold and spatial point lies between the two Prawitz majorants, with the endpoint included in the upper bound.hypothesesU :ℝhU :0 < Ux y :ℝconclusionconclusion 1(1 + prawitzSignApprox (U * (x - y)) - sinc (U * (x - y) / 2) ^ 2) / 2conclusion 2≤ (1 + prawitzSignApprox (U * (x - y)) + sinc (U * (x - y) / 2) ^ 2) / 2Proof (Lean source)
theorem prawitz_halfLine_indicator_bounds (U : ℝ) (hU : 0 < U) (x y : ℝ) : (1 + prawitzSignApprox (U * (x - y)) - sinc (U * (x - y) / 2) ^ 2) / 2 ≤ (Iic x).indicator (fun _ : ℝ => (1 : ℝ)) y ∧ (Iic x).indicator (fun _ : ℝ => (1 : ℝ)) y ≤ (1 + prawitzSignApprox (U * (x - y)) + sinc (U * (x - y) / 2) ^ 2) / 2 := by have he := (abs_le.mp (prawitzSignApprox_integrable_and_error (U * (x - y))).2) rcases lt_trichotomy y x with h | h | h · have hz : 0 < U * (x - y) := mul_pos hU (sub_pos.mpr h) rw [Real.sign_of_pos hz] at he simp only [Set.indicator_of_mem (show y ∈ Iic x from h.le)] constructor <;> linarith [he.1, he.2] · subst y simp [prawitzSignApprox_zero] · have hz : U * (x - y) < 0 := mul_neg_of_pos_of_neg hU (sub_neg.mpr h) rw [Real.sign_of_neg hz] at he simp only [Set.indicator_of_notMem (show y ∉ Iic x from not_le.mpr h)] constructor <;> linarith [he.1, he.2] -
prawitz_spatial_integrabletheorem — For any probability law at any bandwidth and threshold, both spatial factors are integrable. No moment or absence-of-atoms hypothesis is needed for this step.hypothesesμ :U x :ℝconclusionconclusion 1Integrable (fun y : ℝ => prawitzSignApprox (U * (x - y))) μconclusion 2Integrable (fun y : ℝ => sinc (U * (x - y) / 2) ^ 2) μProof (Lean source)
theorem prawitz_spatial_integrable (μ : Measure ℝ) [IsProbabilityMeasure μ] (U x : ℝ) : Integrable (fun y : ℝ => prawitzSignApprox (U * (x - y))) μ ∧ Integrable (fun y : ℝ => sinc (U * (x - y) / 2) ^ 2) μ := by constructor · apply Integrable.of_bound (measurable_prawitzSignApprox.comp (by fun_prop)).aestronglyMeasurable 2 filter_upwards with y exact prawitzSignApprox_abs_le_two _ · apply Integrable.of_bound (by fun_prop) 1 filter_upwards with y have h := Real.abs_sinc_le_one (U * (x - y) / 2) rw [Real.norm_eq_abs, abs_of_nonneg (sq_nonneg _)] nlinarith [le_abs_self (sinc (U * (x - y) / 2)), neg_abs_le (sinc (U * (x - y) / 2))] -
prawitz_cdf_spatial_boundstheorem — Integrating the spatial majorants for a probability law, at positive bandwidth and any threshold, gives a CDF sandwich valid even when the law has an atom at the threshold.hypothesesconclusionconclusion 1(1 + (∫ y, prawitzSignApprox (U * (x - y)) ∂μ) - (∫ y, sinc (U * (x - y) / 2) ^ 2 ∂μ)) / 2conclusion 2≤ (1 + (∫ y, prawitzSignApprox (U * (x - y)) ∂μ) + (∫ y, sinc (U * (x - y) / 2) ^ 2 ∂μ)) / 2Proof (Lean source)
theorem prawitz_cdf_spatial_bounds (μ : Measure ℝ) [IsProbabilityMeasure μ] (U : ℝ) (hU : 0 < U) (x : ℝ) : (1 + (∫ y, prawitzSignApprox (U * (x - y)) ∂μ) - (∫ y, sinc (U * (x - y) / 2) ^ 2 ∂μ)) / 2 ≤ (μ (Iic x)).toReal ∧ (μ (Iic x)).toReal ≤ (1 + (∫ y, prawitzSignApprox (U * (x - y)) ∂μ) + (∫ y, sinc (U * (x - y) / 2) ^ 2 ∂μ)) / 2 := by obtain ⟨hA, hB⟩ := prawitz_spatial_integrable μ U x have hc : Integrable (fun _ : ℝ => (1 : ℝ)) μ := integrable_const 1 have hi := hc.indicator (measurableSet_Iic (a := x)) have hlo := integral_mono ((hc.add hA).sub hB |>.div_const 2) hi (fun y => (prawitz_halfLine_indicator_bounds U hU x y).1) have hhi := integral_mono hi ((hc.add hA).add hB |>.div_const 2) (fun y => (prawitz_halfLine_indicator_bounds U hU x y).2) simp only [integral_div, integral_add' hc hA, integral_sub' (hc.add hA) hB, integral_add' (hc.add hA) hB, integral_const, measure_univ, ENNReal.toReal_one, smul_eq_mul, integral_indicator_const (1 : ℝ) measurableSet_Iic, mul_one, Measure.real] at hlo hhi exact ⟨hlo, hhi⟩ -
prawitzSineWeight_abs_letheorem — On the positive unit band, the sine-weight singularity is at most reciprocal-linear.Proof (Lean source)
theorem prawitzSineWeight_abs_le (t : ℝ) (ht : 0 < t) (hband : t ≤ 1) : |prawitzSineWeight t| ≤ 1 / (pi * t) + 1 := by have him : (prawitzKernel t).im = prawitzSineWeight t / 2 := by rw [prawitzKernel, if_neg (show ¬(t = 0 ∨ 1 < |t|) from not_or.mpr ⟨ht.ne', by simpa [abs_of_pos ht] using not_lt.mpr hband⟩)] simp only [Complex.add_im, Complex.mul_im, Complex.ofReal_re, Complex.ofReal_im, Complex.I_re, Complex.I_im, zero_mul, mul_one, zero_add, add_zero, prawitzSineWeight, abs_of_pos ht, Real.sign_of_pos ht] have hn := prawitzKernel_norm_le t (by simpa [abs_of_pos ht]) (by simpa [abs_of_pos ht] using hband) have hi := Complex.abs_im_le_norm (prawitzKernel t) rw [him, abs_div, abs_of_pos (by norm_num : (0 : ℝ) < 2)] at hi rw [abs_of_pos ht] at hn have he : 2 * (1 / (2 * pi * t) + 1 / 2) = 1 / (pi * t) + 1 := by field_simp linarith -
prawitz_sine_abs_letheorem — Multiplying by the sine wave cancels the zero-frequency singularity: on the positive unit band, the integrand at spatial argument is bounded linearly in that argument.hypothesest z :ℝht :0 < thband :t ≤ 1conclusionProof (Lean source)
theorem prawitz_sine_abs_le (t z : ℝ) (ht : 0 < t) (hband : t ≤ 1) : |prawitzSineWeight t * sin (t * z)| ≤ (1 / pi + 1) * |z| := by have hsin : |sin (t * z)| ≤ t * |z| := by simpa [abs_mul, abs_of_pos ht] using (Real.abs_sin_le_abs (x := t * z)) have hcoef : (1 / (pi * t) + 1) * t = 1 / pi + t := by field_simp calc _ = |prawitzSineWeight t| * |sin (t * z)| := abs_mul _ _ _ ≤ (1 / (pi * t) + 1) * (t * |z|) := mul_le_mul (prawitzSineWeight_abs_le t ht hband) hsin (abs_nonneg _) (by positivity) _ = (1 / pi + t) * |z| := by rw [← mul_assoc, hcoef] _ ≤ _ := mul_le_mul_of_nonneg_right (by linarith) (abs_nonneg _) -
prawitz_sine_joint_integrabletheorem — With a finite first moment, the Prawitz sine integrand at any bandwidth and threshold is jointly integrable. This is the cancellation needed for the singular-filter Fubini step.hypothesesconclusionIntegrable (fun p : ℝ × ℝ => prawitzSineWeight p.1 * sin (p.1 * (U * (x - p.2)))) ((volume.restrict (Ioc (0 : ℝ) 1)).prod μ)Proof (Lean source)
theorem prawitz_sine_joint_integrable (μ : Measure ℝ) [IsProbabilityMeasure μ] (hfirst : Integrable (fun y : ℝ => y) μ) (U x : ℝ) : Integrable (fun p : ℝ × ℝ => prawitzSineWeight p.1 * sin (p.1 * (U * (x - p.2)))) ((volume.restrict (Ioc (0 : ℝ) 1)).prod μ) := by have hmajor : Integrable (fun y : ℝ => (1 / pi + 1) * |U * (x - y)|) μ := (((integrable_const x).sub hfirst).const_mul U).norm.const_mul _ have hprod := hmajor.comp_snd (volume.restrict (Ioc (0 : ℝ) 1)) apply hprod.mono' (by unfold prawitzSineWeight; fun_prop) have hmem : ∀ᵐ p : ℝ × ℝ ∂((volume.restrict (Ioc (0 : ℝ) 1)).prod μ), p.1 ∈ Ioc (0 : ℝ) 1 := by apply (Measure.ae_prod_iff_ae_ae (measurableSet_Ioc.preimage measurable_fst)).mpr filter_upwards [ae_restrict_mem measurableSet_Ioc] with t ht exact Filter.Eventually.of_forall (fun _ => ht) filter_upwards [hmem] with p hp exact prawitz_sine_abs_le p.1 (U * (x - p.2)) hp.1 hp.2 -
prawitz_sign_expectation_fubinitheorem — For a probability law with finite first moment, the expected sign approximation at any bandwidth and threshold equals the frequency-first sine integral.hypothesesconclusion(∫ y, prawitzSignApprox (U * (x - y)) ∂μ)= 2 * ∫ t in (0 : ℝ)..1, prawitzSineWeight t * (∫ y, sin (t * (U * (x - y))) ∂μ)Proof (Lean source)
theorem prawitz_sign_expectation_fubini (μ : Measure ℝ) [IsProbabilityMeasure μ] (hfirst : Integrable (fun y : ℝ => y) μ) (U x : ℝ) : (∫ y, prawitzSignApprox (U * (x - y)) ∂μ) = 2 * ∫ t in (0 : ℝ)..1, prawitzSineWeight t * (∫ y, sin (t * (U * (x - y))) ∂μ) := by have hi := prawitz_sine_joint_integrable μ hfirst U x rw [← Set.uIoc_of_le (by norm_num : (0 : ℝ) ≤ 1)] at hi have hswap := intervalIntegral_integral_swap (f := fun t y => prawitzSineWeight t * sin (t * (U * (x - y)))) hi simp only [prawitzSignApprox, integral_const_mul] rw [← hswap] congr 1 apply intervalIntegral.integral_congr intro t _ exact integral_const_mul _ _ -
prawitz_sinc_expectation_fubinitheorem — For any probability law, the expected squared-sinc majorant at any bandwidth and threshold equals the triangular cosine integral.hypothesesμ :U x :ℝProof (Lean source)
theorem prawitz_sinc_expectation_fubini (μ : Measure ℝ) [IsProbabilityMeasure μ] (U x : ℝ) : (∫ y, sinc (U * (x - y) / 2) ^ 2 ∂μ) = 2 * ∫ t in (0 : ℝ)..1, (1 - t) * (∫ y, cos (t * (U * (x - y))) ∂μ) := by have hpoint (y : ℝ) : sinc (U * (x - y) / 2) ^ 2 = 2 * ∫ t in (0 : ℝ)..1, (1 - t) * cos (t * (U * (x - y))) := by have h := triangular_cosine_integral (U * (x - y) / (2 * pi)) have he : 2 * pi * (U * (x - y) / (2 * pi)) = U * (x - y) := by field_simp have he' : pi * (U * (x - y) / (2 * pi)) = U * (x - y) / 2 := by field_simp rw [he, he'] at h simp only [mul_comm (U * (x - y))] at h linarith have hi : Integrable (fun p : ℝ × ℝ => (1 - p.1) * cos (p.1 * (U * (x - p.2)))) ((volume.restrict (Ioc (0 : ℝ) 1)).prod μ) := by apply Integrable.of_bound (by fun_prop) 1 have hmem : ∀ᵐ p : ℝ × ℝ ∂((volume.restrict (Ioc (0 : ℝ) 1)).prod μ), p.1 ∈ Ioc (0 : ℝ) 1 := by apply (Measure.ae_prod_iff_ae_ae (measurableSet_Ioc.preimage measurable_fst)).mpr filter_upwards [ae_restrict_mem measurableSet_Ioc] with t ht exact Filter.Eventually.of_forall (fun _ => ht) filter_upwards [hmem] with p hp rw [Real.norm_eq_abs, abs_mul, abs_of_nonneg (by linarith [hp.2] : 0 ≤ 1 - p.1)] calc _ ≤ (1 - p.1) * 1 := mul_le_mul_of_nonneg_left (Real.abs_cos_le_one _) (by linarith [hp.2]) _ ≤ 1 := by linarith [hp.1] rw [← Set.uIoc_of_le (by norm_num : (0 : ℝ) ≤ 1)] at hi have hswap := intervalIntegral_integral_swap (f := fun t y => (1 - t) * cos (t * (U * (x - y)))) hi simp_rw [hpoint] rw [integral_const_mul, ← hswap] congr 1 apply intervalIntegral.integral_congr intro t _ exact integral_const_mul _ _
PrawitzSpectralComparison 1 core · 0 supporting This module compares the expected spatial sign approximation and squared-sinc majorant directly to the Gaussian sine integral. ★ prawitz_gaussian_sine_spectral_bound
Signed spectral assembly for the Prawitz filter
This module compares the expected spatial sign approximation and squared-sinc majorant directly to the Gaussian sine integral. Gaussian CDF inversion is independent: it is used only in the later smoothing assembly. Integrability of the four comparison terms is proved in the separate imported module.
For a probability law with finite first moment, positive ordered cutoffs U0 ≤ U, and any threshold x, the distance between half the expected Prawitz sign approximation at U(x − y) and the Gaussian sine integral (1/π)·∫₀^∞ exp(−t²/2)·sin(tx)/t dt, plus half the expected squared sinc of U(x − y)/2, is at most the sum of the four Prawitz spectral terms (2/U)·∫₀^{U0} |K(t/U)|·|φ_μ(t) − φ_γ(t)| dt + (2/U)·∫_{U0}^{U} |K(t/U)|·|φ_μ(t)| dt + 2·∫₀^{U0} |K(t/U)/U − i/(2πt)|·exp(−t²/2) dt + (1/π)·∫_{U0}^{∞} exp(−t²/2)/t dt. The expectations are over y drawn from the law. Here K is the Prawitz spectral filter, φ_μ the characteristic function of the law, and φ_γ that of the standard Gaussian.
Formal statement
Proof (Lean source)
PrawitzSpectralIntegrability 1 core · 0 supporting Finite first moment cancels the low-frequency characteristic-function discrepancy. ★ prawitz_four_terms_integrable
Integrability of the four Gaussian Prawitz spectral terms
Finite first moment cancels the low-frequency characteristic-function discrepancy. The principal correction is bounded, and the two remaining terms stay away from zero. These analytic side conditions are separated from Gaussian sine inversion and the final signed spectral comparison.
For a probability law with finite first moment and positive ordered cutoffs U0 ≤ U, each of the four Prawitz spectral integrands is integrable on its frequency region: the filtered characteristic-function discrepancy on [0, U0], the filtered characteristic-function modulus on [U0, U], the Gaussian principal correction on [0, U0], and the Gaussian tail integrand on (U0, ∞).
Formal statement
Proof (Lean source)
ReciprocalSquareTail 1 core · 0 supporting Telescoping reciprocal differences sandwich the summable positive tail. ★ reciprocal_sq_tail_bounds
Elementary bounds on a shifted reciprocal-square tail
Telescoping reciprocal differences sandwich the summable positive tail. This leaf supplies the deterministic error bound after the Prawitz series identity, without any trigonometric or probability dependency.
At a positive shift x, the reciprocal-square tail Σ_{n≥0} 1/(x+n+1)² is summable and lies between 1/(x+1) and 1/x.
Formal statement
Proof (Lean source)
ShiftedReciprocalSquareRegularity 1 core · 0 supporting The integer reciprocal-square series converges locally uniformly away from its integer poles, including at noninteger real arguments. ★ shifted_reciprocal_sq_summableLocallyUniformlyOn
Local uniform convergence of shifted reciprocal squares
The integer reciprocal-square series converges locally uniformly away from its integer poles, including at noninteger real arguments. This is the boundary-continuity prerequisite missing from the upper-half-plane-only cotangent derivative theorem in Mathlib.
The integer shifted reciprocal-square series Σ_{m∈ℤ} 1/(z+m)² converges locally uniformly on the complex plane with the integers removed.
Formal statement
Proof (Lean source)
SincBoxConvolution 1 core · 0 supporting The interval density whose Fourier transform is sinc has a triangular self-convolution. ★ sincBox_self_convolution
Self-convolution of the sinc interval density
The interval density whose Fourier transform is sinc has a triangular self-convolution. This spatial calculation is the next step toward the Fourier transform of squared sinc.
At every real argument t, the self-convolution of the interval density equal to π on (−1/(2π), 1/(2π)], whose Fourier transform is sinc, equals the triangular function π·max(1 − π|t|, 0).
Formal statement
Proof (Lean source)
SincFourthFourier 1 core · 0 supporting The transform of sinc⁴ is the self-convolution of the squared-sinc Fourier triangle, divided by 2π. ★ sincFourth_fourier_triangleConvolution
Fourier transform of fourth-power sinc
The transform of sinc⁴ is the self-convolution of the squared-sinc
Fourier triangle, divided by 2π. This identity is the unscaled analytic
input for the compact-frequency probability kernel.
At every frequency t, the Fourier integral of the fourth power of sinc equals 1/(2π) times the self-convolution at t of the squared-sinc triangle u ↦ π·max(1 − |u|/2, 0). In particular this identity holds at zero and at the support endpoints.
Formal statement
Proof (Lean source)
SincFourthFubini 1 core · 0 supporting The squared-sinc factor and its integrable Fourier triangle give an absolutely integrable double integral. ★ sincSquared_triangle_integral_swap
Fubini step for the fourth-power sinc transform
The squared-sinc factor and its integrable Fourier triangle give an absolutely integrable double integral. Swapping its order is the analytic step in the fourth-power sinc transform, isolated from Fourier normalization.
At any frequency t, the integral over x of the Fourier exponential times squared sinc times the inverse transform of the triangle u ↦ π·max(1 − |u|/2, 0) equals the integral over u of the triangle times the Fourier integral of squared sinc at t − u: the spatial and frequency integrals may be exchanged.
Formal statement
Proof (Lean source)
SincKernelInversion 1 core · 0 supporting This analytic identity is the independent inversion step needed to bound a CDF difference after convolution with the fourth-power sinc kernel. ★ sinc4Kernel_fourier_inversion
Fourier inversion of the compact-frequency sinc kernel
This analytic identity is the independent inversion step needed to bound a
CDF difference after convolution with the fourth-power sinc kernel. It uses
the same positive-frequency Fourier convention as sinc4Kernel_fourier_eq_zero.
At positive bandwidth T, the fourth-power sinc density at every point y equals 1/(2π) times the inverse Fourier integral, over the support interval [−T, T], of its Fourier transform.
Formal statement
Proof (Lean source)
SincSquaredFourier 1 core · 0 supporting The triangle transform of squared sinc is the base analytic calculation for the compact-frequency fourth-power smoothing kernel. ★ sincSquared_fourier_triangle
Fourier transform of squared sinc
The triangle transform of squared sinc is the base analytic calculation for the compact-frequency fourth-power smoothing kernel. The endpoint formula includes the boundary of its Fourier support.
At every real frequency t, the Fourier integral of squared sinc is the triangular function π·max(1 − |t|/2, 0): it equals π(1 − |t|/2) on frequencies of absolute value at most two and zero outside, including at the two support endpoints.
Formal statement
Proof (Lean source)
SincSquaredInversion 1 core · 1 supporting The triangle transform of squared sinc is integrable. ★ sincSquared_fourier_inversion
Inversion of the squared-sinc Fourier triangle
The triangle transform of squared sinc is integrable. Fourier inversion then
recovers squared sinc at every spatial point, with the positive-exponential
transform convention and its 1/(2π) normalization made explicit.
At every real point x, including zero, squared sinc equals 1/(2π) times the inverse Fourier integral of its triangle transform u ↦ π·max(1 − |u|/2, 0).
Formal statement
Proof (Lean source)
1 supporting declaration (lemmas, instances)
-
sincTriangle_integrabletheorem — The real triangular Fourier transform π max (1 - |u|/2) 0 of squared sinc is integrable over the whole line.conclusionProof (Lean source)
theorem sincTriangle_integrable : Integrable (fun u : ℝ => pi * max (1 - |u| / 2) 0) volume := by let f : ℝ → ℝ := fun u => pi * max (1 - |u| / 2) 0 have hf : Continuous f := by dsimp [f] fun_prop have hsupp : support f ⊆ Icc (-2) 2 := by intro u hu simp only [Function.mem_support] at hu constructor · by_contra hn have hle : u < -2 := lt_of_not_ge hn have hz : f u = 0 := by dsimp [f] rw [abs_of_nonpos (by linarith), max_eq_right (by linarith)] ring exact hu hz · by_contra hn have hge : 2 < u := lt_of_not_ge hn have hz : f u = 0 := by dsimp [f] rw [abs_of_nonneg (by linarith), max_eq_right (by linarith)] ring exact hu hz exact (integrableOn_iff_integrable_of_support_subset hsupp).mp hf.integrableOn_Icc
SincSquaredPrereqs 1 core · 1 supporting The squared-sinc transform uses an integrable spatial function and the overlap length of two translated unit intervals. ★ centeredUnitIntervals_overlap
Elementary prerequisites for the squared-sinc Fourier transform
The squared-sinc transform uses an integrable spatial function and the overlap length of two translated unit intervals. Both facts are stated here without Fourier analysis so they can be proved independently.
The two closed intervals of length two centered at zero and at t overlap in a set of Lebesgue length max(2 − |t|, 0), for every real t.
Formal statement
Proof (Lean source)
1 supporting declaration (lemmas, instances)
-
sincSquared_integrabletheorem — The square of the real sinc function has finite integral over the real line.conclusionProof (Lean source)
theorem sincSquared_integrable : Integrable (fun x : ℝ => sinc x ^ 2) volume := by apply (integrable_inv_one_add_sq.const_mul (2 : ℝ)).mono · fun_prop · filter_upwards with x rw [Real.norm_eq_abs, abs_of_nonneg (by positivity : 0 ≤ sinc x ^ 2)] rw [Real.norm_eq_abs, abs_of_nonneg (by positivity : 0 ≤ 2 * (1 + x ^ 2)⁻¹)] rw [inv_eq_one_div, mul_one_div] apply (le_div_iff₀ (by positivity : 0 < 1 + x ^ 2)).2 by_cases hx : |x| ≤ 1 · have ha2 : |x| * |x| ≤ 1 * 1 := mul_self_le_mul_self (abs_nonneg x) hx have hx2 : x ^ 2 ≤ 1 := by simpa [sq_abs, pow_two] using ha2 have hs := Real.abs_sinc_le_one x have hsl := neg_abs_le (sinc x) have hsr := le_abs_self (sinc x) have hs2 : sinc x ^ 2 ≤ 1 := by nlinarith nlinarith [sq_nonneg (sinc x)] · have hxabs : 1 < |x| := lt_of_not_ge hx have hx0 : x ≠ 0 := by intro h subst x norm_num at hxabs rw [Real.sinc_of_ne_zero hx0, div_pow, div_mul_eq_mul_div] apply (div_le_iff₀ (by positivity : 0 < x ^ 2)).2 have habs2 : (1 : ℝ) ^ 2 < |x| ^ 2 := (sq_lt_sq₀ (by positivity) (abs_nonneg x)).2 hxabs have hx2 : 1 < x ^ 2 := by simpa [sq_abs] using habs2 have hs := Real.abs_sin_le_one x have hsl := neg_abs_le (sin x) have hsr := le_abs_self (sin x) have hs2 : sin x ^ 2 ≤ 1 := by nlinarith nlinarith [sq_nonneg (sin x)]
SincTriangleConvolution 1 core · 1 supporting The squared-sinc transform is a compactly supported triangle. ★ sincTriangle_convolution_outside
Real integrals of the squared-sinc Fourier triangle
The squared-sinc transform is a compactly supported triangle. These two real-variable integrals isolate the compact-support and normalization calculations used in the fourth-power smoothing kernel.
The self-convolution of the squared-sinc Fourier triangle u ↦ π·max(1 − |u|/2, 0) vanishes at every frequency t of absolute value at least four, including the endpoints.
Formal statement
Proof (Lean source)
1 supporting declaration (lemmas, instances)
-
sincTriangle_square_integraltheorem — The squared-sinc Fourier triangle has squared integral 4π²/3 over the real line. The triangle is π max (1 - |u|/2) 0.Proof (Lean source)
theorem sincTriangle_square_integral : (∫ u : ℝ, (pi * max (1 - |u| / 2) 0) ^ 2) = 4 * pi ^ 2 / 3 := by /- Split at -2, 0, and 2. Outside [-2,2] the integrand vanishes; on each half it is the square of an affine function. -/ let f : ℝ → ℝ := fun u => (pi * max (1 - |u| / 2) 0) ^ 2 have hcont : Continuous f := by dsimp [f] fun_prop have hzero (u : ℝ) (hu : 2 ≤ |u|) : f u = 0 := by dsimp [f] rw [max_eq_right (by linarith : 1 - |u| / 2 ≤ 0)] ring have hsupp : support f ⊆ Ioc (-2) 2 := by intro u hu simp only [Function.mem_support] at hu constructor · by_contra hn have hle : u ≤ -2 := le_of_not_gt hn exact hu (hzero u (by rw [abs_of_nonpos (by linarith)]; linarith)) · by_contra hn have hge : 2 ≤ u := le_of_lt (lt_of_not_ge hn) exact hu (hzero u (by rw [abs_of_nonneg (by linarith)]; linarith)) have hleft : (∫ u in (-2 : ℝ)..0, f u) = 2 * pi ^ 2 / 3 := by have heq : ∀ u ∈ uIcc (-2 : ℝ) 0, f u = (pi * (1 + u / 2)) ^ 2 := by intro u hu have hle : u ≤ 0 := by simpa using hu.2 have hge : -2 ≤ u := by simpa using hu.1 dsimp [f] rw [abs_of_nonpos hle, max_eq_left (by linarith : 0 ≤ 1 - -u / 2)] ring have hderiv (u : ℝ) : HasDerivAt (fun v : ℝ => pi ^ 2 * (v + 2) ^ 3 / 12) ((pi * (1 + u / 2)) ^ 2) u := by have h := ((hasDerivAt_id u).add_const 2 |>.pow 3 |>.const_mul (pi ^ 2) |>.div_const 12) change HasDerivAt (fun v : ℝ => pi ^ 2 * (v + 2) ^ 3 / 12) (pi ^ 2 * (3 * (u + 2) ^ 2 * 1) / 12) u at h convert h using 1; ring calc _ = ∫ u in (-2 : ℝ)..0, (pi * (1 + u / 2)) ^ 2 := by apply intervalIntegral.integral_congr exact heq _ = (pi ^ 2 * (0 + 2) ^ 3 / 12) - (pi ^ 2 * (-2 + 2) ^ 3 / 12) := by apply intervalIntegral.integral_eq_sub_of_hasDerivAt (f := fun v : ℝ => pi ^ 2 * (v + 2) ^ 3 / 12) (f' := fun v : ℝ => (pi * (1 + v / 2)) ^ 2) · intro u _ exact hderiv u · have hc : Continuous (fun v : ℝ => (pi * (1 + v / 2)) ^ 2) := by fun_prop exact hc.intervalIntegrable _ _ _ = _ := by ring have hright : (∫ u in (0 : ℝ)..2, f u) = 2 * pi ^ 2 / 3 := by have heq : ∀ u ∈ uIcc (0 : ℝ) 2, f u = (pi * (1 - u / 2)) ^ 2 := by intro u hu have hge : 0 ≤ u := by simpa using hu.1 have hle : u ≤ 2 := by simpa using hu.2 dsimp [f] rw [abs_of_nonneg hge, max_eq_left (by linarith : 0 ≤ 1 - u / 2)] have hderiv (u : ℝ) : HasDerivAt (fun v : ℝ => -(pi ^ 2 * (2 - v) ^ 3 / 12)) ((pi * (1 - u / 2)) ^ 2) u := by have h := (((hasDerivAt_const u (2 : ℝ)).sub (hasDerivAt_id u)).pow 3 |>.const_mul (pi ^ 2) |>.div_const 12 |>.neg) change HasDerivAt (fun v : ℝ => -(pi ^ 2 * (2 - v) ^ 3 / 12)) (-(pi ^ 2 * (3 * (2 - u) ^ 2 * (0 - 1)) / 12)) u at h convert h using 1; ring calc _ = ∫ u in (0 : ℝ)..2, (pi * (1 - u / 2)) ^ 2 := by apply intervalIntegral.integral_congr exact heq _ = -(pi ^ 2 * (2 - 2) ^ 3 / 12) - -(pi ^ 2 * (2 - 0) ^ 3 / 12) := by apply intervalIntegral.integral_eq_sub_of_hasDerivAt (f := fun v : ℝ => -(pi ^ 2 * (2 - v) ^ 3 / 12)) (f' := fun v : ℝ => (pi * (1 - v / 2)) ^ 2) · intro u _ exact hderiv u · have hc : Continuous (fun v : ℝ => (pi * (1 - v / 2)) ^ 2) := by fun_prop exact hc.intervalIntegrable _ _ _ = _ := by ring change (∫ u : ℝ, f u) = _ rw [← intervalIntegral.integral_eq_integral_of_support_subset hsupp, ← intervalIntegral.integral_add_adjacent_intervals (hcont.intervalIntegrable (-2) 0) (hcont.intervalIntegrable 0 2), hleft, hright] ring
SmoothedCDFFourier 1 core · 0 supporting This module isolates the Fourier-analytic part of the scalar Esseen smoothing argument. ★ sinc4_smoothed_cdf_fourier_bound
Fourier control of sinc-smoothed distribution functions
This module isolates the Fourier-analytic part of the scalar Esseen smoothing argument. The difference of two finite-first-moment CDFs is integrable; smoothing it by a compact-frequency kernel gives a bound in terms of their characteristic functions.
For two probability laws with finite first moments and a positive bandwidth T, the convolution at every point z of their CDF difference with the fourth-power sinc density is bounded in absolute value by 1/(2π) times the integral over [−T, T] of their characteristic-function discrepancy divided by |t|.
Formal statement
Proof (Lean source)
SmoothedCDFFourierFubini 1 core · 0 supporting This isolates the Fubini and frequency-zero steps in the smoothing bound. ★ sinc4_smoothed_cdf_fourier_identity
Fourier representation of a smoothed CDF difference
This isolates the Fubini and frequency-zero steps in the smoothing bound. The real CDF difference has an integrable envelope from the first moments, and the sinc kernel has compact Fourier support.
For two probability laws μ and ν with finite first moments and a positive bandwidth T, the convolution at z of their CDF difference with the fourth-power sinc density equals 1/(2π) times the integral over [−T, T] of exp(−itz)·i·(φ_μ(t) − φ_ν(t))/t times the kernel's Fourier transform at t. The quotient is assigned zero at frequency zero, which does not change the interval integral.
Formal statement
Proof (Lean source)
SmoothedCDFFourierSwap 1 core · 0 supporting This module isolates the absolute-integrability and Fubini step after inserting the compact-frequency inverse Fourier formula for sinc fourth. ★ sinc4_smoothed_cdf_fourier_swap
Fubini interchange for a smoothed CDF difference
This module isolates the absolute-integrability and Fubini step after inserting the compact-frequency inverse Fourier formula for sinc fourth.
For two probability laws with finite first moments and a positive bandwidth T, the convolution at z of their CDF difference with the fourth-power sinc density equals 1/(2π) times the integral over [−T, T] of the kernel's Fourier transform times the spatial transform of the shifted CDF difference; no change of variables or division by frequency is used.
Formal statement
Proof (Lean source)
SmoothingKernelTail 1 core · 0 supporting The sinc fourth-power kernel has a quantitative concentration bound at the inverse-bandwidth scale. ★ sinc4Kernel_tail_le_quarter
Tail control for the compact-frequency smoothing kernel
The sinc fourth-power kernel has a quantitative concentration bound at the inverse-bandwidth scale. This is the kernel estimate used when a smoothed CDF is compared with its original CDF.
For a positive bandwidth T, at most one quarter of the fourth-power sinc kernel's mass lies at distance at least 6/T from zero.
Formal statement
Proof (Lean source)
SymmetrizedThirdMoment 1 core · 1 supporting This leaf isolates the moment ingredient of Prawitz's modulus estimate. ★ symmetrized_unit_third_moment_le
Cubic moment control for an independent difference
This leaf isolates the moment ingredient of Prawitz's modulus estimate. The independent difference is integrated against the product law explicitly. The polynomial majorant needs only third moments and products of second moments; it does not require a fourth moment of either marginal.
For a centered probability law with unit second moment and integrable third absolute moment, the difference of two independent draws has an integrable absolute cube whose expectation is at most twice the marginal third absolute moment plus two.
Formal statement
Proof (Lean source)
1 supporting declaration (lemmas, instances)
-
abs_sub_cube_le_moment_polynomialtheorem — The absolute cube of a difference of two real numbers is bounded by a polynomial whose mixed linear terms cancel under centering.hypothesesx y :ℝconclusion|x - y| ^ 3≤ |x| ^ 3 + |y| ^ 3 - 2 * x * y * (|x| + |y|) + x ^ 2 * y ^ 2 + (x ^ 2 + y ^ 2) / 2Proof (Lean source)
theorem abs_sub_cube_le_moment_polynomial (x y : ℝ) : |x - y| ^ 3 ≤ |x| ^ 3 + |y| ^ 3 - 2 * x * y * (|x| + |y|) + x ^ 2 * y ^ 2 + (x ^ 2 + y ^ 2) / 2 := by have hsame (a b : ℝ) (ha : 0 ≤ a) (hb : 0 ≤ b) : |a - b| ^ 3 ≤ a ^ 3 + b ^ 3 - 2 * a * b * (a + b) + a ^ 2 * b ^ 2 + (a ^ 2 + b ^ 2) / 2 := by by_cases hab : b ≤ a · exact nonneg_cube_bound a b ha hb hab · have h := nonneg_cube_bound b a hb ha (le_of_not_ge hab) rw [abs_sub_comm] at h nlinarith [h] have hopposite (a b : ℝ) (ha : 0 ≤ a) (hb : 0 ≤ b) : (a + b) ^ 3 ≤ a ^ 3 + b ^ 3 + 2 * a * b * (a + b) + a ^ 2 * b ^ 2 + (a ^ 2 + b ^ 2) / 2 := by nlinarith [sq_nonneg (a * b - (a + b) / 2), sq_nonneg (a - b)] rcases le_total 0 x with hx | hx <;> rcases le_total 0 y with hy | hy · simpa only [abs_of_nonneg hx, abs_of_nonneg hy] using hsame x y hx hy · have h := hopposite x (-y) hx (neg_nonneg.mpr hy) rw [abs_of_nonneg hx, abs_of_nonpos hy, abs_of_nonneg (show 0 ≤ x - y by linarith)] nlinarith [h] · have h := hopposite (-x) y (neg_nonneg.mpr hx) hy rw [abs_of_nonpos hx, abs_of_nonneg hy, abs_of_nonpos (show x - y ≤ 0 by linarith)] nlinarith [h] · have h := hsame (-x) (-y) (neg_nonneg.mpr hx) (neg_nonneg.mpr hy) have he : |(-x) - (-y)| = |x - y| := by rw [neg_sub_neg, abs_sub_comm] rw [he] at h rw [abs_of_nonpos hx, abs_of_nonpos hy] nlinarith [h]
TriangularCosineIntegral 1 core · 0 supporting The deterministic coefficient is valid at zero frequency as well. ★ triangular_cosine_integral
Fourier coefficient of a triangular weight
The deterministic coefficient is valid at zero frequency as well. Product-to-sum then evaluates the weighted sine coefficients in the Abel expansion of cotangent.
The unit-interval triangular cosine coefficient ∫₀¹ (1 − t)·cos(2πat) dt equals one half of sinc(πa)² at any real frequency a.