Test functions for the exponential transfer identity

This file formalizes the two test functions used in the exponential transfer identity. They are written with max and min; for positive c,d this is equivalent to the corresponding indicator notation and makes global continuity transparent.

noncomputable def Feige.TransferTestFunctions.transferPhi (d x : ℝ) : ℝ

φ(x) = (1 - exp (-x/d)) 1_{x ≥ 0} for d > 0.

Equations

• Feige.TransferTestFunctions.transferPhi d x = max 0 (1 - Real.exp (-x / d))

noncomputable def Feige.TransferTestFunctions.transferPsi (c x : ℝ) : ℝ

ψ(x) = 1_{x ≥ 0} + exp (x/c) 1_{x < 0} for c > 0.

Equations

• Feige.TransferTestFunctions.transferPsi c x = min 1 (Real.exp (x / c))

theorem Feige.TransferTestFunctions.transferPhi_of_nonneg {d x : ℝ} (hd : 0 < d) (hx : 0 ≤ x) : transferPhi d x = 1 - Real.exp (-x / d)

theorem Feige.TransferTestFunctions.transferPhi_of_nonpos {d x : ℝ} (hd : 0 < d) (hx : x ≤ 0) : transferPhi d x = 0

theorem Feige.TransferTestFunctions.transferPsi_of_nonneg {c x : ℝ} (hc : 0 < c) (hx : 0 ≤ x) : transferPsi c x = 1

theorem Feige.TransferTestFunctions.transferPsi_of_nonpos {c x : ℝ} (hc : 0 < c) (hx : x ≤ 0) : transferPsi c x = Real.exp (x / c)

theorem Feige.TransferTestFunctions.continuous_transferPhi (d : ℝ) : Continuous (transferPhi d)

φ is continuous, including at its joining point zero.

theorem Feige.TransferTestFunctions.continuous_transferPsi (c : ℝ) : Continuous (transferPsi c)

ψ is continuous, including at its joining point zero.

theorem Feige.TransferTestFunctions.transferPhi_nonneg (d x : ℝ) : 0 ≤ transferPhi d x

theorem Feige.TransferTestFunctions.transferPhi_le_one {d x : ℝ} (hd : 0 < d) : transferPhi d x ≤ 1

theorem Feige.TransferTestFunctions.transferPsi_nonneg (c x : ℝ) : 0 ≤ transferPsi c x

theorem Feige.TransferTestFunctions.transferPsi_le_one (c x : ℝ) : transferPsi c x ≤ 1

theorem Feige.TransferTestFunctions.norm_transferPhi_le_one {d : ℝ} (hd : 0 < d) (x : ℝ) : ‖transferPhi d x‖ ≤ 1

theorem Feige.TransferTestFunctions.norm_transferPsi_le_one (c x : ℝ) : ‖transferPsi c x‖ ≤ 1

theorem Feige.TransferTestFunctions.integrableOn_transferPhi_affine_mul_exp {d : ℝ} (hd : 0 < d) (y a : ℝ) : MeasureTheory.IntegrableOn (fun (e : ℝ) => transferPhi d (y + a * e) * Real.exp (-e)) (Set.Ioi 0) MeasureTheory.volume

Exponential-weight integrability required by the Stein identity.

theorem Feige.TransferTestFunctions.integrableOn_transferPsi_affine_mul_exp (c y a : ℝ) : MeasureTheory.IntegrableOn (fun (e : ℝ) => transferPsi c (y + a * e) * Real.exp (-e)) (Set.Ioi 0) MeasureTheory.volume

theorem Feige.TransferTestFunctions.tendsto_transferPhi_affine_mul_exp_atTop {d : ℝ} (hd : 0 < d) (y a : ℝ) : Filter.Tendsto (fun (e : ℝ) => transferPhi d (y + a * e) * Real.exp (-e)) Filter.atTop (nhds 0)

Exponential damping supplies the boundary term at infinity.

theorem Feige.TransferTestFunctions.tendsto_transferPsi_affine_mul_exp_atTop (c y a : ℝ) : Filter.Tendsto (fun (e : ℝ) => transferPsi c (y + a * e) * Real.exp (-e)) Filter.atTop (nhds 0)

theorem Feige.TransferTestFunctions.hasDerivAt_transferPhi_of_pos {d x : ℝ} (hd : 0 < d) (hx : 0 < x) : HasDerivAt (transferPhi d) (Real.exp (-x / d) / d) x

Derivative of φ on the positive half-line.

