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]