mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.NumberTheory.LSeries.MellinEqDirichlet

Goal state before:
pp: case inl
ι : Type u_1
inst✝ : Countable ι
a : ι → ℂ
q : ι → ℝ
F : ℝ → ℂ
s : ℂ
hq : ∀ (i : ι), a i = 0 ∨ 0 < q i
hs : 0 < s.re
hF : ∀ t ∈ Ioi 0, HasSum (fun i ↦ a i * ↑(rexp (-π * q i * t))) (F t)
h_sum : Summable fun i ↦ ‖a i‖ / q i ^ s.re
hp : ∀ (i : ι), a i = 0 ∨ 0 < π * q i
i : ι
h : a i = 0
⊢ ‖a i‖ / (π * q i) ^ s.re = π ^ (-s.re) * ‖a i‖ / q i ^ s.re

pp: case inr
ι : Type u_1
inst✝ : Countable ι
a : ι → ℂ
q : ι → ℝ
F : ℝ → ℂ
s : ℂ
hq : ∀ (i : ι), a i = 0 ∨ 0 < q i
hs : 0 < s.re
hF : ∀ t ∈ Ioi 0, HasSum (fun i ↦ a i * ↑(rexp (-π * q i * t))) (F t)
h_sum : Summable fun i ↦ ‖a i‖ / q i ^ s.re
hp : ∀ (i : ι), a i = 0 ∨ 0 < π * q i
i : ι
h : 0 < q i
⊢ ‖a i‖ / (π * q i) ^ s.re = π ^ (-s.re) * ‖a i‖ / q i ^ s.re

Tactic:
·

Goal state after:
case inl
ι : Type u_1
inst✝ : Countable ι
a : ι → ℂ
q : ι → ℝ
F : ℝ → ℂ
s : ℂ
hq : ∀ (i : ι), a i = 0 ∨ 0 < q i
hs : 0 < s.re
hF : ∀ t ∈ Ioi 0, HasSum (fun i ↦ a i * ↑(rexp (-π * q i * t))) (F t)
h_sum : Summable fun i ↦ ‖a i‖ / q i ^ s.re
hp : ∀ (i : ι), a i = 0 ∨ 0 < π * q i
i : ι
h : a i = 0
⊢ ‖a i‖ / (π * q i) ^ s.re = π ^ (-s.re) * ‖a i‖ / q i ^ s.re
Module: Mathlib.NumberTheory.ModularForms.JacobiTheta.TwoVariable

