Characteristic function of the walk and Fourier inversion on ℤ

For the step law X = K - 1 (PoissonDeclumping.stepLaw) and the walk law PoissonDeclumping.walkLaw μ n (an n-fold convolution, source lines 174–181, 842–845):

• PoissonDeclumping.Stable.walkCF_eq_pow: E e^{iθ S_n} = φ(θ)^n with φ = stepCF μ;
• PoissonDeclumping.Stable.charFun_walkLaw_map_div: the characteristic function of S_n / c is φ(t/c)^n;
• PoissonDeclumping.Stable.walkLaw_real_singleton: Fourier inversion on ℤ, P(S_n = k) = (1/2π) ∫_{-π}^{π} φ(θ)^n e^{-ikθ} dθ.

theorem PoissonDeclumping.Stable.isProbabilityMeasure_stepLaw (μ : PMF ℕ) : MeasureTheory.IsProbabilityMeasure (stepLaw μ)

Compatibility name for the common step-law probability instance, without a new instance.

theorem PoissonDeclumping.Stable.isProbabilityMeasure_walkLaw (μ : PMF ℕ) (n : ℕ) : MeasureTheory.IsProbabilityMeasure (walkLaw μ n)

Compatibility name for the common walk-law probability instance, without a new instance.

noncomputable def PoissonDeclumping.Stable.stepCF (μ : PMF ℕ) (θ : ℝ) : ℂ

The characteristic function φ(θ) = E e^{iθX} of one step.

Equations

• PoissonDeclumping.Stable.stepCF μ θ = ∫ (z : ℤ), Complex.exp (↑θ * ↑z * Complex.I) ∂PoissonDeclumping.stepLaw μ

noncomputable def PoissonDeclumping.Stable.walkCF (μ : PMF ℕ) (n : ℕ) (θ : ℝ) : ℂ

The characteristic function E e^{iθ S_n} of the walk at time n.

Equations

• PoissonDeclumping.Stable.walkCF μ n θ = ∫ (z : ℤ), Complex.exp (↑θ * ↑z * Complex.I) ∂PoissonDeclumping.walkLaw μ n

theorem PoissonDeclumping.Stable.integral_conv_int {W P : MeasureTheory.Measure ℤ} (F : ℤ → ℂ) : ∫ (z : ℤ), F z ∂W.conv P = ∫ (p : ℤ × ℤ), F (p.1 + p.2) ∂W.prod P

theorem PoissonDeclumping.Stable.walkCF_eq_pow (μ : PMF ℕ) (n : ℕ) (θ : ℝ) : walkCF μ n θ = stepCF μ θ ^ n

theorem PoissonDeclumping.Stable.norm_walkCF_le (μ : PMF ℕ) (n : ℕ) (θ : ℝ) : ‖walkCF μ n θ‖ ≤ 1

theorem PoissonDeclumping.Stable.norm_stepCF_le (μ : PMF ℕ) (θ : ℝ) : ‖stepCF μ θ‖ ≤ 1

theorem PoissonDeclumping.Stable.continuous_stepCF (μ : PMF ℕ) : Continuous (stepCF μ)

theorem PoissonDeclumping.Stable.charFun_walkLaw_map_div (μ : PMF ℕ) (n : ℕ) (c t : ℝ) : MeasureTheory.charFun (MeasureTheory.Measure.map (fun (z : ℤ) => ↑z / c) (walkLaw μ n)) t = stepCF μ (t / c) ^ n

The characteristic function of S_n / c is φ(θ/c)^n.

theorem PoissonDeclumping.Stable.intervalIntegral_cexp_int_mul_I (m : ℤ) : ∫ (θ : ℝ) in -Real.pi..Real.pi, Complex.exp (↑θ * ↑m * Complex.I) = if m = 0 then ↑(2 * Real.pi) else 0

theorem PoissonDeclumping.Stable.walkLaw_real_singleton (μ : PMF ℕ) (n : ℕ) (k : ℤ) : ↑((walkLaw μ n).real {k}) = 1 / (2 * ↑Real.pi) * ∫ (θ : ℝ) in -Real.pi..Real.pi, stepCF μ θ ^ n * Complex.exp (-(↑θ * ↑k * Complex.I))

Fourier inversion on ℤ: P(S_n = k) = (1/2π) ∫_{-π}^{π} φ(θ)^n e^{-ikθ} dθ.