Theorem: re_log_comb_nonneg_dirichlet (EulerProducts/PNT.lean)

State before:
N : ℕ
χ : DirichletCharacter ℂ N
n : ℕ
hn : 2 ≤ n
x y : ℝ
hx : 1 < x
⊢ 0 ≤
    3 * (-(1 - 1 ↑n * ↑n ^ (-↑x)).log).re + 4 * (-(1 - χ ↑n * ↑n ^ (-(↑x + I * ↑y))).log).re +
      (-(1 - χ ↑n ^ 2 * ↑n ^ (-(↑x + 2 * I * ↑y))).log).re
Tactic:
by_cases hn' : IsUnit (n : ZMod N)
State after:
case pos
N : ℕ
χ : DirichletCharacter ℂ N
n : ℕ
hn : 2 ≤ n
x y : ℝ
hx : 1 < x
hn' : IsUnit ↑n
⊢ 0 ≤
    3 * (-(1 - 1 ↑n * ↑n ^ (-↑x)).log).re + 4 * (-(1 - χ ↑n * ↑n ^ (-(↑x + I * ↑y))).log).re +
      (-(1 - χ ↑n ^ 2 * ↑n ^ (-(↑x + 2 * I * ↑y))).log).re

case neg
N : ℕ
χ : DirichletCharacter ℂ N
n : ℕ
hn : 2 ≤ n
x y : ℝ
hx : 1 < x
hn' : ¬IsUnit ↑n
⊢ 0 ≤
    3 * (-(1 - 1 ↑n * ↑n ^ (-↑x)).log).re + 4 * (-(1 - χ ↑n * ↑n ^ (-(↑x + I * ↑y))).log).re +
      (-(1 - χ ↑n ^ 2 * ↑n ^ (-(↑x + 2 * I * ↑y))).log).re

State before:
case pos
N : ℕ
χ : DirichletCharacter ℂ N
n : ℕ
hn : 2 ≤ n
x y : ℝ
hx : 1 < x
hn' : IsUnit ↑n
⊢ 0 ≤
    3 * (-(1 - 1 ↑n * ↑n ^ (-↑x)).log).re + 4 * (-(1 - χ ↑n * ↑n ^ (-(↑x + I * ↑y))).log).re +
      (-(1 - χ ↑n ^ 2 * ↑n ^ (-(↑x + 2 * I * ↑y))).log).re
Tactic:
have ha₀ : 0 ≤ (n : ℝ) ^ (-x) := Real.rpow_nonneg n.cast_nonneg _
State after:
case pos
N : ℕ
χ : DirichletCharacter ℂ N
n : ℕ
hn : 2 ≤ n
x y : ℝ
hx : 1 < x
hn' : IsUnit ↑n
ha₀ : 0 ≤ ↑n ^ (-x)
⊢ 0 ≤
    3 * (-(1 - 1 ↑n * ↑n ^ (-↑x)).log).re + 4 * (-(1 - χ ↑n * ↑n ^ (-(↑x + I * ↑y))).log).re +
      (-(1 - χ ↑n ^ 2 * ↑n ^ (-(↑x + 2 * I * ↑y))).log).re

State before:
case pos
N : ℕ
χ : DirichletCharacter ℂ N
n : ℕ
hn : 2 ≤ n
x y : ℝ
hx : 1 < x
hn' : IsUnit ↑n
ha₀ : 0 ≤ ↑n ^ (-x)
⊢ 0 ≤
    3 * (-(1 - 1 ↑n * ↑n ^ (-↑x)).log).re + 4 * (-(1 - χ ↑n * ↑n ^ (-(↑x + I * ↑y))).log).re +
      (-(1 - χ ↑n ^ 2 * ↑n ^ (-(↑x + 2 * I * ↑y))).log).re
Tactic:
have ha₁ : (n : ℝ) ^ (-x) < 1 := by
  simpa only [Real.rpow_lt_one_iff n.cast_nonneg, Nat.cast_eq_zero, Nat.one_lt_cast,
    Left.neg_neg_iff, Nat.cast_lt_one, Left.neg_pos_iff]
    using Or.inr <| Or.inl ⟨hn, zero_lt_one.trans hx⟩
