English
The Mellin transform of the indicator of Ioc(0,1) with value 1 is 1/s (when Re(s) > 0).
Русский
Преобразование Меллина индиикатора Ioc(0,1) со значением 1 равно 1/s (при Re(s) > 0).
LaTeX
$$$\text{HasMellin}(\mathbf{1}_{Ioc(0,1)}, s, 1/s).$$$
Lean4
/-- The Mellin transform of the indicator function of `Ioc 0 1`. -/
theorem hasMellin_one_Ioc {s : ℂ} (hs : 0 < re s) : HasMellin (indicator (Ioc 0 1) (fun _ => 1 : ℝ → ℂ)) s (1 / s) :=
by
have aux1 : -1 < (s - 1).re := by simpa only [sub_re, one_re, sub_eq_add_neg] using lt_add_of_pos_left _ hs
have aux2 : s ≠ 0 := by contrapose! hs; rw [hs, zero_re]
have aux3 : MeasurableSet (Ioc (0 : ℝ) 1) := measurableSet_Ioc
simp_rw [HasMellin, mellin, MellinConvergent, ← indicator_smul, IntegrableOn, integrable_indicator_iff aux3,
smul_eq_mul, integral_indicator aux3, mul_one, IntegrableOn,
Measure.restrict_restrict_of_subset Ioc_subset_Ioi_self]
rw [← IntegrableOn, ← intervalIntegrable_iff_integrableOn_Ioc_of_le zero_le_one]
refine ⟨intervalIntegral.intervalIntegrable_cpow' aux1, ?_⟩
rw [← intervalIntegral.integral_of_le zero_le_one, integral_cpow (Or.inl aux1), sub_add_cancel, ofReal_zero,
ofReal_one, one_cpow, zero_cpow aux2, sub_zero]