Goal state before:
pp: case mp
z τ : ℂ
⊢ (Summable fun x ↦ jacobiTheta₂'_term x z τ) → 0 < τ.im

pp: case mpr
z τ : ℂ
⊢ 0 < τ.im → Summable fun x ↦ jacobiTheta₂'_term x z τ

Tactic:
·

Goal state after:
case mp
z τ : ℂ
⊢ (Summable fun x ↦ jacobiTheta₂'_term x z τ) → 0 < τ.im
Module: Mathlib.NumberTheory.LSeries.MellinEqDirichlet

Goal state before:
pp: case inr
ι : Type u_1
inst✝ : Countable ι
a : ι → ℂ
q : ι → ℝ
F : ℝ → ℂ
s : ℂ
hq : ∀ (i : ι), a i = 0 ∨ 0 < q i
hs : 0 < s.re
hF : ∀ t ∈ Ioi 0, HasSum (fun i ↦ a i * ↑(rexp (-π * q i * t))) (F t)
h_sum : Summable fun i ↦ ‖a i‖ / q i ^ s.re
hp : ∀ (i : ι), a i = 0 ∨ 0 < π * q i
i : ι
h : 0 < q i
⊢ ‖a i‖ / (π * q i) ^ s.re = π ^ (-s.re) * ‖a i‖ / q i ^ s.re

Tactic:
·

Goal state after:
case inr
ι : Type u_1
inst✝ : Countable ι
a : ι → ℂ
q : ι → ℝ
F : ℝ → ℂ
s : ℂ
hq : ∀ (i : ι), a i = 0 ∨ 0 < q i
hs : 0 < s.re
hF : ∀ t ∈ Ioi 0, HasSum (fun i ↦ a i * ↑(rexp (-π * q i * t))) (F t)
h_sum : Summable fun i ↦ ‖a i‖ / q i ^ s.re
hp : ∀ (i : ι), a i = 0 ∨ 0 < π * q i
i : ι
h : 0 < q i
⊢ ‖a i‖ / (π * q i) ^ s.re = π ^ (-s.re) * ‖a i‖ / q i ^ s.re
Module: Mathlib.NumberTheory.LSeries.AbstractFuncEq

Goal state before:
pp: case inr.inl
E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℂ E
P : WeakFEPair E
hx : 0 < 1
⊢ (Ioi 1).indicator (fun x ↦ P.f x - P.f₀) 1 + (Ioo 0 1).indicator (fun x ↦ P.f x - (P.ε * ↑(x ^ (-P.k))) • P.g₀) 1 -
        P.f 1 +
      P.f₀ =
    (Ioo 0 1).indicator (fun x ↦ P.f₀ - (P.ε * ↑(x ^ (-P.k))) • P.g₀) 1 + {1}.indicator (fun x ↦ P.f₀ - P.f 1) 1

pp: case inr.inr
E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℂ E
P : WeakFEPair E
x : ℝ
hx : 0 < x
hx' : 1 < x
⊢ (Ioi 1).indicator (fun x ↦ P.f x - P.f₀) x + (Ioo 0 1).indicator (fun x ↦ P.f x - (P.ε * ↑(x ^ (-P.k))) • P.g₀) x -
        P.f x +
      P.f₀ =
    (Ioo 0 1).indicator (fun x ↦ P.f₀ - (P.ε * ↑(x ^ (-P.k))) • P.g₀) x + {1}.indicator (fun x ↦ P.f₀ - P.f 1) x

Tactic:
·

Goal state after:
case inr.inl
E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℂ E
P : WeakFEPair E
hx : 0 < 1
⊢ (Ioi 1).indicator (fun x ↦ P.f x - P.f₀) 1 + (Ioo 0 1).indicator (fun x ↦ P.f x - (P.ε * ↑(x ^ (-P.k))) • P.g₀) 1 -
        P.f 1 +
      P.f₀ =
    (Ioo 0 1).indicator (fun x ↦ P.f₀ - (P.ε * ↑(x ^ (-P.k))) • P.g₀) 1 + {1}.indicator (fun x ↦ P.f₀ - P.f 1) 1
Module: Mathlib.NumberTheory.LSeries.AbstractFuncEq

Goal state before:
pp: case inr.inr
E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℂ E
P : WeakFEPair E
x : ℝ
hx : 0 < x
hx' : 1 < x
⊢ (Ioi 1).indicator (fun x ↦ P.f x - P.f₀) x + (Ioo 0 1).indicator (fun x ↦ P.f x - (P.ε * ↑(x ^ (-P.k))) • P.g₀) x -
        P.f x +
      P.f₀ =
    (Ioo 0 1).indicator (fun x ↦ P.f₀ - (P.ε * ↑(x ^ (-P.k))) • P.g₀) x + {1}.indicator (fun x ↦ P.f₀ - P.f 1) x

Tactic:
·

Goal state after:
case inr.inr
E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℂ E
P : WeakFEPair E
x : ℝ
hx : 0 < x
hx' : 1 < x
⊢ (Ioi 1).indicator (fun x ↦ P.f x - P.f₀) x + (Ioo 0 1).indicator (fun x ↦ P.f x - (P.ε * ↑(x ^ (-P.k))) • P.g₀) x -
        P.f x +
      P.f₀ =
    (Ioo 0 1).indicator (fun x ↦ P.f₀ - (P.ε * ↑(x ^ (-P.k))) • P.g₀) x + {1}.indicator (fun x ↦ P.f₀ - P.f 1) x
Module: Mathlib.NumberTheory.ModularForms.JacobiTheta.Bounds

Goal state before:
pp: case inr.refine_2
a : ℝ
ha : 0 ≤ a
aux' : (fun t ↦ ((1 - rexp (-π * t)) ^ 2)⁻¹) =O[atTop] fun x ↦ 1
ha' : 0 < a
⊢ (fun t ↦ a * rexp (-π * a ^ 2 * t) / (1 - rexp (-π * t))) =O[atTop] fun t ↦ rexp (-(π * a ^ 2) * t)

Tactic:
·

Goal state after:
case inr.refine_2
a : ℝ
ha : 0 ≤ a
aux' : (fun t ↦ ((1 - rexp (-π * t)) ^ 2)⁻¹) =O[atTop] fun x ↦ 1
ha' : 0 < a
⊢ (fun t ↦ a * rexp (-π * a ^ 2 * t) / (1 - rexp (-π * t))) =O[atTop] fun t ↦ rexp (-(π * a ^ 2) * t)
Module: Mathlib.NumberTheory.ModularForms.JacobiTheta.TwoVariable

Goal state before:
pp: case mpr
z τ : ℂ
⊢ 0 < τ.im → Summable fun x ↦ jacobiTheta₂'_term x z τ

Tactic:
·

Goal state after:
case mpr
z τ : ℂ
⊢ 0 < τ.im → Summable fun x ↦ jacobiTheta₂'_term x z τ
Module: Mathlib.NumberTheory.ModularForms.JacobiTheta.Bounds

Goal state before:
pp: case ofNat
k : ℕ
a t : ℝ
ht : 0 < t
a✝ : ℕ
⊢ ‖f_int k a t (Int.ofNat a✝)‖ = ‖(fun t_1 ↦ Int.rec (f_nat k a t) (f_nat k (1 - a) t) t_1) (Int.ofNat a✝)‖

pp: case negSucc
k : ℕ
a t : ℝ
ht : 0 < t
m : ℕ
⊢ ‖f_int k a t (Int.negSucc m)‖ = ‖(fun t_1 ↦ Int.rec (f_nat k a t) (f_nat k (1 - a) t) t_1) (Int.negSucc m)‖

Tactic:
·

Goal state after:
case ofNat
k : ℕ
a t : ℝ
ht : 0 < t
a✝ : ℕ
⊢ ‖f_int k a t (Int.ofNat a✝)‖ = ‖(fun t_1 ↦ Int.rec (f_nat k a t) (f_nat k (1 - a) t) t_1) (Int.ofNat a✝)‖
Module: Mathlib.NumberTheory.ModularForms.JacobiTheta.Bounds

Goal state before:
pp: case negSucc
k : ℕ
a t : ℝ
ht : 0 < t
m : ℕ
⊢ ‖f_int k a t (Int.negSucc m)‖ = ‖(fun t_1 ↦ Int.rec (f_nat k a t) (f_nat k (1 - a) t) t_1) (Int.negSucc m)‖

Tactic:
·

Goal state after:
case negSucc
k : ℕ
a t : ℝ
ht : 0 < t
m : ℕ
⊢ ‖f_int k a t (Int.negSucc m)‖ = ‖(fun t_1 ↦ Int.rec (f_nat k a t) (f_nat k (1 - a) t) t_1) (Int.negSucc m)‖
Module: Mathlib.NumberTheory.ModularForms.JacobiTheta.Bounds

Goal state before:
pp: k : ℕ
a : UnitAddCircle
t b : ℝ
⊢ ∑' (n : ℤ), f_int k (b + 1) t n = ∑' (n : ℤ), f_int k b t n

Tactic:
← (Equiv.addRight (1 : ℤ)).tsum_eq (f := fun n ↦ f_int k b t n)

Goal state after:
k : ℕ
a : UnitAddCircle
t b : ℝ
⊢ ∑' (n : ℤ), f_int k (b + 1) t n = ∑' (c : ℤ), f_int k b t ((Equiv.addRight 1) c)
Module: Mathlib.NumberTheory.ModularForms.JacobiTheta.Bounds

Goal state before:
pp: case ofNat
k : ℕ
a : ℝ
ha : a ∈ Icc 0 1
t : ℝ
ht : 0 < t
a✝ : ℕ
⊢ f_int k a t (Int.ofNat a✝) = Int.rec (f_nat k a t) (f_nat k (1 - a) t) (Int.ofNat a✝)

pp: case negSucc
k : ℕ
a : ℝ
ha : a ∈ Icc 0 1
t : ℝ
ht : 0 < t
a✝ : ℕ
⊢ f_int k a t (Int.negSucc a✝) = Int.rec (f_nat k a t) (f_nat k (1 - a) t) (Int.negSucc a✝)

Tactic:
·

Goal state after:
case ofNat
k : ℕ
a : ℝ
ha : a ∈ Icc 0 1
t : ℝ
ht : 0 < t
a✝ : ℕ
⊢ f_int k a t (Int.ofNat a✝) = Int.rec (f_nat k a t) (f_nat k (1 - a) t) (Int.ofNat a✝)
Module: Mathlib.NumberTheory.ModularForms.JacobiTheta.Bounds

Goal state before:
pp: case negSucc
k : ℕ
a : ℝ
ha : a ∈ Icc 0 1
t : ℝ
ht : 0 < t
a✝ : ℕ
⊢ f_int k a t (Int.negSucc a✝) = Int.rec (f_nat k a t) (f_nat k (1 - a) t) (Int.negSucc a✝)

Tactic:
·

Goal state after:
case negSucc
k : ℕ
a : ℝ
ha : a ∈ Icc 0 1
t : ℝ
ht : 0 < t
a✝ : ℕ
⊢ f_int k a t (Int.negSucc a✝) = Int.rec (f_nat k a t) (f_nat k (1 - a) t) (Int.negSucc a✝)
Module: Mathlib.NumberTheory.LSeries.MellinEqDirichlet

Goal state before:
pp: ι : Type u_1
inst✝ : Countable ι
a : ι → ℂ
p : ι → ℝ
F : ℝ → ℂ
s : ℂ
hp : ∀ (i : ι), 0 ≤ p i
hs : 0 < s.re
h_sum : Summable fun i ↦ ‖a i‖ / p i ^ s.re
hs' : s ≠ 0
a' : ι → ℂ := fun i ↦ if p i = 0 then 0 else a i
hp' : ∀ (i : ι), a' i = 0 ∨ 0 < p i
this : ∀ (i : ι) (t : ℝ), (if p i = 0 then 0 else a i * ↑(rexp (-π * p i * t))) = a' i * ↑(rexp (-π * p i * t))
hF : ∀ t ∈ Ioi 0, HasSum (fun i ↦ a' i * ↑(rexp (-π * p i * t))) (F t)
i : ι
⊢ ↑π ^ (-s) * Complex.Gamma s * a i / ↑(p i) ^ s = ↑π ^ (-s) * Complex.Gamma s * a' i / ↑(p i) ^ s

pp: ι : Type u_1
inst✝ : Countable ι
a : ι → ℂ
p : ι → ℝ
F : ℝ → ℂ
s : ℂ
hp : ∀ (i : ι), 0 ≤ p i
hs : 0 < s.re
h_sum : Summable fun i ↦ ‖a i‖ / p i ^ s.re
hs' : s ≠ 0
a' : ι → ℂ := fun i ↦ if p i = 0 then 0 else a i
hp' : ∀ (i : ι), a' i = 0 ∨ 0 < p i
this : ∀ (i : ι) (t : ℝ), (if p i = 0 then 0 else a i * ↑(rexp (-π * p i * t))) = a' i * ↑(rexp (-π * p i * t))
hF : ∀ t ∈ Ioi 0, HasSum (fun i ↦ a' i * ↑(rexp (-π * p i * t))) (F t)
⊢ Summable fun i ↦ ‖a' i‖ / p i ^ s.re

Tactic:
·

Goal state after:
ι : Type u_1
inst✝ : Countable ι
a : ι → ℂ
p : ι → ℝ
F : ℝ → ℂ
s : ℂ
hp : ∀ (i : ι), 0 ≤ p i
hs : 0 < s.re
h_sum : Summable fun i ↦ ‖a i‖ / p i ^ s.re
hs' : s ≠ 0
a' : ι → ℂ := fun i ↦ if p i = 0 then 0 else a i
hp' : ∀ (i : ι), a' i = 0 ∨ 0 < p i
this : ∀ (i : ι) (t : ℝ), (if p i = 0 then 0 else a i * ↑(rexp (-π * p i * t))) = a' i * ↑(rexp (-π * p i * t))
hF : ∀ t ∈ Ioi 0, HasSum (fun i ↦ a' i * ↑(rexp (-π * p i * t))) (F t)
i : ι
⊢ ↑π ^ (-s) * Complex.Gamma s * a i / ↑(p i) ^ s = ↑π ^ (-s) * Complex.Gamma s * a' i / ↑(p i) ^ s
Module: Mathlib.NumberTheory.LSeries.MellinEqDirichlet

Goal state before:
pp: ι : Type u_1
inst✝ : Countable ι
a : ι → ℂ
p : ι → ℝ
F : ℝ → ℂ
s : ℂ
hp : ∀ (i : ι), 0 ≤ p i
hs : 0 < s.re
h_sum : Summable fun i ↦ ‖a i‖ / p i ^ s.re
hs' : s ≠ 0
a' : ι → ℂ := fun i ↦ if p i = 0 then 0 else a i
hp' : ∀ (i : ι), a' i = 0 ∨ 0 < p i
this : ∀ (i : ι) (t : ℝ), (if p i = 0 then 0 else a i * ↑(rexp (-π * p i * t))) = a' i * ↑(rexp (-π * p i * t))
hF : ∀ t ∈ Ioi 0, HasSum (fun i ↦ a' i * ↑(rexp (-π * p i * t))) (F t)
⊢ Summable fun i ↦ ‖a' i‖ / p i ^ s.re

Tactic:
·

Goal state after:
ι : Type u_1
inst✝ : Countable ι
a : ι → ℂ
p : ι → ℝ
F : ℝ → ℂ
s : ℂ
hp : ∀ (i : ι), 0 ≤ p i
hs : 0 < s.re
h_sum : Summable fun i ↦ ‖a i‖ / p i ^ s.re
hs' : s ≠ 0
a' : ι → ℂ := fun i ↦ if p i = 0 then 0 else a i
hp' : ∀ (i : ι), a' i = 0 ∨ 0 < p i
this : ∀ (i : ι) (t : ℝ), (if p i = 0 then 0 else a i * ↑(rexp (-π * p i * t))) = a' i * ↑(rexp (-π * p i * t))
hF : ∀ t ∈ Ioi 0, HasSum (fun i ↦ a' i * ↑(rexp (-π * p i * t))) (F t)
⊢ Summable fun i ↦ ‖a' i‖ / p i ^ s.re
Module: Mathlib.NumberTheory.LSeries.MellinEqDirichlet

Goal state before:
pp: case pos
ι : Type u_1
inst✝ : Countable ι
a : ι → ℂ
p : ι → ℝ
F : ℝ → ℂ
s : ℂ
hp : ∀ (i : ι), 0 ≤ p i
hs : 0 < s.re
h_sum : Summable fun i ↦ ‖a i‖ / p i ^ s.re
hs' : s ≠ 0
a' : ι → ℂ := fun i ↦ if p i = 0 then 0 else a i
hp' : ∀ (i : ι), a' i = 0 ∨ 0 < p i
this : ∀ (i : ι) (t : ℝ), (if p i = 0 then 0 else a i * ↑(rexp (-π * p i * t))) = a' i * ↑(rexp (-π * p i * t))
hF : ∀ t ∈ Ioi 0, HasSum (fun i ↦ a' i * ↑(rexp (-π * p i * t))) (F t)
i : ι
h✝ : p i = 0
⊢ ‖‖0‖ / p i ^ s.re‖ ≤ ‖a i‖ / p i ^ s.re

pp: case neg
ι : Type u_1
inst✝ : Countable ι
a : ι → ℂ
p : ι → ℝ
F : ℝ → ℂ
s : ℂ
hp : ∀ (i : ι), 0 ≤ p i
hs : 0 < s.re
h_sum : Summable fun i ↦ ‖a i‖ / p i ^ s.re
hs' : s ≠ 0
a' : ι → ℂ := fun i ↦ if p i = 0 then 0 else a i
hp' : ∀ (i : ι), a' i = 0 ∨ 0 < p i
this : ∀ (i : ι) (t : ℝ), (if p i = 0 then 0 else a i * ↑(rexp (-π * p i * t))) = a' i * ↑(rexp (-π * p i * t))
hF : ∀ t ∈ Ioi 0, HasSum (fun i ↦ a' i * ↑(rexp (-π * p i * t))) (F t)
i : ι
h✝ : ¬p i = 0
⊢ ‖‖a i‖ / p i ^ s.re‖ ≤ ‖a i‖ / p i ^ s.re

Tactic:
·

Goal state after:
case pos
ι : Type u_1
inst✝ : Countable ι
a : ι → ℂ
p : ι → ℝ
F : ℝ → ℂ
s : ℂ
hp : ∀ (i : ι), 0 ≤ p i
hs : 0 < s.re
h_sum : Summable fun i ↦ ‖a i‖ / p i ^ s.re
hs' : s ≠ 0
a' : ι → ℂ := fun i ↦ if p i = 0 then 0 else a i
hp' : ∀ (i : ι), a' i = 0 ∨ 0 < p i
this : ∀ (i : ι) (t : ℝ), (if p i = 0 then 0 else a i * ↑(rexp (-π * p i * t))) = a' i * ↑(rexp (-π * p i * t))
hF : ∀ t ∈ Ioi 0, HasSum (fun i ↦ a' i * ↑(rexp (-π * p i * t))) (F t)
i : ι
h✝ : p i = 0
⊢ ‖‖0‖ / p i ^ s.re‖ ≤ ‖a i‖ / p i ^ s.re
Module: Mathlib.NumberTheory.LSeries.MellinEqDirichlet

Goal state before:
pp: case neg
ι : Type u_1
inst✝ : Countable ι
a : ι → ℂ
p : ι → ℝ
F : ℝ → ℂ
s : ℂ
hp : ∀ (i : ι), 0 ≤ p i
hs : 0 < s.re
h_sum : Summable fun i ↦ ‖a i‖ / p i ^ s.re
hs' : s ≠ 0
a' : ι → ℂ := fun i ↦ if p i = 0 then 0 else a i
hp' : ∀ (i : ι), a' i = 0 ∨ 0 < p i
this : ∀ (i : ι) (t : ℝ), (if p i = 0 then 0 else a i * ↑(rexp (-π * p i * t))) = a' i * ↑(rexp (-π * p i * t))
hF : ∀ t ∈ Ioi 0, HasSum (fun i ↦ a' i * ↑(rexp (-π * p i * t))) (F t)
i : ι
h✝ : ¬p i = 0
⊢ ‖‖a i‖ / p i ^ s.re‖ ≤ ‖a i‖ / p i ^ s.re

Tactic:
·

Goal state after:
case neg
ι : Type u_1
inst✝ : Countable ι
a : ι → ℂ
p : ι → ℝ
F : ℝ → ℂ
s : ℂ
hp : ∀ (i : ι), 0 ≤ p i
hs : 0 < s.re
h_sum : Summable fun i ↦ ‖a i‖ / p i ^ s.re
hs' : s ≠ 0
a' : ι → ℂ := fun i ↦ if p i = 0 then 0 else a i
hp' : ∀ (i : ι), a' i = 0 ∨ 0 < p i
this : ∀ (i : ι) (t : ℝ), (if p i = 0 then 0 else a i * ↑(rexp (-π * p i * t))) = a' i * ↑(rexp (-π * p i * t))
hF : ∀ t ∈ Ioi 0, HasSum (fun i ↦ a' i * ↑(rexp (-π * p i * t))) (F t)
i : ι
h✝ : ¬p i = 0
⊢ ‖‖a i‖ / p i ^ s.re‖ ≤ ‖a i‖ / p i ^ s.re
Module: Mathlib.NumberTheory.LSeries.AbstractFuncEq

Goal state before:
pp: case 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
⊢ Integrable (fun x ↦ ↑x ^ (s - 1) • P.f₀) (volume.restrict (Ioc 0 1))

pp: 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 ↦ P.ε • ↑x ^ (s - ↑P.k - 1) • P.g₀) (volume.restrict (Ioc 0 1))

Tactic:
·

Goal state after:
case 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
⊢ Integrable (fun x ↦ ↑x ^ (s - 1) • P.f₀) (volume.restrict (Ioc 0 1))
Module: Mathlib.NumberTheory.LSeries.AbstractFuncEq

Goal state before:
pp: 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 ↦ P.ε • ↑x ^ (s - ↑P.k - 1) • P.g₀) (volume.restrict (Ioc 0 1))

Tactic:
·

Goal state after:
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 ↦ P.ε • ↑x ^ (s - ↑P.k - 1) • P.g₀) (volume.restrict (Ioc 0 1))
Module: Mathlib.NumberTheory.LSeries.AbstractFuncEq

Goal state before:
pp: 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 0..1, ↑x ^ (s - 1)) * 1 = 1 / s * 1

pp: 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
⊢ -(P.ε * ((∫ (x : ℝ) in 0..1, ↑x ^ (s - ↑P.k - 1)) * 1)) = P.ε / (↑P.k - s) * 1

Tactic:
·

Goal state after:
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 0..1, ↑x ^ (s - 1)) * 1 = 1 / s * 1
Module: Mathlib.NumberTheory.LSeries.AbstractFuncEq

Goal state before:
pp: 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
⊢ -(P.ε * ((∫ (x : ℝ) in 0..1, ↑x ^ (s - ↑P.k - 1)) * 1)) = P.ε / (↑P.k - s) * 1

Tactic:
·

Goal state after:
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
⊢ -(P.ε * ((∫ (x : ℝ) in 0..1, ↑x ^ (s - ↑P.k - 1)) * 1)) = P.ε / (↑P.k - s) * 1
Module: Mathlib.NumberTheory.LSeries.MellinEqDirichlet

Goal state before:
pp: case e'_5
ι : Type u_1
inst✝ : Countable ι
a : ι → ℂ
r : ι → ℝ
F : ℝ → ℂ
s : ℂ
hs : 0 < s.re
h_sum : Summable fun i ↦ ‖a i‖ / |r i| ^ s.re
hs' : 0 < (s / 2).re
hF : ∀ t ∈ Ioi 0, HasSum (fun i ↦ if r i ^ 2 = 0 then 0 else a i * ↑(rexp (-π * r i ^ 2 * t))) (F t)
i : ι
⊢ s.Gammaℝ * a i = ↑π ^ (-(s / 2)) * Complex.Gamma (s / 2) * a i

pp: case e'_6
ι : Type u_1
inst✝ : Countable ι
a : ι → ℂ
r : ι → ℝ
F : ℝ → ℂ
s : ℂ
hs : 0 < s.re
h_sum : Summable fun i ↦ ‖a i‖ / |r i| ^ s.re
hs' : 0 < (s / 2).re
hF : ∀ t ∈ Ioi 0, HasSum (fun i ↦ if r i ^ 2 = 0 then 0 else a i * ↑(rexp (-π * r i ^ 2 * t))) (F t)
i : ι
⊢ ↑|r i| ^ s = ↑(r i ^ 2) ^ (s / 2)

pp: ι : Type u_1
inst✝ : Countable ι
a : ι → ℂ
r : ι → ℝ
F : ℝ → ℂ
s : ℂ
hs : 0 < s.re
h_sum : Summable fun i ↦ ‖a i‖ / |r i| ^ s.re
hs' : 0 < (s / 2).re
hF : ∀ t ∈ Ioi 0, HasSum (fun i ↦ if r i ^ 2 = 0 then 0 else a i * ↑(rexp (-π * r i ^ 2 * t))) (F t)
⊢ Summable fun i ↦ ‖a i‖ / (r i ^ 2) ^ (s / 2).re

Tactic:
·

Goal state after:
case e'_5
ι : Type u_1
inst✝ : Countable ι
a : ι → ℂ
r : ι → ℝ
F : ℝ → ℂ
s : ℂ
hs : 0 < s.re
h_sum : Summable fun i ↦ ‖a i‖ / |r i| ^ s.re
hs' : 0 < (s / 2).re
hF : ∀ t ∈ Ioi 0, HasSum (fun i ↦ if r i ^ 2 = 0 then 0 else a i * ↑(rexp (-π * r i ^ 2 * t))) (F t)
i : ι
⊢ s.Gammaℝ * a i = ↑π ^ (-(s / 2)) * Complex.Gamma (s / 2) * a i
Module: Mathlib.NumberTheory.LSeries.MellinEqDirichlet

Goal state before:
pp: case e'_6
ι : Type u_1
inst✝ : Countable ι
a : ι → ℂ
r : ι → ℝ
F : ℝ → ℂ
s : ℂ
hs : 0 < s.re
h_sum : Summable fun i ↦ ‖a i‖ / |r i| ^ s.re
hs' : 0 < (s / 2).re
hF : ∀ t ∈ Ioi 0, HasSum (fun i ↦ if r i ^ 2 = 0 then 0 else a i * ↑(rexp (-π * r i ^ 2 * t))) (F t)
i : ι
⊢ ↑|r i| ^ s = ↑(r i ^ 2) ^ (s / 2)

pp: ι : Type u_1
inst✝ : Countable ι
a : ι → ℂ
r : ι → ℝ
F : ℝ → ℂ
s : ℂ
hs : 0 < s.re
h_sum : Summable fun i ↦ ‖a i‖ / |r i| ^ s.re
hs' : 0 < (s / 2).re
hF : ∀ t ∈ Ioi 0, HasSum (fun i ↦ if r i ^ 2 = 0 then 0 else a i * ↑(rexp (-π * r i ^ 2 * t))) (F t)
⊢ Summable fun i ↦ ‖a i‖ / (r i ^ 2) ^ (s / 2).re

Tactic:
·

Goal state after:
case e'_6
ι : Type u_1
inst✝ : Countable ι
a : ι → ℂ
r : ι → ℝ
F : ℝ → ℂ
s : ℂ
hs : 0 < s.re
h_sum : Summable fun i ↦ ‖a i‖ / |r i| ^ s.re
hs' : 0 < (s / 2).re
hF : ∀ t ∈ Ioi 0, HasSum (fun i ↦ if r i ^ 2 = 0 then 0 else a i * ↑(rexp (-π * r i ^ 2 * t))) (F t)
i : ι
⊢ ↑|r i| ^ s = ↑(r i ^ 2) ^ (s / 2)
Module: Mathlib.NumberTheory.LSeries.AbstractFuncEq

Goal state before:
pp: case refine_1
E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℂ E
P : WeakFEPair E
s : ℂ
hs : s ≠ 0 ∨ P.f₀ = 0
hs' : s ≠ ↑P.k ∨ P.g₀ = 0
⊢ DifferentiableAt ℂ (fun s ↦ (1 / s) • P.f₀) s

pp: case refine_2
E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℂ E
P : WeakFEPair E
s : ℂ
hs : s ≠ 0 ∨ P.f₀ = 0
hs' : s ≠ ↑P.k ∨ P.g₀ = 0
⊢ DifferentiableAt ℂ (fun s ↦ (P.ε / (↑P.k - s)) • P.g₀) s

Tactic:
·

Goal state after:
case refine_1
E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℂ E
P : WeakFEPair E
s : ℂ
hs : s ≠ 0 ∨ P.f₀ = 0
hs' : s ≠ ↑P.k ∨ P.g₀ = 0
⊢ DifferentiableAt ℂ (fun s ↦ (1 / s) • P.f₀) s
Module: Mathlib.NumberTheory.LSeries.AbstractFuncEq

Goal state before:
pp: case refine_1.inl
E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℂ E
P : WeakFEPair E
s : ℂ
hs' : s ≠ ↑P.k ∨ P.g₀ = 0
hs : s ≠ 0
⊢ DifferentiableAt ℂ (fun s ↦ (1 / s) • P.f₀) s

pp: case refine_1.inr
E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℂ E
P : WeakFEPair E
s : ℂ
hs' : s ≠ ↑P.k ∨ P.g₀ = 0
hs : P.f₀ = 0
⊢ DifferentiableAt ℂ (fun s ↦ (1 / s) • P.f₀) s

Tactic:
·

Goal state after:
case refine_1.inl
E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℂ E
P : WeakFEPair E
s : ℂ
hs' : s ≠ ↑P.k ∨ P.g₀ = 0
hs : s ≠ 0
⊢ DifferentiableAt ℂ (fun s ↦ (1 / s) • P.f₀) s
Module: Mathlib.NumberTheory.LSeries.HurwitzZetaEven

Goal state before:
pp: case inl
a : UnitAddCircle
x : ℝ
hx : x ≤ 0
⊢ evenKernel a x = 1 / x ^ (1 / 2) * cosKernel a (1 / x)

pp: case inr
a : UnitAddCircle
x : ℝ
hx : 0 < x
⊢ evenKernel a x = 1 / x ^ (1 / 2) * cosKernel a (1 / x)

Tactic:
·

Goal state after:
case inl
a : UnitAddCircle
x : ℝ
hx : x ≤ 0
⊢ evenKernel a x = 1 / x ^ (1 / 2) * cosKernel a (1 / x)
Module: Mathlib.NumberTheory.LSeries.AbstractFuncEq

Goal state before:
pp: case refine_1.inr
E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℂ E
P : WeakFEPair E
s : ℂ
hs' : s ≠ ↑P.k ∨ P.g₀ = 0
hs : P.f₀ = 0
⊢ DifferentiableAt ℂ (fun s ↦ (1 / s) • P.f₀) s

Tactic:
·

Goal state after:
case refine_1.inr
E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℂ E
P : WeakFEPair E
s : ℂ
hs' : s ≠ ↑P.k ∨ P.g₀ = 0
hs : P.f₀ = 0
⊢ DifferentiableAt ℂ (fun s ↦ (1 / s) • P.f₀) s
Module: Mathlib.NumberTheory.LSeries.AbstractFuncEq

Goal state before:
pp: case refine_2
E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℂ E
P : WeakFEPair E
s : ℂ
hs : s ≠ 0 ∨ P.f₀ = 0
hs' : s ≠ ↑P.k ∨ P.g₀ = 0
⊢ DifferentiableAt ℂ (fun s ↦ (P.ε / (↑P.k - s)) • P.g₀) s

Tactic:
·

Goal state after:
case refine_2
E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℂ E
P : WeakFEPair E
s : ℂ
hs : s ≠ 0 ∨ P.f₀ = 0
hs' : s ≠ ↑P.k ∨ P.g₀ = 0
⊢ DifferentiableAt ℂ (fun s ↦ (P.ε / (↑P.k - s)) • P.g₀) s
Module: Mathlib.NumberTheory.LSeries.AbstractFuncEq

Goal state before:
pp: case refine_2.inl
E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℂ E
P : WeakFEPair E
s : ℂ
hs : s ≠ 0 ∨ P.f₀ = 0
hs' : s ≠ ↑P.k
⊢ DifferentiableAt ℂ (fun s ↦ (P.ε / (↑P.k - s)) • P.g₀) s

pp: case refine_2.inr
E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℂ E
P : WeakFEPair E
s : ℂ
hs : s ≠ 0 ∨ P.f₀ = 0
hs' : P.g₀ = 0
⊢ DifferentiableAt ℂ (fun s ↦ (P.ε / (↑P.k - s)) • P.g₀) s

Tactic:
·

Goal state after:
case refine_2.inl
E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℂ E
P : WeakFEPair E
s : ℂ
hs : s ≠ 0 ∨ P.f₀ = 0
hs' : s ≠ ↑P.k
⊢ DifferentiableAt ℂ (fun s ↦ (P.ε / (↑P.k - s)) • P.g₀) s
Module: Mathlib.NumberTheory.LSeries.AbstractFuncEq

Goal state before:
pp: case refine_2.inr
E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℂ E
P : WeakFEPair E
s : ℂ
hs : s ≠ 0 ∨ P.f₀ = 0
hs' : P.g₀ = 0
⊢ DifferentiableAt ℂ (fun s ↦ (P.ε / (↑P.k - s)) • P.g₀) s

Tactic:
·

Goal state after:
case refine_2.inr
E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℂ E
P : WeakFEPair E
s : ℂ
hs : s ≠ 0 ∨ P.f₀ = 0
hs' : P.g₀ = 0
⊢ DifferentiableAt ℂ (fun s ↦ (P.ε / (↑P.k - s)) • P.g₀) s
Module: Mathlib.NumberTheory.LSeries.MellinEqDirichlet

Goal state before:
pp: case e'_6
ι : Type u_1
inst✝ : Countable ι
a : ι → ℂ
r : ι → ℝ
F : ℝ → ℂ
s : ℂ
hs : 0 < s.re
h_sum : Summable fun i ↦ ‖a i‖ / |r i| ^ s.re
hs' : 0 < (s / 2).re
hF : ∀ t ∈ Ioi 0, HasSum (fun i ↦ if r i ^ 2 = 0 then 0 else a i * ↑(rexp (-π * r i ^ 2 * t))) (F t)
i : ι
⊢ ↑|r i| ^ s = ↑|r i| ^ (↑2 * (s / 2))

pp: case e'_6.hlt
ι : Type u_1
inst✝ : Countable ι
a : ι → ℂ
r : ι → ℝ
F : ℝ → ℂ
s : ℂ
hs : 0 < s.re
h_sum : Summable fun i ↦ ‖a i‖ / |r i| ^ s.re
hs' : 0 < (s / 2).re
hF : ∀ t ∈ Ioi 0, HasSum (fun i ↦ if r i ^ 2 = 0 then 0 else a i * ↑(rexp (-π * r i ^ 2 * t))) (F t)
i : ι
⊢ -π < ↑2 * (↑|r i|).arg

pp: case e'_6.hle
ι : Type u_1
inst✝ : Countable ι
a : ι → ℂ
r : ι → ℝ
F : ℝ → ℂ
s : ℂ
hs : 0 < s.re
h_sum : Summable fun i ↦ ‖a i‖ / |r i| ^ s.re
hs' : 0 < (s / 2).re
hF : ∀ t ∈ Ioi 0, HasSum (fun i ↦ if r i ^ 2 = 0 then 0 else a i * ↑(rexp (-π * r i ^ 2 * t))) (F t)
i : ι
⊢ ↑2 * (↑|r i|).arg ≤ π

Tactic:
·

Goal state after:
case e'_6
ι : Type u_1
inst✝ : Countable ι
a : ι → ℂ
r : ι → ℝ
F : ℝ → ℂ
s : ℂ
hs : 0 < s.re
h_sum : Summable fun i ↦ ‖a i‖ / |r i| ^ s.re
hs' : 0 < (s / 2).re
hF : ∀ t ∈ Ioi 0, HasSum (fun i ↦ if r i ^ 2 = 0 then 0 else a i * ↑(rexp (-π * r i ^ 2 * t))) (F t)
i : ι
⊢ ↑|r i| ^ s = ↑|r i| ^ (↑2 * (s / 2))