Theorem: norm_zeta_product_ge_one (EulerProducts/PNT.lean)

State before:
x : ℝ
hx : 0 < x
y : ℝ
⊢ ‖ζ (1 + ↑x) ^ 3 * ζ (1 + ↑x + I * ↑y) ^ 4 * ζ (1 + ↑x + 2 * I * ↑y)‖ ≥ 1
Tactic:
have ⟨h₀, h₁, h₂⟩ := one_lt_re_of_pos y hx
State after:
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
⊢ ‖ζ (1 + ↑x) ^ 3 * ζ (1 + ↑x + I * ↑y) ^ 4 * ζ (1 + ↑x + 2 * I * ↑y)‖ ≥ 1

State before:
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
⊢ ‖ζ (1 + ↑x) ^ 3 * ζ (1 + ↑x + I * ↑y) ^ 4 * ζ (1 + ↑x + 2 * I * ↑y)‖ ≥ 1
Tactic:
simpa only [one_pow, norm_mul, norm_pow, DirichletCharacter.LSeries_modOne_eq,
  LSeries_one_eq_riemannZeta, h₀, h₁, h₂] using norm_dirichlet_product_ge_one χ₁ hx y
State after:
no goals