theorem Feige.TransferTestFunctions.hasDerivAt_transferPhi_of_neg {d x : ℝ} (hd : 0 < d) (hx : x < 0) : HasDerivAt (transferPhi d) 0 x

Derivative of φ on the negative half-line.

theorem Feige.TransferTestFunctions.hasDerivAt_transferPsi_of_pos {c x : ℝ} (hc : 0 < c) (hx : 0 < x) : HasDerivAt (transferPsi c) 0 x

Derivative of ψ on the positive half-line.

theorem Feige.TransferTestFunctions.hasDerivAt_transferPsi_of_neg {c x : ℝ} (hc : 0 < c) (hx : x < 0) : HasDerivAt (transferPsi c) (Real.exp (x / c) / c) x

Derivative of ψ on the negative half-line.

theorem Feige.TransferTestFunctions.hasDerivAt_transferPhi_of_ne_zero {d x : ℝ} (hd : 0 < d) (hx : x ≠ 0) : HasDerivAt (transferPhi d) (if 0 < x then Real.exp (-x / d) / d else 0) x

Away from zero, φ' has the piecewise formula used by the transfer identity.

theorem Feige.TransferTestFunctions.hasDerivAt_transferPsi_of_ne_zero {c x : ℝ} (hc : 0 < c) (hx : x ≠ 0) : HasDerivAt (transferPsi c) (if x < 0 then Real.exp (x / c) / c else 0) x

Away from zero, ψ' has the piecewise formula used by the transfer identity.

noncomputable def Feige.TransferTestFunctions.transferPhiDeriv (d x : ℝ) : ℝ

The a.e. derivative used when applying Stein's identity to φ.

Equations

• Feige.TransferTestFunctions.transferPhiDeriv d x = if 0 < x then Real.exp (-x / d) / d else 0

noncomputable def Feige.TransferTestFunctions.transferPsiDeriv (c x : ℝ) : ℝ

The a.e. derivative used when applying Stein's identity to ψ.

Equations

• Feige.TransferTestFunctions.transferPsiDeriv c x = if x < 0 then Real.exp (x / c) / c else 0

theorem Feige.TransferTestFunctions.measurable_transferPhiDeriv (d : ℝ) : Measurable (transferPhiDeriv d)

theorem Feige.TransferTestFunctions.measurable_transferPsiDeriv (c : ℝ) : Measurable (transferPsiDeriv c)

theorem Feige.TransferTestFunctions.norm_transferPhiDeriv_le {d : ℝ} (hd : 0 < d) (x : ℝ) : ‖transferPhiDeriv d x‖ ≤ 1 / d

theorem Feige.TransferTestFunctions.norm_transferPsiDeriv_le {c : ℝ} (hc : 0 < c) (x : ℝ) : ‖transferPsiDeriv c x‖ ≤ 1 / c

theorem Feige.TransferTestFunctions.integrableOn_transferPhiDeriv_affine_mul_exp {d : ℝ} (hd : 0 < d) (y a : ℝ) : MeasureTheory.IntegrableOn (fun (e : ℝ) => a * transferPhiDeriv d (y + a * e) * Real.exp (-e)) (Set.Ioi 0) MeasureTheory.volume

Weighted integrability of the formal derivative of φ along an affine path.

theorem Feige.TransferTestFunctions.integrableOn_transferPsiDeriv_affine_mul_exp {c : ℝ} (hc : 0 < c) (y a : ℝ) : MeasureTheory.IntegrableOn (fun (e : ℝ) => a * transferPsiDeriv c (y + a * e) * Real.exp (-e)) (Set.Ioi 0) MeasureTheory.volume

Weighted integrability of the formal derivative of ψ.

theorem Feige.TransferTestFunctions.intervalIntegrable_transferPhiDeriv_affine {d : ℝ} (hd : 0 < d) (y a r s : ℝ) (hrs : r ≤ s) : IntervalIntegrable (fun (e : ℝ) => a * transferPhiDeriv d (y + a * e)) MeasureTheory.volume r s

The formal derivative of φ is integrable on every finite interval.

theorem Feige.TransferTestFunctions.intervalIntegrable_transferPsiDeriv_affine {c : ℝ} (hc : 0 < c) (y a r s : ℝ) (hrs : r ≤ s) : IntervalIntegrable (fun (e : ℝ) => a * transferPsiDeriv c (y + a * e)) MeasureTheory.volume r s

The formal derivative of ψ is integrable on every finite interval.

