-- Mathlib/NumberTheory/LSeries/Nonvanishing.lean
/-- For positive `x` and nonzero `y` and a Dirichlet character `χ` we have that
`|L(χ^0, 1 + x)^3 L(χ, 1 + x + I * y)^4 L(χ^2, 1 + x + 2 * I * y)| ≥ 1. -/
lemma norm_LSeries_product_ge_one {x : ℝ} (hx : 0 < x) (y : ℝ) :
    ‖L ↗(1 : DirichletCharacter ℂ N) (1 + x) ^ 3 * L ↗χ (1 + x + I * y) ^ 4 *
      L ↗(χ ^ 2 :) (1 + x + 2 * I * y)‖ ≥ 1

Proof state:
N : ℕ
χ : DirichletCharacter ℂ N
x : ℝ
hx : 0 < x
y : ℝ
h₀ : 1 < (1 + ↑x).re
h₁ : 1 < (1 + ↑x + I * ↑y).re
h₂ : 1 < (1 + ↑x + 2 * I * ↑y).re
H₀ : Summable fun p => -log (1 - 1 ↑↑p * ↑↑p ^ (-(1 + ↑x)))
H₁ : Summable fun p => -log (1 - χ ↑↑p * ↑↑p ^ (-(1 + ↑x + I * ↑y)))
H₂ : Summable fun p => -log (1 - (χ ^ 2) ↑↑p * ↑↑p ^ (-(1 + ↑x + 2 * I * ↑y)))
hsum₀ : Summable fun i => 3 * (-log (1 - 1 ↑↑i * ↑↑i ^ (-(1 + ↑x)))).re
hsum₁ : Summable fun i => 4 * (-log (1 - χ ↑↑i * ↑↑i ^ (-(1 + ↑x + I * ↑y)))).re
hsum₂ : Summable fun x_1 => (-log (1 - (χ ^ 2) ↑↑x_1 * ↑↑x_1 ^ (-(1 + ↑x + 2 * I * ↑y)))).re
⊢ ‖cexp (∑' (p : Nat.Primes), -log (1 - 1 ↑↑p * ↑↑p ^ (-(1 + ↑x)))) ^ 3 *
          cexp (∑' (p : Nat.Primes), -log (1 - χ ↑↑p * ↑↑p ^ (-(1 + ↑x + I * ↑y)))) ^ 4 *
        cexp (∑' (p : Nat.Primes), -log (1 - (χ ^ 2) ↑↑p * ↑↑p ^ (-(1 + ↑x + 2 * I * ↑y))))‖ ≥
    1

Tactic:
simp only [← exp_nat_mul, Nat.cast_ofNat, ← exp_add, norm_exp, add_re, mul_re,
  re_ofNat, im_ofNat, zero_mul, sub_zero, Real.one_le_exp_iff]

Result:
N : ℕ
χ : DirichletCharacter ℂ N
x : ℝ
hx : 0 < x
y : ℝ
h₀ : 1 < (1 + ↑x).re
h₁ : 1 < (1 + ↑x + I * ↑y).re
h₂ : 1 < (1 + ↑x + 2 * I * ↑y).re
H₀ : Summable fun p => -log (1 - 1 ↑↑p * ↑↑p ^ (-(1 + ↑x)))
H₁ : Summable fun p => -log (1 - χ ↑↑p * ↑↑p ^ (-(1 + ↑x + I * ↑y)))
H₂ : Summable fun p => -log (1 - (χ ^ 2) ↑↑p * ↑↑p ^ (-(1 + ↑x + 2 * I * ↑y)))
hsum₀ : Summable fun i => 3 * (-log (1 - 1 ↑↑i * ↑↑i ^ (-(1 + ↑x)))).re
hsum₁ : Summable fun i => 4 * (-log (1 - χ ↑↑i * ↑↑i ^ (-(1 + ↑x + I * ↑y)))).re
hsum₂ : Summable fun x_1 => (-log (1 - (χ ^ 2) ↑↑x_1 * ↑↑x_1 ^ (-(1 + ↑x + 2 * I * ↑y)))).re
⊢ 0 ≤
    3 * (∑' (p : Nat.Primes), -log (1 - 1 ↑↑p * ↑↑p ^ (-(1 + ↑x)))).re +
        4 * (∑' (p : Nat.Primes), -log (1 - χ ↑↑p * ↑↑p ^ (-(1 + ↑x + I * ↑y)))).re +
      (∑' (p : Nat.Primes), -log (1 - (χ ^ 2) ↑↑p * ↑↑p ^ (-(1 + ↑x + 2 * I * ↑y)))).re

Proof state:
N : ℕ
χ : DirichletCharacter ℂ N
x : ℝ
hx : 0 < x
y : ℝ
h₀ : 1 < (1 + ↑x).re
h₁ : 1 < (1 + ↑x + I * ↑y).re
h₂ : 1 < (1 + ↑x + 2 * I * ↑y).re
H₀ : Summable fun p => -log (1 - 1 ↑↑p * ↑↑p ^ (-(1 + ↑x)))
⊢ ‖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₁ := summable_neg_log_one_sub_mul_prime_cpow χ h₁

Result:
N : ℕ
χ : DirichletCharacter ℂ N
x : ℝ
hx : 0 < x
y : ℝ
h₀ : 1 < (1 + ↑x).re
h₁ : 1 < (1 + ↑x + I * ↑y).re
h₂ : 1 < (1 + ↑x + 2 * I * ↑y).re
H₀ : Summable fun p => -log (1 - 1 ↑↑p * ↑↑p ^ (-(1 + ↑x)))
H₁ : Summable fun p => -log (1 - χ ↑↑p * ↑↑p ^ (-(1 + ↑x + I * ↑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

Proof state:
N : ℕ
χ : DirichletCharacter ℂ N
x : ℝ
hx : 0 < x
y : ℝ
h₀ : 1 < (1 + ↑x).re
h₁ : 1 < (1 + ↑x + I * ↑y).re
h₂ : 1 < (1 + ↑x + 2 * I * ↑y).re
H₀ : Summable fun p => -log (1 - 1 ↑↑p * ↑↑p ^ (-(1 + ↑x)))
H₁ : Summable fun p => -log (1 - χ ↑↑p * ↑↑p ^ (-(1 + ↑x + I * ↑y)))
H₂ : Summable fun p => -log (1 - (χ ^ 2) ↑↑p * ↑↑p ^ (-(1 + ↑x + 2 * I * ↑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:
have hsum₀ := (hasSum_re H₀.hasSum).summable.mul_left 3

Result:
N : ℕ
χ : DirichletCharacter ℂ N
x : ℝ
hx : 0 < x
y : ℝ
h₀ : 1 < (1 + ↑x).re
h₁ : 1 < (1 + ↑x + I * ↑y).re
h₂ : 1 < (1 + ↑x + 2 * I * ↑y).re
H₀ : Summable fun p => -log (1 - 1 ↑↑p * ↑↑p ^ (-(1 + ↑x)))
H₁ : Summable fun p => -log (1 - χ ↑↑p * ↑↑p ^ (-(1 + ↑x + I * ↑y)))
H₂ : Summable fun p => -log (1 - (χ ^ 2) ↑↑p * ↑↑p ^ (-(1 + ↑x + 2 * I * ↑y)))
hsum₀ : Summable fun i => 3 * (-log (1 - 1 ↑↑i * ↑↑i ^ (-(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

Proof state:
N : ℕ
χ : DirichletCharacter ℂ N
x : ℝ
hx : 0 < x
y : ℝ
h₀ : 1 < (1 + ↑x).re
h₁ : 1 < (1 + ↑x + I * ↑y).re
h₂ : 1 < (1 + ↑x + 2 * I * ↑y).re
H₀ : Summable fun p => -log (1 - 1 ↑↑p * ↑↑p ^ (-(1 + ↑x)))
H₁ : Summable fun p => -log (1 - χ ↑↑p * ↑↑p ^ (-(1 + ↑x + I * ↑y)))
H₂ : Summable fun p => -log (1 - (χ ^ 2) ↑↑p * ↑↑p ^ (-(1 + ↑x + 2 * I * ↑y)))
hsum₀ : Summable fun i => 3 * (-log (1 - 1 ↑↑i * ↑↑i ^ (-(1 + ↑x)))).re
hsum₁ : Summable fun i => 4 * (-log (1 - χ ↑↑i * ↑↑i ^ (-(1 + ↑x + I * ↑y)))).re
hsum₂ : Summable fun x_1 => (-log (1 - (χ ^ 2) ↑↑x_1 * ↑↑x_1 ^ (-(1 + ↑x + 2 * I * ↑y)))).re
⊢ 0 ≤
    ∑' (b : Nat.Primes),
      (3 * (-log (1 - 1 ↑↑b * ↑↑b ^ (-(1 + ↑x)))).re + 4 * (-log (1 - χ ↑↑b * ↑↑b ^ (-(1 + ↑x + I * ↑y)))).re +
        (-log (1 - (χ ^ 2) ↑↑b * ↑↑b ^ (-(1 + ↑x + 2 * I * ↑y)))).re)

Tactic:
simpa only [neg_add_rev, neg_re, mul_neg, χ.pow_apply' two_ne_zero, ge_iff_le, add_re, one_re,
  ofReal_re, ofReal_add, ofReal_one] using
    tsum_nonneg fun (p : Nat.Primes) ↦ χ.re_log_comb_nonneg p.prop.two_le h₀ y

Result:
no goals

Proof state:
N : ℕ
χ : DirichletCharacter ℂ N
x : ℝ
hx : 0 < x
y : ℝ
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 H₀ := summable_neg_log_one_sub_mul_prime_cpow (N := N) 1 h₀

Result:
N : ℕ
χ : DirichletCharacter ℂ N
x : ℝ
hx : 0 < x
y : ℝ
h₀ : 1 < (1 + ↑x).re
h₁ : 1 < (1 + ↑x + I * ↑y).re
h₂ : 1 < (1 + ↑x + 2 * I * ↑y).re
H₀ : Summable fun p => -log (1 - 1 ↑↑p * ↑↑p ^ (-(1 + ↑x)))
⊢ ‖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

Proof state:
N : ℕ
χ : DirichletCharacter ℂ N
x : ℝ
hx : 0 < x
y : ℝ
h₀ : 1 < (1 + ↑x).re
h₁ : 1 < (1 + ↑x + I * ↑y).re
h₂ : 1 < (1 + ↑x + 2 * I * ↑y).re
H₀ : Summable fun p => -log (1 - 1 ↑↑p * ↑↑p ^ (-(1 + ↑x)))
H₁ : Summable fun p => -log (1 - χ ↑↑p * ↑↑p ^ (-(1 + ↑x + I * ↑y)))
H₂ : Summable fun p => -log (1 - (χ ^ 2) ↑↑p * ↑↑p ^ (-(1 + ↑x + 2 * I * ↑y)))
hsum₀ : Summable fun i => 3 * (-log (1 - 1 ↑↑i * ↑↑i ^ (-(1 + ↑x)))).re
hsum₁ : Summable fun i => 4 * (-log (1 - χ ↑↑i * ↑↑i ^ (-(1 + ↑x + 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 hsum₂ := (hasSum_re H₂.hasSum).summable

Result:
N : ℕ
χ : DirichletCharacter ℂ N
x : ℝ
hx : 0 < x
y : ℝ
h₀ : 1 < (1 + ↑x).re
h₁ : 1 < (1 + ↑x + I * ↑y).re
h₂ : 1 < (1 + ↑x + 2 * I * ↑y).re
H₀ : Summable fun p => -log (1 - 1 ↑↑p * ↑↑p ^ (-(1 + ↑x)))
H₁ : Summable fun p => -log (1 - χ ↑↑p * ↑↑p ^ (-(1 + ↑x + I * ↑y)))
H₂ : Summable fun p => -log (1 - (χ ^ 2) ↑↑p * ↑↑p ^ (-(1 + ↑x + 2 * I * ↑y)))
hsum₀ : Summable fun i => 3 * (-log (1 - 1 ↑↑i * ↑↑i ^ (-(1 + ↑x)))).re
hsum₁ : Summable fun i => 4 * (-log (1 - χ ↑↑i * ↑↑i ^ (-(1 + ↑x + I * ↑y)))).re
hsum₂ : Summable fun x_1 => (-log (1 - (χ ^ 2) ↑↑x_1 * ↑↑x_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