-- Mathlib/NumberTheory/LSeries/Dirichlet.lean
/-- The L-series of a Dirichlet character mod `N > 0` does not converge absolutely at `s = 1`. -/
lemma not_LSeriesSummable_at_one {N : ℕ} (hN : N ≠ 0) (χ : DirichletCharacter ℂ N) :
    ¬ LSeriesSummable ↗χ 1

Proof state:
N : ℕ
hN : N ≠ 0
χ : DirichletCharacter ℂ N
h : LSeriesSummable (fun n => χ ↑n) 1
n : ℕ
⊢ (if ↑n = 1 then 1 / ↑n else 0) ≤ if n = 0 then 0 else ‖χ ↑n‖ / ↑n ^ re 1

Tactic:
split_ifs with h₁ h₂

Result:
case pos
N : ℕ
hN : N ≠ 0
χ : DirichletCharacter ℂ N
h : LSeriesSummable (fun n => χ ↑n) 1
n : ℕ
h₁ : ↑n = 1
h₂ : n = 0
⊢ 1 / ↑n ≤ 0

case neg
N : ℕ
hN : N ≠ 0
χ : DirichletCharacter ℂ N
h : LSeriesSummable (fun n => χ ↑n) 1
n : ℕ
h₁ : ↑n = 1
h₂ : ¬n = 0
⊢ 1 / ↑n ≤ ‖χ ↑n‖ / ↑n ^ re 1

case pos
N : ℕ
hN : N ≠ 0
χ : DirichletCharacter ℂ N
h : LSeriesSummable (fun n => χ ↑n) 1
n : ℕ
h₁ : ¬↑n = 1
h✝ : n = 0
⊢ 0 ≤ 0

case neg
N : ℕ
hN : N ≠ 0
χ : DirichletCharacter ℂ N
h : LSeriesSummable (fun n => χ ↑n) 1
n : ℕ
h₁ : ¬↑n = 1
h✝ : ¬n = 0
⊢ 0 ≤ ‖χ ↑n‖ / ↑n ^ re 1

Proof state:
N : ℕ
hN : N ≠ 0
χ : DirichletCharacter ℂ N
⊢ ¬LSeriesSummable (fun n => χ ↑n) 1

Tactic:
refine fun h ↦ (Real.not_summable_indicator_one_div_natCast hN 1) ?_

Result:
N : ℕ
hN : N ≠ 0
χ : DirichletCharacter ℂ N
h : LSeriesSummable (fun n => χ ↑n) 1
⊢ Summable ({n | ↑n = 1}.indicator fun n => 1 / ↑n)

Proof state:
case neg
N : ℕ
hN : N ≠ 0
χ : DirichletCharacter ℂ N
h : LSeriesSummable (fun n => χ ↑n) 1
n : ℕ
h₁ : ↑n = 1
h₂ : ¬n = 0
⊢ 1 / ↑n ≤ ‖χ ↑n‖ / ↑n ^ re 1

Tactic:
simp [h₁, χ.map_one]

Result:
no goals

Proof state:
case neg
N : ℕ
hN : N ≠ 0
χ : DirichletCharacter ℂ N
h : LSeriesSummable (fun n => χ ↑n) 1
n : ℕ
h₁ : ¬↑n = 1
h✝ : ¬n = 0
⊢ 0 ≤ ‖χ ↑n‖ / ↑n ^ re 1

Tactic:
positivity

Result:
no goals

Proof state:
N : ℕ
hN : N ≠ 0
χ : DirichletCharacter ℂ N
h : LSeriesSummable (fun n => χ ↑n) 1
m : ℕ
x✝ : m ∈ {n | ↑n = 1}
⊢ 0 ≤ 1 / ↑m

Tactic:
positivity

Result:
no goals

Proof state:
N : ℕ
hN : N ≠ 0
χ : DirichletCharacter ℂ N
h : LSeriesSummable (fun n => χ ↑n) 1
⊢ Summable ({n | ↑n = 1}.indicator fun n => 1 / ↑n)

Tactic:
refine h.norm.of_nonneg_of_le (fun m ↦ Set.indicator_apply_nonneg (fun _ ↦ by positivity))
  (fun n ↦ ?_)

Result:
N : ℕ
hN : N ≠ 0
χ : DirichletCharacter ℂ N
h : LSeriesSummable (fun n => χ ↑n) 1
n : ℕ
⊢ {n | ↑n = 1}.indicator (fun n => 1 / ↑n) n ≤ ‖term (fun n => χ ↑n) 1 n‖

Proof state:
case pos
N : ℕ
hN : N ≠ 0
χ : DirichletCharacter ℂ N
h : LSeriesSummable (fun n => χ ↑n) 1
n : ℕ
h₁ : ↑n = 1
h₂ : n = 0
⊢ 1 / ↑n ≤ 0

Tactic:
simp [h₂]

Result:
no goals

Proof state:
N : ℕ
hN : N ≠ 0
χ : DirichletCharacter ℂ N
h : LSeriesSummable (fun n => χ ↑n) 1
n : ℕ
⊢ {n | ↑n = 1}.indicator (fun n => 1 / ↑n) n ≤ ‖term (fun n => χ ↑n) 1 n‖

Tactic:
simp only [norm_term_eq, Set.indicator, Set.mem_setOf_eq]

Result:
N : ℕ
hN : N ≠ 0
χ : DirichletCharacter ℂ N
h : LSeriesSummable (fun n => χ ↑n) 1
n : ℕ
⊢ (if ↑n = 1 then 1 / ↑n else 0) ≤ if n = 0 then 0 else ‖χ ↑n‖ / ↑n ^ re 1

Proof state:
case pos
N : ℕ
hN : N ≠ 0
χ : DirichletCharacter ℂ N
h : LSeriesSummable (fun n => χ ↑n) 1
n : ℕ
h₁ : ¬↑n = 1
h✝ : n = 0
⊢ 0 ≤ 0

case neg
N : ℕ
hN : N ≠ 0
χ : DirichletCharacter ℂ N
h : LSeriesSummable (fun n => χ ↑n) 1
n : ℕ
h₁ : ¬↑n = 1
h✝ : ¬n = 0
⊢ 0 ≤ ‖χ ↑n‖ / ↑n ^ re 1

Tactic:
all_goals positivity

Result:
no goals