integral_charFun_Icc — Mathlib

English

Let μ be a finite measure and r > 0. Then the integral of the characteristic function over the interval [-r, r] equals 2r times the integral of sinc(r x) with respect to μ: ∫_{-r}^{r} χ_μ(t) dt = 2 r ∫ x sinc(r x) dμ.

Русский

Пусть μ — конечная мера, а r > 0. Тогда интеграл характеристической функции по интервалу [-r, r] равен 2r умножить на интеграл sinc(r x) по μ: ∫ χ_μ(t) dt = 2 r ∫ sinc(r x) dμ.

LaTeX

$$$\int_{-r}^{r} \operatorname{charFun}_{\mu}(t) \, dt = 2 r \int x \, \operatorname{sinc}(r x) \, d\mu(x)$$$

Lean4

theorem integral_charFun_Icc [IsFiniteMeasure μ] (hr : 0 < r) :
    ∫ t in -r..r, charFun μ t = 2 * r * ∫ x, sinc (r * x) ∂μ :=
  by
  have h_int :
    Integrable (Function.uncurry fun (x y : ℝ) ↦ cexp (x * y * I)) ((volume.restrict (Set.uIoc (-r) r)).prod μ) :=
    by
    simp only [neg_le_self_iff, hr.le, Set.uIoc_of_le]
      -- integrable since the function has norm 1 everywhere and the measure is finite

    rw [← integrable_norm_iff (by fun_prop)]
    suffices (fun a => ‖Function.uncurry (fun (x y : ℝ) ↦ cexp (x * y * I)) a‖) = fun _ ↦ 1
      by
      rw [this]
      fun_prop
    ext p
    rw [← Prod.mk.eta (p := p)]
    norm_cast
    simp only [Function.uncurry_apply_pair, norm_exp_ofReal_mul_I]
  calc
    ∫ t in -r..r, charFun μ t
    _ = ∫ x in -r..r, ∫ y, cexp (x * y * I) ∂μ := by simp_rw [charFun_apply_real]
    _ = ∫ y, ∫ x in -r..r, cexp (x * y * I) ∂volume ∂μ := by rw [intervalIntegral_integral_swap h_int]
    _ = ∫ y, if r * y = 0 then 2 * (r : ℂ) else y⁻¹ * ∫ x in -(y * r)..y * r, cexp (x * I) ∂volume ∂μ :=
      by
      congr with y
      by_cases hy : y = 0
      · simp [hy, two_mul]
      simp only [mul_eq_zero, hr.ne', hy, or_self, ↓reduceIte, ofReal_inv]
      have h :=
        intervalIntegral.integral_comp_smul_deriv (E := ℂ) (a := -r) (b := r) (f := fun x ↦ y * x) (f' := fun _ ↦ y)
          (g := fun x ↦ cexp (x * I)) ?_ (by fun_prop) (by fun_prop)
      swap
      · intro x hx
        simp_rw [mul_comm y]
        exact hasDerivAt_mul_const _
      simp only [Function.comp_apply, ofReal_mul, real_smul, intervalIntegral.integral_const_mul, mul_neg] at h
      rw [← h, ← mul_assoc]
      norm_cast
      simp [mul_comm _ y, mul_inv_cancel₀ hy]
    _ = ∫ x, 2 * (r : ℂ) * sinc (r * x) ∂μ := by
      congr with y
      rw [integral_exp_mul_I_eq_sinc]
      split_ifs with hry
      · simp [hry]
      have hy : y ≠ 0 := fun hy ↦ hry (by simp [hy])
      norm_cast
      field_simp
    _ = 2 * r * ∫ x, sinc (r * x) ∂μ := by
      norm_cast
      rw [integral_complex_ofReal, ← integral_const_mul]

Похожие утверждения