Taylor bounds for characteristic functions

TheoremGlobal second-order bound for the imaginary exponential#✓fully proved

For every real number \(u\), \(|e^{iu} - 1 - iu| \le u^2\), with no restriction on the size of \(u\).

The proof splits at \(u^2 \le 27\): in that range the squared norm is \((1 - \cos u)^2 + (u - \sin u)^2 \le u^4/4 + u^6/36 \le u^4\), using \(1 - \cos u \le u^2/2\) and \(|u - \sin u| \le |u|^3/6\); outside that range \(|u| > 5\) and the triangle inequality gives \(2 + |u| \le u^2\).

theorem norm_exp_ofReal_mul_I_sub_one_sub_le (u : ℝ) :
    ‖Complex.exp (↑u * Complex.I) - 1 - ↑u * Complex.I‖ ≤ u ^ 2

Used by 1

Used bySecond-order Taylor bound for the characteristic function

TheoremSecond-order Taylor bound for the characteristic function#✓fully proved

Let \(X\) be a measurable real random variable on a probability space with \(X^2\) integrable, and let \(\varphi_X\) be the characteristic function of the law of \(X\). Then for every real \(t\), \(|\varphi_X(t) - 1 - it\,\mathbb{E}[X]| \le t^2 \, \mathbb{E}[X^2]\).

theorem norm_charFun_sub_one_sub_le
    {Ω : Type*} [MeasurableSpace Ω] {μ : Measure Ω} [IsProbabilityMeasure μ]
    (X : Ω → ℝ) (hmeas : Measurable X)
    (hX_sq_int : Integrable (fun ω => (X ω) ^ 2) μ)
    (t : ℝ) :
    ‖charFun (μ.map X) t - 1 - ↑t * Complex.I * ↑(∫ ω, X ω ∂μ)‖
      ≤ t ^ 2 * ∫ ω, (X ω) ^ 2 ∂μ

Uses 1 · Used by 1

Proof usesGlobal second-order bound for the imaginary exponential

Used byCharacteristic-function second-order bound

TheoremFirst-order Taylor bound for the characteristic function#✓fully proved

Let \(X\) be a measurable real random variable on a probability space with \(|X|\) integrable, and let \(\varphi_X\) be the characteristic function of the law of \(X\). Then for every real \(t\), \(|\varphi_X(t) - 1| \le |t| \, \mathbb{E}|X|\).

theorem norm_charFun_sub_one_le
    {Ω : Type*} [MeasurableSpace Ω] {μ : Measure Ω} [IsProbabilityMeasure μ]
    (X : Ω → ℝ) (hmeas : Measurable X) (hX_int : Integrable (fun ω => |X ω|) μ)
    (t : ℝ) :
    ‖charFun (μ.map X) t - 1‖ ≤ |t| * ∫ ω, |X ω| ∂μ

TheoremCharacteristic-function second-order bound#✓fully proved

Let \(X\) be a measurable real random variable on a probability space with \(\mathbb{E}[X] = 0\) and \(X^2\) integrable, and let \(\varphi_X\) be the characteristic function of the law of \(X\). Then for every real \(t\), \(|\varphi_X(t) - 1| \le t^2 \, \mathbb{E}[X^2]\).

theorem norm_charFun_sub_one_le_sq_mul_variance
    {Ω : Type*} [MeasurableSpace Ω] {μ : Measure Ω} [IsProbabilityMeasure μ]
    (X : Ω → ℝ) (hmeas : Measurable X)
    (hmean : ∫ ω, X ω ∂μ = 0)
    (hint2 : Integrable (fun ω => (X ω) ^ 2) μ)
    (t : ℝ) :
    ‖charFun (μ.map X) t - 1‖ ≤ t ^ 2 * ∫ ω, (X ω) ^ 2 ∂μ

Uses 1

Proof usesSecond-order Taylor bound for the characteristic function

4 fully proved

The dependency explorer needs JavaScript and its graph data.

Download the complete graph data.