internlm/Lean-Github huggingface dataset:
Theorem: re_log_comb_nonneg_dirichlet
Proof 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 _
Proof 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
Theorem: re_log_comb_nonneg_dirichlet
Proof 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⟩
Proof 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
Theorem: re_log_comb_nonneg_dirichlet
Proof 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
Proof 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
Theorem: re_log_comb_nonneg_dirichlet
Proof 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]
Proof 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
Theorem: re_log_comb_nonneg_dirichlet
Proof 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
Proof 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
Theorem: re_log_comb_nonneg_dirichlet
Proof 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⟩
Proof state after:
no goals
Theorem: re_log_comb_nonneg_dirichlet
Proof 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]]
Proof 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
Theorem: re_log_comb_nonneg_dirichlet
Proof 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
Proof state after:
no goals
Theorem: re_log_comb_nonneg_dirichlet
Proof 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]
Proof state after:
no goals
Theorem: re_log_comb_nonneg_dirichlet
Proof 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
Proof 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))
Theorem: re_log_comb_nonneg_dirichlet
Proof 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
Proof state after:
no goals
Theorem: re_log_comb_nonneg_dirichlet
Proof 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
Proof 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)))
Theorem: re_log_comb_nonneg_dirichlet
Proof 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]
Proof 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)))
Theorem: re_log_comb_nonneg_dirichlet
Proof 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
Proof state after:
no goals
Theorem: re_log_comb_nonneg_dirichlet
Proof 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
Proof 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
Theorem: re_log_comb_nonneg_dirichlet
Proof 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
Proof state after:
no goals
Theorem: re_log_comb_nonneg_dirichlet
Proof 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]
Proof 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
Theorem: re_log_comb_nonneg_dirichlet
Proof 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
Proof state after:
no goals
Theorem: re_log_comb_nonneg_dirichlet
Proof 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
Proof state after:
no goals
Theorem: re_log_comb_nonneg_dirichlet
Proof 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']
Proof state after:
no goals
Theorem: one_lt_re_of_pos
Proof state before:
x y : ℝ
hx : 0 < x
⊢ 1 < (1 + ↑x).re ∧ 1 < (1 + ↑x + I * ↑y).re ∧ 1 < (1 + ↑x + 2 * I * ↑y).re
Tactic:
simp only [add_re, one_re, ofReal_re, lt_add_iff_pos_right, hx, mul_re, I_re, zero_mul, I_im,
  ofReal_im, mul_zero, sub_self, add_zero, re_ofNat, im_ofNat, mul_one, mul_im, and_self]
Proof state after:
no goals
Theorem: norm_dirichlet_product_ge_one
Proof state before:
N : ℕ
χ : DirichletCharacter ℂ N
x : ℝ
hx : 0 < x
y : ℝ
⊢ ‖L (fun n => 1 ↑n) (1 + ↑x) ^ 3 * L (fun n => χ ↑n) (1 + ↑x + I * ↑y) ^ 4 *
        L (fun n => (χ ^ 2) ↑n) (1 + ↑x + 2 * I * ↑y)‖ ≥
    1
Tactic:
let χ₀ := (1 : DirichletCharacter ℂ N)
Proof state after:
N : ℕ
χ : DirichletCharacter ℂ N
x : ℝ
hx : 0 < x
y : ℝ
χ₀ : DirichletCharacter ℂ N := 1
⊢ ‖L (fun n => 1 ↑n) (1 + ↑x) ^ 3 * L (fun n => χ ↑n) (1 + ↑x + I * ↑y) ^ 4 *
        L (fun n => (χ ^ 2) ↑n) (1 + ↑x + 2 * I * ↑y)‖ ≥
    1
Theorem: norm_dirichlet_product_ge_one
Proof state before:
N : ℕ
χ : DirichletCharacter ℂ N
x : ℝ
hx : 0 < x
y : ℝ
χ₀ : DirichletCharacter ℂ N := 1
⊢ ‖L (fun n => 1 ↑n) (1 + ↑x) ^ 3 * L (fun n => χ ↑n) (1 + ↑x + I * ↑y) ^ 4 *
        L (fun n => (χ ^ 2) ↑n) (1 + ↑x + 2 * I * ↑y)‖ ≥
    1