theorem Feige.TransferTestFunctions.ae_hasDerivAt_transferPhi_comp_affine {d y a : ℝ} (hd : 0 < d) (ha : a ≠ 0) : ∀ᵐ (e : ℝ), HasDerivAt (transferPhi d ∘ fun (t : ℝ) => y + a * t) (a * transferPhiDeriv d (y + a * e)) e

An affine path hits the exceptional point zero only on a null set, so the composite φ (y + a e) has the expected derivative a.e.

theorem Feige.TransferTestFunctions.ae_hasDerivAt_transferPsi_comp_affine {c y a : ℝ} (hc : 0 < c) (ha : a ≠ 0) : ∀ᵐ (e : ℝ), HasDerivAt (transferPsi c ∘ fun (t : ℝ) => y + a * t) (a * transferPsiDeriv c (y + a * e)) e

The analogous a.e. composite derivative statement for ψ.

theorem Feige.TransferTestFunctions.transferPhi_stein_fixed {d y a : ℝ} (hd : 0 < d) (ha : a ≠ 0) : (∫ (e : ℝ) in Set.Ioi 0, transferPhi d (y + a * e) * Real.exp (-e)) - transferPhi d y = ∫ (e : ℝ) in Set.Ioi 0, a * transferPhiDeriv d (y + a * e) * Real.exp (-e)

Fixed-y, positive-scale one-sided Stein identity for the first test function. The proof splits according to whether the unique affine kink -y/a lies in the positive half-line.

theorem Feige.TransferTestFunctions.transferPsi_stein_fixed {c y a : ℝ} (hc : 0 < c) (ha : a ≠ 0) : (∫ (e : ℝ) in Set.Ioi 0, transferPsi c (y + a * e) * Real.exp (-e)) - transferPsi c y = ∫ (e : ℝ) in Set.Ioi 0, a * transferPsiDeriv c (y + a * e) * Real.exp (-e)

Fixed-y, positive-scale one-sided Stein identity for ψ.

theorem Feige.TransferTestFunctions.transferPhi_stein_fixed_sub {d y b : ℝ} (hd : 0 < d) (hb : 0 < b) : transferPhi d y - ∫ (e : ℝ) in Set.Ioi 0, transferPhi d (y - b * e) * Real.exp (-e) = ∫ (e : ℝ) in Set.Ioi 0, b * transferPhiDeriv d (y - b * e) * Real.exp (-e)

Negative-affine fixed-y Stein identity for φ.

theorem Feige.TransferTestFunctions.transferPsi_stein_fixed_sub {c y b : ℝ} (hc : 0 < c) (hb : 0 < b) : transferPsi c y - ∫ (e : ℝ) in Set.Ioi 0, transferPsi c (y - b * e) * Real.exp (-e) = ∫ (e : ℝ) in Set.Ioi 0, b * transferPsiDeriv c (y - b * e) * Real.exp (-e)

Negative-affine fixed-y Stein identity for ψ.

theorem Feige.TransferTestFunctions.transferPhi_stein_fixed_two_sided {d y a b : ℝ} (hd : 0 < d) (ha : 0 < a) (hb : 0 < b) : (∫ (e : ℝ) in Set.Ioi 0, transferPhi d (y + a * e) * Real.exp (-e)) - ∫ (e : ℝ) in Set.Ioi 0, transferPhi d (y - b * e) * Real.exp (-e) = (∫ (e : ℝ) in Set.Ioi 0, a * transferPhiDeriv d (y + a * e) * Real.exp (-e)) + ∫ (e : ℝ) in Set.Ioi 0, b * transferPhiDeriv d (y - b * e) * Real.exp (-e)

Fixed-y two-sided exponential Stein identity for φ.

theorem Feige.TransferTestFunctions.transferPsi_stein_fixed_two_sided {c y a b : ℝ} (hc : 0 < c) (ha : 0 < a) (hb : 0 < b) : (∫ (e : ℝ) in Set.Ioi 0, transferPsi c (y + a * e) * Real.exp (-e)) - ∫ (e : ℝ) in Set.Ioi 0, transferPsi c (y - b * e) * Real.exp (-e) = (∫ (e : ℝ) in Set.Ioi 0, a * transferPsiDeriv c (y + a * e) * Real.exp (-e)) + ∫ (e : ℝ) in Set.Ioi 0, b * transferPsiDeriv c (y - b * e) * Real.exp (-e)

Fixed-y two-sided exponential Stein identity for ψ.