Theorem: norm_dirichlet_product_ge_one (EulerProducts/PNT.lean)

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)
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

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
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

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]
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

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
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

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
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

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
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

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]
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

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]
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

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₂]
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)

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₀
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

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]
State after:
no goals

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
⊢ 1 + ↑x = ↑(1 + ↑x).re
Tactic:
simp only [add_re, one_re, ofReal_re, ofReal_add, ofReal_one]
State after:
no goals