Tactic:
have ⟨h₀, h₁, h₂⟩ := one_lt_re_of_pos y hx
Proof state after:
N : ℕ
χ : DirichletCharacter ℂ N
x : ℝ
hx : 0 < x
y : ℝ
χ₀ : DirichletCharacter ℂ N := 1
h₀ : 1 < (1 + ↑x).re
h₁ : 1 < (1 + ↑x + I * ↑y).re
h₂ : 1 < (1 + ↑x + 2 * I * ↑y).re
⊢ ‖L (fun n => 1 ↑n) (1 + ↑x) ^ 3 * L (fun n => χ ↑n) (1 + ↑x + I * ↑y) ^ 4 *
        L (fun n => (χ ^ 2) ↑n) (1 + ↑x + 2 * I * ↑y)‖ ≥
    1
Theorem: norm_dirichlet_product_ge_one
Proof state before:
N : ℕ
χ : DirichletCharacter ℂ N
x : ℝ
hx : 0 < x
y : ℝ
χ₀ : DirichletCharacter ℂ N := 1
h₀ : 1 < (1 + ↑x).re
h₁ : 1 < (1 + ↑x + I * ↑y).re
h₂ : 1 < (1 + ↑x + 2 * I * ↑y).re
⊢ ‖L (fun n => 1 ↑n) (1 + ↑x) ^ 3 * L (fun n => χ ↑n) (1 + ↑x + I * ↑y) ^ 4 *
        L (fun n => (χ ^ 2) ↑n) (1 + ↑x + 2 * I * ↑y)‖ ≥
    1
Tactic:
have hx₁ : 1 + (x : ℂ) = (1 + x : ℂ).re := by simp only [add_re, one_re, ofReal_re, ofReal_add, ofReal_one]
Proof state after:
N : ℕ
χ : DirichletCharacter ℂ N
x : ℝ
hx : 0 < x
y : ℝ
χ₀ : DirichletCharacter ℂ N := 1
h₀ : 1 < (1 + ↑x).re
h₁ : 1 < (1 + ↑x + I * ↑y).re
h₂ : 1 < (1 + ↑x + 2 * I * ↑y).re
hx₁ : 1 + ↑x = ↑(1 + ↑x).re
⊢ ‖L (fun n => 1 ↑n) (1 + ↑x) ^ 3 * L (fun n => χ ↑n) (1 + ↑x + I * ↑y) ^ 4 *
        L (fun n => (χ ^ 2) ↑n) (1 + ↑x + 2 * I * ↑y)‖ ≥
    1
Theorem: norm_dirichlet_product_ge_one
Proof state before:
N : ℕ
χ : DirichletCharacter ℂ N
x : ℝ
hx : 0 < x
y : ℝ
χ₀ : DirichletCharacter ℂ N := 1
h₀ : 1 < (1 + ↑x).re
h₁ : 1 < (1 + ↑x + I * ↑y).re
h₂ : 1 < (1 + ↑x + 2 * I * ↑y).re
hx₁ : 1 + ↑x = ↑(1 + ↑x).re
⊢ ‖L (fun n => 1 ↑n) (1 + ↑x) ^ 3 * L (fun n => χ ↑n) (1 + ↑x + I * ↑y) ^ 4 *
        L (fun n => (χ ^ 2) ↑n) (1 + ↑x + 2 * I * ↑y)‖ ≥
    1
Tactic:
have hsum₀ :=
  (hasSum_re (summable_neg_log_one_sub_char_mul_prime_cpow χ₀ h₀).hasSum).summable.mul_left 3