State after:
case pos
N : ℕ
χ : DirichletCharacter ℂ N
n : ℕ
hn : 2 ≤ n
x y : ℝ
hx : 1 < x
hn' : IsUnit ↑n
ha₀ : 0 ≤ ↑n ^ (-x)
ha₁ : ↑n ^ (-x) < 1
⊢ 0 ≤
    3 * (-(1 - 1 ↑n * ↑n ^ (-↑x)).log).re + 4 * (-(1 - χ ↑n * ↑n ^ (-(↑x + I * ↑y))).log).re +
      (-(1 - χ ↑n ^ 2 * ↑n ^ (-(↑x + 2 * I * ↑y))).log).re

State before:
case pos
N : ℕ
χ : DirichletCharacter ℂ N
n : ℕ
hn : 2 ≤ n
x y : ℝ
hx : 1 < x
hn' : IsUnit ↑n
ha₀ : 0 ≤ ↑n ^ (-x)
ha₁ : ↑n ^ (-x) < 1
⊢ 0 ≤
    3 * (-(1 - 1 ↑n * ↑n ^ (-↑x)).log).re + 4 * (-(1 - χ ↑n * ↑n ^ (-(↑x + I * ↑y))).log).re +
      (-(1 - χ ↑n ^ 2 * ↑n ^ (-(↑x + 2 * I * ↑y))).log).re
Tactic:
have hz : ‖χ n * (n : ℂ) ^ (-(I * y))‖ = 1 := by
  rw [norm_mul, ← hn'.unit_spec, DirichletCharacter.unit_norm_eq_one χ hn'.unit, one_mul,
    norm_eq_abs, abs_cpow_of_imp fun h ↦ False.elim <| by linarith [Nat.cast_eq_zero.mp h, hn]]
  simp
State after:
case pos
N : ℕ
χ : DirichletCharacter ℂ N
n : ℕ
hn : 2 ≤ n
x y : ℝ
hx : 1 < x
hn' : IsUnit ↑n
ha₀ : 0 ≤ ↑n ^ (-x)
ha₁ : ↑n ^ (-x) < 1
hz : ‖χ ↑n * ↑n ^ (-(I * ↑y))‖ = 1
⊢ 0 ≤
    3 * (-(1 - 1 ↑n * ↑n ^ (-↑x)).log).re + 4 * (-(1 - χ ↑n * ↑n ^ (-(↑x + I * ↑y))).log).re +
      (-(1 - χ ↑n ^ 2 * ↑n ^ (-(↑x + 2 * I * ↑y))).log).re

State before:
case pos
N : ℕ
χ : DirichletCharacter ℂ N
n : ℕ
hn : 2 ≤ n
x y : ℝ
hx : 1 < x
hn' : IsUnit ↑n
ha₀ : 0 ≤ ↑n ^ (-x)
ha₁ : ↑n ^ (-x) < 1
hz : ‖χ ↑n * ↑n ^ (-(I * ↑y))‖ = 1
⊢ 0 ≤
    3 * (-(1 - 1 ↑n * ↑n ^ (-↑x)).log).re + 4 * (-(1 - χ ↑n * ↑n ^ (-(↑x + I * ↑y))).log).re +
      (-(1 - χ ↑n ^ 2 * ↑n ^ (-(↑x + 2 * I * ↑y))).log).re
