English
An auxiliary equality expresses equivalence between two representations of f_modif's deviation from f, via indicator-based decompositions on intervals (0,1) and at 1, ensuring consistency on (0,∞).
Русский
Вспомогательное равенство выражает эквивалентность двух представлений отклонения f_modif от f через индикаторы на интервалах (0,1) и в точке 1.
LaTeX
$$f_modif_aux1 : EqOn (fun x => f_modif x - f x + f0) ( (Ioo 0 1).indicator (fun x => f0 - (ε * x^(−k)) • g0) + {1}.indicator (fun _ => f0 - f 1) ) (Ioi 0)$$
Lean4
/-- Compute the Mellin transform of the modifying term used to kill off the constants at
`0` and `∞`. -/
theorem f_modif_aux2 [CompleteSpace E] {s : ℂ} (hs : P.k < re s) :
mellin (fun x ↦ P.f_modif x - P.f x + P.f₀) s = (1 / s) • P.f₀ + (P.ε / (P.k - s)) • P.g₀ :=
by
have h_re1 : -1 < re (s - 1) := by simpa using P.hk.trans hs
have h_re2 : -1 < re (s - P.k - 1) := by simpa using hs
calc
_ =
∫ (x : ℝ) in Ioi 0,
(x : ℂ) ^ (s - 1) •
((Ioo 0 1).indicator (fun t : ℝ ↦ P.f₀ - (P.ε * ↑(t ^ (-P.k))) • P.g₀) x +
({ 1 } : Set ℝ).indicator (fun _ ↦ P.f₀ - P.f 1) x) :=
setIntegral_congr_fun measurableSet_Ioi (fun x hx ↦ by simp [f_modif_aux1 P hx])
_ =
∫ (x : ℝ) in Ioi 0,
(x : ℂ) ^ (s - 1) • ((Ioo 0 1).indicator (fun t : ℝ ↦ P.f₀ - (P.ε * ↑(t ^ (-P.k))) • P.g₀) x) :=
by
refine
setIntegral_congr_ae measurableSet_Ioi
(eventually_of_mem (U := { 1 }ᶜ) (compl_mem_ae_iff.mpr (subsingleton_singleton.measure_zero _))
(fun x hx _ ↦ ?_))
rw [indicator_of_notMem hx, add_zero]
_ = ∫ (x : ℝ) in Ioc 0 1, (x : ℂ) ^ (s - 1) • (P.f₀ - (P.ε * ↑(x ^ (-P.k))) • P.g₀) := by
simp_rw [← indicator_smul, setIntegral_indicator measurableSet_Ioo, inter_eq_right.mpr Ioo_subset_Ioi_self,
integral_Ioc_eq_integral_Ioo]
_ = ∫ x : ℝ in Ioc 0 1, ((x : ℂ) ^ (s - 1) • P.f₀ - P.ε • (x : ℂ) ^ (s - P.k - 1) • P.g₀) :=
by
refine setIntegral_congr_fun measurableSet_Ioc (fun x ⟨hx, _⟩ ↦ ?_)
rw [ofReal_cpow hx.le, ofReal_neg, smul_sub, ← mul_smul, mul_comm, mul_assoc, mul_smul, mul_comm, ←
cpow_add _ _ (ofReal_ne_zero.mpr hx.ne'), ← sub_eq_add_neg, sub_right_comm]
_ =
(∫ (x : ℝ) in Ioc 0 1, (x : ℂ) ^ (s - 1)) • P.f₀ -
P.ε • (∫ (x : ℝ) in Ioc 0 1, (x : ℂ) ^ (s - P.k - 1)) • P.g₀ :=
by
rw [integral_sub, integral_smul, integral_smul_const, integral_smul_const]
· apply Integrable.smul_const
rw [← IntegrableOn, ← intervalIntegrable_iff_integrableOn_Ioc_of_le zero_le_one]
exact intervalIntegral.intervalIntegrable_cpow' h_re1
· refine (Integrable.smul_const ?_ _).smul _
rw [← IntegrableOn, ← intervalIntegrable_iff_integrableOn_Ioc_of_le zero_le_one]
exact intervalIntegral.intervalIntegrable_cpow' h_re2
_ = _ := by
simp_rw [← intervalIntegral.integral_of_le zero_le_one, integral_cpow (Or.inl h_re1),
integral_cpow (Or.inl h_re2), ofReal_zero, ofReal_one, one_cpow, sub_add_cancel,
zero_cpow fun h ↦ lt_irrefl _ (P.hk.le.trans_lt (zero_re ▸ h ▸ hs)),
zero_cpow (sub_ne_zero.mpr (fun h ↦ lt_irrefl _ ((ofReal_re _) ▸ h ▸ hs)) : s - P.k ≠ 0), sub_zero,
sub_eq_add_neg (_ • _), ← mul_smul, ← neg_smul, mul_one_div, ← div_neg, neg_sub]