Proof state after:
N : ℕ
χ : DirichletCharacter ℂ N
x : ℝ
hx : 0 < x
y : ℝ
χ₀ : DirichletCharacter ℂ N := 1
h₀ : 1 < (1 + ↑x).re
h₁ : 1 < (1 + ↑x + I * ↑y).re
h₂ : 1 < (1 + ↑x + 2 * I * ↑y).re
hx₁ : 1 + ↑x = ↑(1 + ↑x).re
hsum₀ : Summable fun i => 3 * (-(1 - χ₀ ↑↑i * ↑↑i ^ (-(1 + ↑x))).log).re
⊢ ‖L (fun n => 1 ↑n) (1 + ↑x) ^ 3 * L (fun n => χ ↑n) (1 + ↑x + I * ↑y) ^ 4 *
        L (fun n => (χ ^ 2) ↑n) (1 + ↑x + 2 * I * ↑y)‖ ≥
    1
Theorem: norm_dirichlet_product_ge_one
Proof state before:
N : ℕ
χ : DirichletCharacter ℂ N
x : ℝ
hx : 0 < x
y : ℝ
χ₀ : DirichletCharacter ℂ N := 1
h₀ : 1 < (1 + ↑x).re
h₁ : 1 < (1 + ↑x + I * ↑y).re
h₂ : 1 < (1 + ↑x + 2 * I * ↑y).re
hx₁ : 1 + ↑x = ↑(1 + ↑x).re
hsum₀ : Summable fun i => 3 * (-(1 - χ₀ ↑↑i * ↑↑i ^ (-(1 + ↑x))).log).re
⊢ ‖L (fun n => 1 ↑n) (1 + ↑x) ^ 3 * L (fun n => χ ↑n) (1 + ↑x + I * ↑y) ^ 4 *
        L (fun n => (χ ^ 2) ↑n) (1 + ↑x + 2 * I * ↑y)‖ ≥
    1
Tactic:
have hsum₁ :=
  (hasSum_re (summable_neg_log_one_sub_char_mul_prime_cpow χ h₁).hasSum).summable.mul_left 4
Proof state after:
N : ℕ
χ : DirichletCharacter ℂ N
x : ℝ
hx : 0 < x
y : ℝ
χ₀ : DirichletCharacter ℂ N := 1
h₀ : 1 < (1 + ↑x).re
h₁ : 1 < (1 + ↑x + I * ↑y).re
h₂ : 1 < (1 + ↑x + 2 * I * ↑y).re
hx₁ : 1 + ↑x = ↑(1 + ↑x).re
hsum₀ : Summable fun i => 3 * (-(1 - χ₀ ↑↑i * ↑↑i ^ (-(1 + ↑x))).log).re
hsum₁ : Summable fun i => 4 * (-(1 - χ ↑↑i * ↑↑i ^ (-(1 + ↑x + I * ↑y))).log).re
⊢ ‖L (fun n => 1 ↑n) (1 + ↑x) ^ 3 * L (fun n => χ ↑n) (1 + ↑x + I * ↑y) ^ 4 *
        L (fun n => (χ ^ 2) ↑n) (1 + ↑x + 2 * I * ↑y)‖ ≥
    1
Theorem: norm_dirichlet_product_ge_one
Proof state before:
N : ℕ
χ : DirichletCharacter ℂ N
x : ℝ
hx : 0 < x
y : ℝ
χ₀ : DirichletCharacter ℂ N := 1
h₀ : 1 < (1 + ↑x).re
h₁ : 1 < (1 + ↑x + I * ↑y).re
h₂ : 1 < (1 + ↑x + 2 * I * ↑y).re
hx₁ : 1 + ↑x = ↑(1 + ↑x).re
hsum₀ : Summable fun i => 3 * (-(1 - χ₀ ↑↑i * ↑↑i ^ (-(1 + ↑x))).log).re
hsum₁ : Summable fun i => 4 * (-(1 - χ ↑↑i * ↑↑i ^ (-(1 + ↑x + I * ↑y))).log).re
⊢ ‖L (fun n => 1 ↑n) (1 + ↑x) ^ 3 * L (fun n => χ ↑n) (1 + ↑x + I * ↑y) ^ 4 *
        L (fun n => (χ ^ 2) ↑n) (1 + ↑x + 2 * I * ↑y)‖ ≥
    1