Tactic:
rw [MulChar.one_apply hn', one_mul]
State after:
case pos
N : ℕ
χ : DirichletCharacter ℂ N
n : ℕ
hn : 2 ≤ n
x y : ℝ
hx : 1 < x
hn' : IsUnit ↑n
ha₀ : 0 ≤ ↑n ^ (-x)
ha₁ : ↑n ^ (-x) < 1
hz : ‖χ ↑n * ↑n ^ (-(I * ↑y))‖ = 1
⊢ 0 ≤
    3 * (-(1 - ↑n ^ (-↑x)).log).re + 4 * (-(1 - χ ↑n * ↑n ^ (-(↑x + I * ↑y))).log).re +
      (-(1 - χ ↑n ^ 2 * ↑n ^ (-(↑x + 2 * I * ↑y))).log).re

State before:
case pos
N : ℕ
χ : DirichletCharacter ℂ N
n : ℕ
hn : 2 ≤ n
x y : ℝ
hx : 1 < x
hn' : IsUnit ↑n
ha₀ : 0 ≤ ↑n ^ (-x)
ha₁ : ↑n ^ (-x) < 1
hz : ‖χ ↑n * ↑n ^ (-(I * ↑y))‖ = 1
⊢ 0 ≤
    3 * (-(1 - ↑n ^ (-↑x)).log).re + 4 * (-(1 - χ ↑n * ↑n ^ (-(↑x + I * ↑y))).log).re +
      (-(1 - χ ↑n ^ 2 * ↑n ^ (-(↑x + 2 * I * ↑y))).log).re
Tactic:
convert re_log_comb_nonneg' ha₀ ha₁ hz using 6
State after:
case h.e'_4.h.e'_5.h.e'_5.h.e'_6.h.e'_1.h.e'_3
N : ℕ
χ : DirichletCharacter ℂ N
n : ℕ
hn : 2 ≤ n
x y : ℝ
hx : 1 < x
hn' : IsUnit ↑n
ha₀ : 0 ≤ ↑n ^ (-x)
ha₁ : ↑n ^ (-x) < 1
hz : ‖χ ↑n * ↑n ^ (-(I * ↑y))‖ = 1
⊢ (1 - ↑n ^ (-↑x)).log = (1 - ↑(↑n ^ (-x))).log

case h.e'_4.h.e'_5.h.e'_6.h.e'_6.h.e'_1.h.e'_3
N : ℕ
χ : DirichletCharacter ℂ N
n : ℕ
hn : 2 ≤ n
x y : ℝ
hx : 1 < x
hn' : IsUnit ↑n
ha₀ : 0 ≤ ↑n ^ (-x)
ha₁ : ↑n ^ (-x) < 1
hz : ‖χ ↑n * ↑n ^ (-(I * ↑y))‖ = 1
⊢ (1 - χ ↑n * ↑n ^ (-(↑x + I * ↑y))).log = (1 - ↑(↑n ^ (-x)) * (χ ↑n * ↑n ^ (-(I * ↑y)))).log

case h.e'_4.h.e'_6.h.e'_1.h.e'_3.h.e'_1.h.e'_6
N : ℕ
χ : DirichletCharacter ℂ N
n : ℕ
hn : 2 ≤ n
x y : ℝ
hx : 1 < x
hn' : IsUnit ↑n
ha₀ : 0 ≤ ↑n ^ (-x)
ha₁ : ↑n ^ (-x) < 1
hz : ‖χ ↑n * ↑n ^ (-(I * ↑y))‖ = 1
⊢ χ ↑n ^ 2 * ↑n ^ (-(↑x + 2 * I * ↑y)) = ↑(↑n ^ (-x)) * (χ ↑n * ↑n ^ (-(I * ↑y))) ^ 2

State before:
N : ℕ
χ : DirichletCharacter ℂ N
n : ℕ
hn : 2 ≤ n
x y : ℝ
hx : 1 < x
hn' : IsUnit ↑n
ha₀ : 0 ≤ ↑n ^ (-x)
⊢ ↑n ^ (-x) < 1
Tactic:
simpa only [Real.rpow_lt_one_iff n.cast_nonneg, Nat.cast_eq_zero, Nat.one_lt_cast,
  Left.neg_neg_iff, Nat.cast_lt_one, Left.neg_pos_iff]
  using Or.inr <| Or.inl ⟨hn, zero_lt_one.trans hx⟩
State after:
no goals

State before:
N : ℕ
χ : DirichletCharacter ℂ N
n : ℕ
hn : 2 ≤ n
x y : ℝ
hx : 1 < x
hn' : IsUnit ↑n
ha₀ : 0 ≤ ↑n ^ (-x)
ha₁ : ↑n ^ (-x) < 1
⊢ ‖χ ↑n * ↑n ^ (-(I * ↑y))‖ = 1
Tactic:
rw [norm_mul, ← hn'.unit_spec, DirichletCharacter.unit_norm_eq_one χ hn'.unit, one_mul,
  norm_eq_abs, abs_cpow_of_imp fun h ↦ False.elim <| by linarith [Nat.cast_eq_zero.mp h, hn]]
State after:
N : ℕ
χ : DirichletCharacter ℂ N
n : ℕ
hn : 2 ≤ n
x y : ℝ
hx : 1 < x
hn' : IsUnit ↑n
ha₀ : 0 ≤ ↑n ^ (-x)
ha₁ : ↑n ^ (-x) < 1
⊢ Complex.abs ↑n ^ (-(I * ↑y)).re / ((↑n).arg * (-(I * ↑y)).im).exp = 1

State before:
N : ℕ
χ : DirichletCharacter ℂ N
n : ℕ
hn : 2 ≤ n
x y : ℝ
hx : 1 < x
hn' : IsUnit ↑n
ha₀ : 0 ≤ ↑n ^ (-x)
ha₁ : ↑n ^ (-x) < 1
⊢ Complex.abs ↑n ^ (-(I * ↑y)).re / ((↑n).arg * (-(I * ↑y)).im).exp = 1
Tactic:
simp
State after:
no goals

State before:
N : ℕ
χ : DirichletCharacter ℂ N
n : ℕ
hn : 2 ≤ n
x y : ℝ
hx : 1 < x
hn' : IsUnit ↑n
ha₀ : 0 ≤ ↑n ^ (-x)
ha₁ : ↑n ^ (-x) < 1
h : ↑n = 0
⊢ False
Tactic:
linarith [Nat.cast_eq_zero.mp h, hn]
State after:
no goals

State before:
case h.e'_4.h.e'_5.h.e'_5.h.e'_6.h.e'_1.h.e'_3
N : ℕ
χ : DirichletCharacter ℂ N
n : ℕ
hn : 2 ≤ n
x y : ℝ
hx : 1 < x
hn' : IsUnit ↑n
ha₀ : 0 ≤ ↑n ^ (-x)
ha₁ : ↑n ^ (-x) < 1
hz : ‖χ ↑n * ↑n ^ (-(I * ↑y))‖ = 1
⊢ (1 - ↑n ^ (-↑x)).log = (1 - ↑(↑n ^ (-x))).log
Tactic:
congr 2
State after:
case h.e'_4.h.e'_5.h.e'_5.h.e'_6.h.e'_1.h.e'_3.e_x.e_a
N : ℕ
χ : DirichletCharacter ℂ N
n : ℕ
hn : 2 ≤ n
x y : ℝ
hx : 1 < x
hn' : IsUnit ↑n
ha₀ : 0 ≤ ↑n ^ (-x)
ha₁ : ↑n ^ (-x) < 1
hz : ‖χ ↑n * ↑n ^ (-(I * ↑y))‖ = 1
⊢ ↑n ^ (-↑x) = ↑(↑n ^ (-x))

State before:
case h.e'_4.h.e'_5.h.e'_5.h.e'_6.h.e'_1.h.e'_3.e_x.e_a
N : ℕ
χ : DirichletCharacter ℂ N
n : ℕ
hn : 2 ≤ n
x y : ℝ
hx : 1 < x
hn' : IsUnit ↑n
ha₀ : 0 ≤ ↑n ^ (-x)
ha₁ : ↑n ^ (-x) < 1
hz : ‖χ ↑n * ↑n ^ (-(I * ↑y))‖ = 1
⊢ ↑n ^ (-↑x) = ↑(↑n ^ (-x))
Tactic:
exact_mod_cast (ofReal_cpow n.cast_nonneg (-x)).symm
State after:
no goals

State before:
case h.e'_4.h.e'_5.h.e'_6.h.e'_6.h.e'_1.h.e'_3
N : ℕ
χ : DirichletCharacter ℂ N
n : ℕ
hn : 2 ≤ n
x y : ℝ
hx : 1 < x
hn' : IsUnit ↑n
ha₀ : 0 ≤ ↑n ^ (-x)
ha₁ : ↑n ^ (-x) < 1
hz : ‖χ ↑n * ↑n ^ (-(I * ↑y))‖ = 1
⊢ (1 - χ ↑n * ↑n ^ (-(↑x + I * ↑y))).log = (1 - ↑(↑n ^ (-x)) * (χ ↑n * ↑n ^ (-(I * ↑y)))).log
Tactic:
congr 2
State after:
case h.e'_4.h.e'_5.h.e'_6.h.e'_6.h.e'_1.h.e'_3.e_x.e_a
N : ℕ
χ : DirichletCharacter ℂ N
n : ℕ
hn : 2 ≤ n
x y : ℝ
hx : 1 < x
hn' : IsUnit ↑n
ha₀ : 0 ≤ ↑n ^ (-x)
ha₁ : ↑n ^ (-x) < 1
hz : ‖χ ↑n * ↑n ^ (-(I * ↑y))‖ = 1
⊢ χ ↑n * ↑n ^ (-(↑x + I * ↑y)) = ↑(↑n ^ (-x)) * (χ ↑n * ↑n ^ (-(I * ↑y)))

State before:
case h.e'_4.h.e'_5.h.e'_6.h.e'_6.h.e'_1.h.e'_3.e_x.e_a
N : ℕ
χ : DirichletCharacter ℂ N
n : ℕ
hn : 2 ≤ n
x y : ℝ
hx : 1 < x
hn' : IsUnit ↑n
ha₀ : 0 ≤ ↑n ^ (-x)
ha₁ : ↑n ^ (-x) < 1
hz : ‖χ ↑n * ↑n ^ (-(I * ↑y))‖ = 1
⊢ χ ↑n * ↑n ^ (-(↑x + I * ↑y)) = ↑(↑n ^ (-x)) * (χ ↑n * ↑n ^ (-(I * ↑y)))
Tactic:
rw [neg_add, cpow_add _ _ <| by norm_cast; linarith, ← ofReal_neg,
  ofReal_cpow n.cast_nonneg (-x), ofReal_natCast]
State after:
case h.e'_4.h.e'_5.h.e'_6.h.e'_6.h.e'_1.h.e'_3.e_x.e_a
N : ℕ
χ : DirichletCharacter ℂ N
n : ℕ
hn : 2 ≤ n
x y : ℝ
hx : 1 < x
hn' : IsUnit ↑n
ha₀ : 0 ≤ ↑n ^ (-x)
ha₁ : ↑n ^ (-x) < 1
hz : ‖χ ↑n * ↑n ^ (-(I * ↑y))‖ = 1
⊢ χ ↑n * (↑n ^ ↑(-x) * ↑n ^ (-(I * ↑y))) = ↑n ^ ↑(-x) * (χ ↑n * ↑n ^ (-(I * ↑y)))

State before:
case h.e'_4.h.e'_5.h.e'_6.h.e'_6.h.e'_1.h.e'_3.e_x.e_a
N : ℕ
χ : DirichletCharacter ℂ N
n : ℕ
hn : 2 ≤ n
x y : ℝ
hx : 1 < x
hn' : IsUnit ↑n
ha₀ : 0 ≤ ↑n ^ (-x)
ha₁ : ↑n ^ (-x) < 1
hz : ‖χ ↑n * ↑n ^ (-(I * ↑y))‖ = 1
⊢ χ ↑n * (↑n ^ ↑(-x) * ↑n ^ (-(I * ↑y))) = ↑n ^ ↑(-x) * (χ ↑n * ↑n ^ (-(I * ↑y)))
Tactic:
ring
State after:
no goals

State before:
N : ℕ
χ : DirichletCharacter ℂ N
n : ℕ
hn : 2 ≤ n
x y : ℝ
hx : 1 < x
hn' : IsUnit ↑n
ha₀ : 0 ≤ ↑n ^ (-x)
ha₁ : ↑n ^ (-x) < 1
hz : ‖χ ↑n * ↑n ^ (-(I * ↑y))‖ = 1
⊢ ↑n ≠ 0
Tactic:
norm_cast
State after:
N : ℕ
χ : DirichletCharacter ℂ N
n : ℕ
hn : 2 ≤ n
x y : ℝ
hx : 1 < x
hn' : IsUnit ↑n
ha₀ : 0 ≤ ↑n ^ (-x)
ha₁ : ↑n ^ (-x) < 1
hz : ‖χ ↑n * ↑n ^ (-(I * ↑y))‖ = 1
⊢ ¬n = 0

State before:
N : ℕ
χ : DirichletCharacter ℂ N
n : ℕ
hn : 2 ≤ n
x y : ℝ
hx : 1 < x
hn' : IsUnit ↑n
ha₀ : 0 ≤ ↑n ^ (-x)
ha₁ : ↑n ^ (-x) < 1
hz : ‖χ ↑n * ↑n ^ (-(I * ↑y))‖ = 1
⊢ ¬n = 0
Tactic:
linarith
State after:
no goals

State before:
case h.e'_4.h.e'_6.h.e'_1.h.e'_3.h.e'_1.h.e'_6
N : ℕ
χ : DirichletCharacter ℂ N
n : ℕ
hn : 2 ≤ n
x y : ℝ
hx : 1 < x
hn' : IsUnit ↑n
ha₀ : 0 ≤ ↑n ^ (-x)
ha₁ : ↑n ^ (-x) < 1
hz : ‖χ ↑n * ↑n ^ (-(I * ↑y))‖ = 1
⊢ χ ↑n ^ 2 * ↑n ^ (-(↑x + 2 * I * ↑y)) = ↑(↑n ^ (-x)) * (χ ↑n * ↑n ^ (-(I * ↑y))) ^ 2
Tactic:
rw [neg_add, cpow_add _ _ <| by norm_cast; linarith, ← ofReal_neg,
  ofReal_cpow n.cast_nonneg (-x), ofReal_natCast,
  show -(2 * I * y) = (2 : ℕ) * (-I * y) by ring, cpow_nat_mul]
State after:
case h.e'_4.h.e'_6.h.e'_1.h.e'_3.h.e'_1.h.e'_6
N : ℕ
χ : DirichletCharacter ℂ N
n : ℕ
hn : 2 ≤ n
x y : ℝ
hx : 1 < x
hn' : IsUnit ↑n
ha₀ : 0 ≤ ↑n ^ (-x)
ha₁ : ↑n ^ (-x) < 1
hz : ‖χ ↑n * ↑n ^ (-(I * ↑y))‖ = 1
⊢ χ ↑n ^ 2 * (↑n ^ ↑(-x) * (↑n ^ (-I * ↑y)) ^ 2) = ↑n ^ ↑(-x) * (χ ↑n * ↑n ^ (-(I * ↑y))) ^ 2

State before:
case h.e'_4.h.e'_6.h.e'_1.h.e'_3.h.e'_1.h.e'_6
N : ℕ
χ : DirichletCharacter ℂ N
n : ℕ
hn : 2 ≤ n
x y : ℝ
hx : 1 < x
hn' : IsUnit ↑n
ha₀ : 0 ≤ ↑n ^ (-x)
ha₁ : ↑n ^ (-x) < 1
hz : ‖χ ↑n * ↑n ^ (-(I * ↑y))‖ = 1
⊢ χ ↑n ^ 2 * (↑n ^ ↑(-x) * (↑n ^ (-I * ↑y)) ^ 2) = ↑n ^ ↑(-x) * (χ ↑n * ↑n ^ (-(I * ↑y))) ^ 2
Tactic:
ring_nf
State after:
no goals

State before:
N : ℕ
χ : DirichletCharacter ℂ N
n : ℕ
hn : 2 ≤ n
x y : ℝ
hx : 1 < x
hn' : IsUnit ↑n
ha₀ : 0 ≤ ↑n ^ (-x)
ha₁ : ↑n ^ (-x) < 1
hz : ‖χ ↑n * ↑n ^ (-(I * ↑y))‖ = 1
⊢ -(2 * I * ↑y) = ↑2 * (-I * ↑y)
Tactic:
ring
State after:
no goals

State before:
case neg
N : ℕ
χ : DirichletCharacter ℂ N
n : ℕ
hn : 2 ≤ n
x y : ℝ
hx : 1 < x
hn' : ¬IsUnit ↑n
⊢ 0 ≤
    3 * (-(1 - 1 ↑n * ↑n ^ (-↑x)).log).re + 4 * (-(1 - χ ↑n * ↑n ^ (-(↑x + I * ↑y))).log).re +
      (-(1 - χ ↑n ^ 2 * ↑n ^ (-(↑x + 2 * I * ↑y))).log).re
Tactic:
simp [MulChar.map_nonunit _ hn']
State after:
no goals