-- Mathlib/NumberTheory/LSeries/AbstractFuncEq.lean
/-- Compute the Mellin transform of the modifying term used to kill off the constants at
`0` and `∞`. -/
lemma 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₀

Proof state:
E : Type u_1
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℂ E
P : WeakFEPair E
inst✝ : CompleteSpace E
s : ℂ
hs : P.k < s.re
h_re1 : -1 < (s - 1).re
⊢ mellin (fun x => P.f_modif x - P.f x + P.f₀) s = (1 / s) • P.f₀ + (P.ε / (↑P.k - s)) • P.g₀

Tactic:
have h_re2 : -1 < re (s - P.k - 1) := by simpa using hs

Result:
E : Type u_1
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℂ E
P : WeakFEPair E
inst✝ : CompleteSpace E
s : ℂ
hs : P.k < s.re
h_re1 : -1 < (s - 1).re
h_re2 : -1 < (s - ↑P.k - 1).re
⊢ mellin (fun x => P.f_modif x - P.f x + P.f₀) s = (1 / s) • P.f₀ + (P.ε / (↑P.k - s)) • P.g₀

Proof state:
E : Type u_1
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℂ E
P : WeakFEPair E
inst✝ : CompleteSpace E
s : ℂ
hs : P.k < s.re
h_re1 : -1 < (s - 1).re
h_re2 : -1 < (s - ↑P.k - 1).re
x : ℝ
hx : x ∈ {1}ᶜ
x✝ : x ∈ Ioi 0
⊢ ↑x ^ (s - 1) •
      ((Ioo 0 1).indicator (fun t => P.f₀ - (P.ε * ↑(t ^ (-P.k))) • P.g₀) x + {1}.indicator (fun x => P.f₀ - P.f 1) x) =
    ↑x ^ (s - 1) • (Ioo 0 1).indicator (fun t => P.f₀ - (P.ε * ↑(t ^ (-P.k))) • P.g₀) x

Tactic:
rw [indicator_of_not_mem hx, add_zero]

Result:
no goals

Proof state:
case hg
E : Type u_1
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℂ E
P : WeakFEPair E
inst✝ : CompleteSpace E
s : ℂ
hs : P.k < s.re
h_re1 : -1 < (s - 1).re
h_re2 : -1 < (s - ↑P.k - 1).re
⊢ Integrable (fun x => ↑x ^ (s - ↑P.k - 1)) (volume.restrict (Ioc 0 1))

Tactic:
rw [← IntegrableOn, ← intervalIntegrable_iff_integrableOn_Ioc_of_le zero_le_one]

Result:
case hg
E : Type u_1
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℂ E
P : WeakFEPair E
inst✝ : CompleteSpace E
s : ℂ
hs : P.k < s.re
h_re1 : -1 < (s - 1).re
h_re2 : -1 < (s - ↑P.k - 1).re
⊢ IntervalIntegrable (fun x => ↑x ^ (s - ↑P.k - 1)) volume 0 1

Proof state:
case hf.hf
E : Type u_1
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℂ E
P : WeakFEPair E
inst✝ : CompleteSpace E
s : ℂ
hs : P.k < s.re
h_re1 : -1 < (s - 1).re
h_re2 : -1 < (s - ↑P.k - 1).re
⊢ IntervalIntegrable (fun x => ↑x ^ (s - 1)) volume 0 1

Tactic:
exact intervalIntegral.intervalIntegrable_cpow' h_re1

Result:
no goals

Proof state:
E : Type u_1
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℂ E
P : WeakFEPair E
inst✝ : CompleteSpace E
s : ℂ
hs : P.k < s.re
h_re1 : -1 < (s - 1).re
h_re2 : -1 < (s - ↑P.k - 1).re
⊢ ∫ (x : ℝ) in Ioi 0,
      ↑x ^ (s - 1) •
        ((Ioo 0 1).indicator (fun t => P.f₀ - (P.ε * ↑(t ^ (-P.k))) • P.g₀) x +
          {1}.indicator (fun x => P.f₀ - P.f 1) x) =
    ∫ (x : ℝ) in Ioi 0, ↑x ^ (s - 1) • (Ioo 0 1).indicator (fun t => P.f₀ - (P.ε * ↑(t ^ (-P.k))) • P.g₀) x

Tactic:
refine setIntegral_congr_ae measurableSet_Ioi (eventually_of_mem (U := {1}ᶜ)
    (compl_mem_ae_iff.mpr (subsingleton_singleton.measure_zero _)) (fun x hx _ ↦ ?_))

Result:
E : Type u_1
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℂ E
P : WeakFEPair E
inst✝ : CompleteSpace E
s : ℂ
hs : P.k < s.re
h_re1 : -1 < (s - 1).re
h_re2 : -1 < (s - ↑P.k - 1).re
x : ℝ
hx : x ∈ {1}ᶜ
x✝ : x ∈ Ioi 0
⊢ ↑x ^ (s - 1) •
      ((Ioo 0 1).indicator (fun t => P.f₀ - (P.ε * ↑(t ^ (-P.k))) • P.g₀) x + {1}.indicator (fun x => P.f₀ - P.f 1) x) =
    ↑x ^ (s - 1) • (Ioo 0 1).indicator (fun t => P.f₀ - (P.ε * ↑(t ^ (-P.k))) • P.g₀) x