Tactic:
have hsum₂ :=
  (hasSum_re (summable_neg_log_one_sub_char_mul_prime_cpow (χ ^ 2) h₂).hasSum).summable
Proof state after:
N : ℕ
χ : DirichletCharacter ℂ N
x : ℝ
hx : 0 < x
y : ℝ
χ₀ : DirichletCharacter ℂ N := 1
h₀ : 1 < (1 + ↑x).re
h₁ : 1 < (1 + ↑x + I * ↑y).re
h₂ : 1 < (1 + ↑x + 2 * I * ↑y).re
hx₁ : 1 + ↑x = ↑(1 + ↑x).re
hsum₀ : Summable fun i => 3 * (-(1 - χ₀ ↑↑i * ↑↑i ^ (-(1 + ↑x))).log).re
hsum₁ : Summable fun i => 4 * (-(1 - χ ↑↑i * ↑↑i ^ (-(1 + ↑x + I * ↑y))).log).re
hsum₂ : Summable fun x_1 => (-(1 - (χ ^ 2) ↑↑x_1 * ↑↑x_1 ^ (-(1 + ↑x + 2 * I * ↑y))).log).re
⊢ ‖L (fun n => 1 ↑n) (1 + ↑x) ^ 3 * L (fun n => χ ↑n) (1 + ↑x + I * ↑y) ^ 4 *
        L (fun n => (χ ^ 2) ↑n) (1 + ↑x + 2 * I * ↑y)‖ ≥
    1
Theorem: norm_dirichlet_product_ge_one
Proof state before:
N : ℕ
χ : DirichletCharacter ℂ N
x : ℝ
hx : 0 < x
y : ℝ
χ₀ : DirichletCharacter ℂ N := 1
h₀ : 1 < (1 + ↑x).re
h₁ : 1 < (1 + ↑x + I * ↑y).re
h₂ : 1 < (1 + ↑x + 2 * I * ↑y).re
hx₁ : 1 + ↑x = ↑(1 + ↑x).re
hsum₀ : Summable fun i => 3 * (-(1 - χ₀ ↑↑i * ↑↑i ^ (-(1 + ↑x))).log).re
hsum₁ : Summable fun i => 4 * (-(1 - χ ↑↑i * ↑↑i ^ (-(1 + ↑x + I * ↑y))).log).re
hsum₂ : Summable fun x_1 => (-(1 - (χ ^ 2) ↑↑x_1 * ↑↑x_1 ^ (-(1 + ↑x + 2 * I * ↑y))).log).re
⊢ ‖L (fun n => 1 ↑n) (1 + ↑x) ^ 3 * L (fun n => χ ↑n) (1 + ↑x + I * ↑y) ^ 4 *
        L (fun n => (χ ^ 2) ↑n) (1 + ↑x + 2 * I * ↑y)‖ ≥
    1
Tactic:
rw [← DirichletCharacter.LSeries_eulerProduct' _ h₀,
  ← DirichletCharacter.LSeries_eulerProduct' χ h₁,
  ← DirichletCharacter.LSeries_eulerProduct' (χ ^ 2) h₂, ← exp_nat_mul, ← exp_nat_mul, ← exp_add,
  ← exp_add, norm_eq_abs, abs_exp]
