Exponential Stein identity

This file isolates the integration-by-parts step behind the local exponential transfer identity used in the proof of Theorem 2.1. The main theorem is a one-sided identity on the positive half-line. Its assumptions expose exactly the two weighted integrability conditions and the boundary condition at infinity needed for improper integration by parts.

theorem Feige.ExponentialStein.integrableOn_comp_mul_exp {φ : ℝ → ℝ} (hφ : Continuous φ) (hbound : ∀ (x : ℝ), ‖φ x‖ ≤ 1) (y a : ℝ) : MeasureTheory.IntegrableOn (fun (e : ℝ) => φ (y + a * e) * Real.exp (-e)) (Set.Ioi 0) MeasureTheory.volume

A uniformly unit-bounded continuous function, composed with an affine path and multiplied by the exponential density, is integrable on the positive half-line.

theorem Feige.ExponentialStein.tendsto_comp_mul_exp_atTop {φ : ℝ → ℝ} (hbound : ∀ (x : ℝ), ‖φ x‖ ≤ 1) (y a : ℝ) : Filter.Tendsto (fun (e : ℝ) => φ (y + a * e) * Real.exp (-e)) Filter.atTop (nhds 0)

The same exponential damping forces the affine composite to vanish at infinity.

theorem Feige.ExponentialStein.integral_Ioi_comp_exp_sub {φ φ' : ℝ → ℝ} {y a : ℝ} (hφ : ∀ (x : ℝ), HasDerivAt φ (φ' x) x) (hintφ : MeasureTheory.IntegrableOn (fun (e : ℝ) => φ (y + a * e) * Real.exp (-e)) (Set.Ioi 0) MeasureTheory.volume) (hintφ' : MeasureTheory.IntegrableOn (fun (e : ℝ) => a * φ' (y + a * e) * Real.exp (-e)) (Set.Ioi 0) MeasureTheory.volume) (hzero : Filter.Tendsto (fun (e : ℝ) => φ (y + a * e) * Real.exp (-e)) (nhdsWithin 0 (Set.Ioi 0)) (nhds (φ y))) (htop : Filter.Tendsto (fun (e : ℝ) => φ (y + a * e) * Real.exp (-e)) Filter.atTop (nhds 0)) : (∫ (e : ℝ) in Set.Ioi 0, φ (y + a * e) * Real.exp (-e)) - φ y = ∫ (e : ℝ) in Set.Ioi 0, a * φ' (y + a * e) * Real.exp (-e)

One-sided exponential integration by parts.

For a differentiable function φ, this says

∫₀∞ φ(y + a e)e⁻ᵉ de - φ(y) = a ∫₀∞ φ'(y + a e)e⁻ᵉ de.

The hypotheses are deliberately stated as the precise weighted integrability and boundary requirements. Bounded φ and bounded φ' satisfy them, as do many unbounded test functions.

theorem Feige.ExponentialStein.two_sided_integral_Ioi {φ φ' : ℝ → ℝ} {y a b : ℝ} (hφ : ∀ (x : ℝ), HasDerivAt φ (φ' x) x) (hintPlus : MeasureTheory.IntegrableOn (fun (e : ℝ) => φ (y + a * e) * Real.exp (-e)) (Set.Ioi 0) MeasureTheory.volume) (hintDerivPlus : MeasureTheory.IntegrableOn (fun (e : ℝ) => a * φ' (y + a * e) * Real.exp (-e)) (Set.Ioi 0) MeasureTheory.volume) (hzeroPlus : Filter.Tendsto (fun (e : ℝ) => φ (y + a * e) * Real.exp (-e)) (nhdsWithin 0 (Set.Ioi 0)) (nhds (φ y))) (htopPlus : Filter.Tendsto (fun (e : ℝ) => φ (y + a * e) * Real.exp (-e)) Filter.atTop (nhds 0)) (hintMinus : MeasureTheory.IntegrableOn (fun (e : ℝ) => φ (y - b * e) * Real.exp (-e)) (Set.Ioi 0) MeasureTheory.volume) (hintDerivMinus : MeasureTheory.IntegrableOn (fun (e : ℝ) => -b * φ' (y - b * e) * Real.exp (-e)) (Set.Ioi 0) MeasureTheory.volume) (hzeroMinus : Filter.Tendsto (fun (e : ℝ) => φ (y - b * e) * Real.exp (-e)) (nhdsWithin 0 (Set.Ioi 0)) (nhds (φ y))) (htopMinus : Filter.Tendsto (fun (e : ℝ) => φ (y - b * e) * Real.exp (-e)) Filter.atTop (nhds 0)) : (∫ (e : ℝ) in Set.Ioi 0, φ (y + a * e) * Real.exp (-e)) - ∫ (e : ℝ) in Set.Ioi 0, φ (y - b * e) * Real.exp (-e) = (∫ (e : ℝ) in Set.Ioi 0, a * φ' (y + a * e) * Real.exp (-e)) + b * ∫ (e : ℝ) in Set.Ioi 0, φ' (y - b * e) * Real.exp (-e)

Two-sided exponential Stein identity at a fixed value of y.

This is the two-sided identity before averaging over the law of Y. The first four analytic hypotheses are the one-sided requirements for y + aE; the next four are those for y - bE.

theorem Feige.ExponentialStein.integral_Ioi_mul_deriv_one_kink {u v u' v' : ℝ → ℝ} {k a' b' : ℝ} (hk : 0 < k) (hu_cont : Continuous u) (hv_cont : Continuous v) (hu : ∀ (x : ℝ), 0 < x → x ≠ k → HasDerivAt u (u' x) x) (hv : ∀ (x : ℝ), 0 < x → HasDerivAt v (v' x) x) (hu'_fin : IntervalIntegrable u' MeasureTheory.volume 0 k) (hv'_fin : IntervalIntegrable v' MeasureTheory.volume 0 k) (huv'_int : MeasureTheory.IntegrableOn (u * v') (Set.Ioi 0) MeasureTheory.volume) (hu'v_int : MeasureTheory.IntegrableOn (u' * v) (Set.Ioi 0) MeasureTheory.volume) (h_zero : u 0 * v 0 = a') (h_top : Filter.Tendsto (u * v) Filter.atTop (nhds b')) : ∫ (x : ℝ) in Set.Ioi 0, u x * v' x = b' - a' - ∫ (x : ℝ) in Set.Ioi 0, u' x * v x

Improper integration by parts with one possible nondifferentiability point k in the positive half-line. The finite interval theorem does not require differentiability at its right endpoint, and the improper tail theorem does not require it at its left endpoint, so the two pieces join using continuity alone.