Proof state after:
N : ℕ
χ : DirichletCharacter ℂ N
x : ℝ
hx : 0 < x
y : ℝ
χ₀ : DirichletCharacter ℂ N := 1
h₀ : 1 < (1 + ↑x).re
h₁ : 1 < (1 + ↑x + I * ↑y).re
h₂ : 1 < (1 + ↑x + 2 * I * ↑y).re
hx₁ : 1 + ↑x = ↑(1 + ↑x).re
hsum₀ : Summable fun i => 3 * (-(1 - χ₀ ↑↑i * ↑↑i ^ (-(1 + ↑x))).log).re
hsum₁ : Summable fun i => 4 * (-(1 - χ ↑↑i * ↑↑i ^ (-(1 + ↑x + I * ↑y))).log).re
hsum₂ : Summable fun x_1 => (-(1 - (χ ^ 2) ↑↑x_1 * ↑↑x_1 ^ (-(1 + ↑x + 2 * I * ↑y))).log).re
⊢ (↑3 * ∑' (p : Primes), -(1 - 1 ↑↑p * ↑↑p ^ (-(1 + ↑x))).log +
            ↑4 * ∑' (p : Primes), -(1 - χ ↑↑p * ↑↑p ^ (-(1 + ↑x + I * ↑y))).log +
          ∑' (p : Primes), -(1 - (χ ^ 2) ↑↑p * ↑↑p ^ (-(1 + ↑x + 2 * I * ↑y))).log).re.exp ≥
    1
Theorem: norm_dirichlet_product_ge_one
Proof state before:
N : ℕ
χ : DirichletCharacter ℂ N
x : ℝ
hx : 0 < x
y : ℝ
χ₀ : DirichletCharacter ℂ N := 1
h₀ : 1 < (1 + ↑x).re
h₁ : 1 < (1 + ↑x + I * ↑y).re
h₂ : 1 < (1 + ↑x + 2 * I * ↑y).re
hx₁ : 1 + ↑x = ↑(1 + ↑x).re
hsum₀ : Summable fun i => 3 * (-(1 - χ₀ ↑↑i * ↑↑i ^ (-(1 + ↑x))).log).re
hsum₁ : Summable fun i => 4 * (-(1 - χ ↑↑i * ↑↑i ^ (-(1 + ↑x + I * ↑y))).log).re
hsum₂ : Summable fun x_1 => (-(1 - (χ ^ 2) ↑↑x_1 * ↑↑x_1 ^ (-(1 + ↑x + 2 * I * ↑y))).log).re
⊢ (↑3 * ∑' (p : Primes), -(1 - 1 ↑↑p * ↑↑p ^ (-(1 + ↑x))).log +
            ↑4 * ∑' (p : Primes), -(1 - χ ↑↑p * ↑↑p ^ (-(1 + ↑x + I * ↑y))).log +
          ∑' (p : Primes), -(1 - (χ ^ 2) ↑↑p * ↑↑p ^ (-(1 + ↑x + 2 * I * ↑y))).log).re.exp ≥
    1
Tactic:
simp only [Nat.cast_ofNat, add_re, mul_re, re_ofNat, im_ofNat, zero_mul, sub_zero,
  Real.one_le_exp_iff]
Proof state after:
N : ℕ
χ : DirichletCharacter ℂ N
x : ℝ
hx : 0 < x
y : ℝ
χ₀ : DirichletCharacter ℂ N := 1
h₀ : 1 < (1 + ↑x).re
h₁ : 1 < (1 + ↑x + I * ↑y).re
h₂ : 1 < (1 + ↑x + 2 * I * ↑y).re
hx₁ : 1 + ↑x = ↑(1 + ↑x).re
hsum₀ : Summable fun i => 3 * (-(1 - χ₀ ↑↑i * ↑↑i ^ (-(1 + ↑x))).log).re
hsum₁ : Summable fun i => 4 * (-(1 - χ ↑↑i * ↑↑i ^ (-(1 + ↑x + I * ↑y))).log).re
hsum₂ : Summable fun x_1 => (-(1 - (χ ^ 2) ↑↑x_1 * ↑↑x_1 ^ (-(1 + ↑x + 2 * I * ↑y))).log).re
⊢ 0 ≤
    3 * (∑' (p : Primes), -(1 - 1 ↑↑p * ↑↑p ^ (-(1 + ↑x))).log).re +
        4 * (∑' (p : Primes), -(1 - χ ↑↑p * ↑↑p ^ (-(1 + ↑x + I * ↑y))).log).re +
      (∑' (p : Primes), -(1 - (χ ^ 2) ↑↑p * ↑↑p ^ (-(1 + ↑x + 2 * I * ↑y))).log).re
Theorem: norm_dirichlet_product_ge_one
Proof state before:
N : ℕ
χ : DirichletCharacter ℂ N
x : ℝ
hx : 0 < x
y : ℝ
χ₀ : DirichletCharacter ℂ N := 1
h₀ : 1 < (1 + ↑x).re
h₁ : 1 < (1 + ↑x + I * ↑y).re
h₂ : 1 < (1 + ↑x + 2 * I * ↑y).re
hx₁ : 1 + ↑x = ↑(1 + ↑x).re
hsum₀ : Summable fun i => 3 * (-(1 - χ₀ ↑↑i * ↑↑i ^ (-(1 + ↑x))).log).re
hsum₁ : Summable fun i => 4 * (-(1 - χ ↑↑i * ↑↑i ^ (-(1 + ↑x + I * ↑y))).log).re
hsum₂ : Summable fun x_1 => (-(1 - (χ ^ 2) ↑↑x_1 * ↑↑x_1 ^ (-(1 + ↑x + 2 * I * ↑y))).log).re
⊢ 0 ≤
    3 * (∑' (p : Primes), -(1 - 1 ↑↑p * ↑↑p ^ (-(1 + ↑x))).log).re +
        4 * (∑' (p : Primes), -(1 - χ ↑↑p * ↑↑p ^ (-(1 + ↑x + I * ↑y))).log).re +
      (∑' (p : Primes), -(1 - (χ ^ 2) ↑↑p * ↑↑p ^ (-(1 + ↑x + 2 * I * ↑y))).log).re
Tactic:
rw [re_tsum <| summable_neg_log_one_sub_char_mul_prime_cpow _ h₀,
  re_tsum <| summable_neg_log_one_sub_char_mul_prime_cpow _ h₁,
  re_tsum <| summable_neg_log_one_sub_char_mul_prime_cpow _ h₂, ← tsum_mul_left, ← tsum_mul_left,
  ← tsum_add hsum₀ hsum₁, ← tsum_add (hsum₀.add hsum₁) hsum₂]
Proof state after:
N : ℕ
χ : DirichletCharacter ℂ N
x : ℝ
hx : 0 < x
y : ℝ
χ₀ : DirichletCharacter ℂ N := 1
h₀ : 1 < (1 + ↑x).re
h₁ : 1 < (1 + ↑x + I * ↑y).re
h₂ : 1 < (1 + ↑x + 2 * I * ↑y).re
hx₁ : 1 + ↑x = ↑(1 + ↑x).re
hsum₀ : Summable fun i => 3 * (-(1 - χ₀ ↑↑i * ↑↑i ^ (-(1 + ↑x))).log).re
hsum₁ : Summable fun i => 4 * (-(1 - χ ↑↑i * ↑↑i ^ (-(1 + ↑x + I * ↑y))).log).re
hsum₂ : Summable fun x_1 => (-(1 - (χ ^ 2) ↑↑x_1 * ↑↑x_1 ^ (-(1 + ↑x + 2 * I * ↑y))).log).re
⊢ 0 ≤
    ∑' (b : Primes),
      (3 * (-(1 - χ₀ ↑↑b * ↑↑b ^ (-(1 + ↑x))).log).re + 4 * (-(1 - χ ↑↑b * ↑↑b ^ (-(1 + ↑x + I * ↑y))).log).re +
        (-(1 - (χ ^ 2) ↑↑b * ↑↑b ^ (-(1 + ↑x + 2 * I * ↑y))).log).re)
Theorem: norm_dirichlet_product_ge_one
Proof state before:
N : ℕ
χ : DirichletCharacter ℂ N
x : ℝ
hx : 0 < x
y : ℝ
χ₀ : DirichletCharacter ℂ N := 1
h₀ : 1 < (1 + ↑x).re
h₁ : 1 < (1 + ↑x + I * ↑y).re
h₂ : 1 < (1 + ↑x + 2 * I * ↑y).re
hx₁ : 1 + ↑x = ↑(1 + ↑x).re
hsum₀ : Summable fun i => 3 * (-(1 - χ₀ ↑↑i * ↑↑i ^ (-(1 + ↑x))).log).re
hsum₁ : Summable fun i => 4 * (-(1 - χ ↑↑i * ↑↑i ^ (-(1 + ↑x + I * ↑y))).log).re
hsum₂ : Summable fun x_1 => (-(1 - (χ ^ 2) ↑↑x_1 * ↑↑x_1 ^ (-(1 + ↑x + 2 * I * ↑y))).log).re
⊢ 0 ≤
    ∑' (b : Primes),
      (3 * (-(1 - χ₀ ↑↑b * ↑↑b ^ (-(1 + ↑x))).log).re + 4 * (-(1 - χ ↑↑b * ↑↑b ^ (-(1 + ↑x + I * ↑y))).log).re +
        (-(1 - (χ ^ 2) ↑↑b * ↑↑b ^ (-(1 + ↑x + 2 * I * ↑y))).log).re)
Tactic:
convert tsum_nonneg fun p : Nat.Primes ↦ re_log_comb_nonneg_dirichlet χ p.prop.two_le h₀
Proof state after:
case h.e'_4.h.e'_5.h.h.e'_6.h.e'_1.h.e'_3.h.e'_1.h.e'_6.h.e'_5
N : ℕ
χ : DirichletCharacter ℂ N
x : ℝ
hx : 0 < x
y : ℝ
χ₀ : DirichletCharacter ℂ N := 1
h₀ : 1 < (1 + ↑x).re
h₁ : 1 < (1 + ↑x + I * ↑y).re
h₂ : 1 < (1 + ↑x + 2 * I * ↑y).re
hx₁ : 1 + ↑x = ↑(1 + ↑x).re
hsum₀ : Summable fun i => 3 * (-(1 - χ₀ ↑↑i * ↑↑i ^ (-(1 + ↑x))).log).re
hsum₁ : Summable fun i => 4 * (-(1 - χ ↑↑i * ↑↑i ^ (-(1 + ↑x + I * ↑y))).log).re
hsum₂ : Summable fun x_1 => (-(1 - (χ ^ 2) ↑↑x_1 * ↑↑x_1 ^ (-(1 + ↑x + 2 * I * ↑y))).log).re
x✝ : Primes
⊢ (χ ^ 2) ↑↑x✝ = χ ↑↑x✝ ^ 2
Theorem: norm_dirichlet_product_ge_one
Proof state before:
case h.e'_4.h.e'_5.h.h.e'_6.h.e'_1.h.e'_3.h.e'_1.h.e'_6.h.e'_5
N : ℕ
χ : DirichletCharacter ℂ N
x : ℝ
hx : 0 < x
y : ℝ
χ₀ : DirichletCharacter ℂ N := 1
h₀ : 1 < (1 + ↑x).re
h₁ : 1 < (1 + ↑x + I * ↑y).re
h₂ : 1 < (1 + ↑x + 2 * I * ↑y).re
hx₁ : 1 + ↑x = ↑(1 + ↑x).re
hsum₀ : Summable fun i => 3 * (-(1 - χ₀ ↑↑i * ↑↑i ^ (-(1 + ↑x))).log).re
hsum₁ : Summable fun i => 4 * (-(1 - χ ↑↑i * ↑↑i ^ (-(1 + ↑x + I * ↑y))).log).re
hsum₂ : Summable fun x_1 => (-(1 - (χ ^ 2) ↑↑x_1 * ↑↑x_1 ^ (-(1 + ↑x + 2 * I * ↑y))).log).re
x✝ : Primes
⊢ (χ ^ 2) ↑↑x✝ = χ ↑↑x✝ ^ 2
Tactic:
rw [sq, sq, MulChar.mul_apply]
Proof state after:
no goals