Theorem: re_log_comb_nonneg' (EulerProducts/PNT.lean)

State before:
a : ℝ
ha₀ : 0 ≤ a
ha₁ : a < 1
z : ℂ
hz : ‖z‖ = 1
⊢ 0 ≤ 3 * (-(1 - ↑a).log).re + 4 * (-(1 - ↑a * z).log).re + (-(1 - ↑a * z ^ 2).log).re
Tactic:
have hac₀ : ‖(a : ℂ)‖ < 1 := by
  simp only [norm_eq_abs, abs_ofReal, _root_.abs_of_nonneg ha₀, ha₁]
State after:
a : ℝ
ha₀ : 0 ≤ a
ha₁ : a < 1
z : ℂ
hz : ‖z‖ = 1
hac₀ : ‖↑a‖ < 1
⊢ 0 ≤ 3 * (-(1 - ↑a).log).re + 4 * (-(1 - ↑a * z).log).re + (-(1 - ↑a * z ^ 2).log).re

State before:
a : ℝ
ha₀ : 0 ≤ a
ha₁ : a < 1
z : ℂ
hz : ‖z‖ = 1
hac₀ : ‖↑a‖ < 1
⊢ 0 ≤ 3 * (-(1 - ↑a).log).re + 4 * (-(1 - ↑a * z).log).re + (-(1 - ↑a * z ^ 2).log).re
Tactic:
have hac₁ : ‖a * z‖ < 1 := by rwa [norm_mul, hz, mul_one]
State after:
a : ℝ
ha₀ : 0 ≤ a
ha₁ : a < 1
z : ℂ
hz : ‖z‖ = 1
hac₀ : ‖↑a‖ < 1
hac₁ : ‖↑a * z‖ < 1
⊢ 0 ≤ 3 * (-(1 - ↑a).log).re + 4 * (-(1 - ↑a * z).log).re + (-(1 - ↑a * z ^ 2).log).re

State before:
a : ℝ
ha₀ : 0 ≤ a
ha₁ : a < 1
z : ℂ
hz : ‖z‖ = 1
hac₀ : ‖↑a‖ < 1
hac₁ : ‖↑a * z‖ < 1
⊢ 0 ≤ 3 * (-(1 - ↑a).log).re + 4 * (-(1 - ↑a * z).log).re + (-(1 - ↑a * z ^ 2).log).re
Tactic:
have hac₂ : ‖a * z ^ 2‖ < 1 := by rwa [norm_mul, norm_pow, hz, one_pow, mul_one]
State after:
a : ℝ
ha₀ : 0 ≤ a
ha₁ : a < 1
z : ℂ
hz : ‖z‖ = 1
hac₀ : ‖↑a‖ < 1
hac₁ : ‖↑a * z‖ < 1
hac₂ : ‖↑a * z ^ 2‖ < 1
⊢ 0 ≤ 3 * (-(1 - ↑a).log).re + 4 * (-(1 - ↑a * z).log).re + (-(1 - ↑a * z ^ 2).log).re

State before:
a : ℝ
ha₀ : 0 ≤ a
ha₁ : a < 1
z : ℂ
hz : ‖z‖ = 1
hac₀ : ‖↑a‖ < 1
hac₁ : ‖↑a * z‖ < 1
hac₂ : ‖↑a * z ^ 2‖ < 1
⊢ 0 ≤ 3 * (-(1 - ↑a).log).re + 4 * (-(1 - ↑a * z).log).re + (-(1 - ↑a * z ^ 2).log).re
Tactic:
have H₀ := (hasSum_re <| hasSum_taylorSeries_neg_log hac₀).mul_left 3
State after:
a : ℝ
ha₀ : 0 ≤ a
ha₁ : a < 1
z : ℂ
hz : ‖z‖ = 1
hac₀ : ‖↑a‖ < 1
hac₁ : ‖↑a * z‖ < 1
hac₂ : ‖↑a * z ^ 2‖ < 1
H₀ : HasSum (fun i => 3 * (↑a ^ i / ↑i).re) (3 * (-(1 - ↑a).log).re)
⊢ 0 ≤ 3 * (-(1 - ↑a).log).re + 4 * (-(1 - ↑a * z).log).re + (-(1 - ↑a * z ^ 2).log).re

State before:
a : ℝ
ha₀ : 0 ≤ a
ha₁ : a < 1
z : ℂ
hz : ‖z‖ = 1
hac₀ : ‖↑a‖ < 1
hac₁ : ‖↑a * z‖ < 1
hac₂ : ‖↑a * z ^ 2‖ < 1
H₀ : HasSum (fun i => 3 * (↑a ^ i / ↑i).re) (3 * (-(1 - ↑a).log).re)
⊢ 0 ≤ 3 * (-(1 - ↑a).log).re + 4 * (-(1 - ↑a * z).log).re + (-(1 - ↑a * z ^ 2).log).re
Tactic:
have H₁ := (hasSum_re <| hasSum_taylorSeries_neg_log hac₁).mul_left 4
State after:
a : ℝ
ha₀ : 0 ≤ a
ha₁ : a < 1
z : ℂ
hz : ‖z‖ = 1
hac₀ : ‖↑a‖ < 1
hac₁ : ‖↑a * z‖ < 1
hac₂ : ‖↑a * z ^ 2‖ < 1
H₀ : HasSum (fun i => 3 * (↑a ^ i / ↑i).re) (3 * (-(1 - ↑a).log).re)
H₁ : HasSum (fun i => 4 * ((↑a * z) ^ i / ↑i).re) (4 * (-(1 - ↑a * z).log).re)
⊢ 0 ≤ 3 * (-(1 - ↑a).log).re + 4 * (-(1 - ↑a * z).log).re + (-(1 - ↑a * z ^ 2).log).re

State before:
a : ℝ
ha₀ : 0 ≤ a
ha₁ : a < 1
z : ℂ
hz : ‖z‖ = 1
hac₀ : ‖↑a‖ < 1
hac₁ : ‖↑a * z‖ < 1
hac₂ : ‖↑a * z ^ 2‖ < 1
H₀ : HasSum (fun i => 3 * (↑a ^ i / ↑i).re) (3 * (-(1 - ↑a).log).re)
H₁ : HasSum (fun i => 4 * ((↑a * z) ^ i / ↑i).re) (4 * (-(1 - ↑a * z).log).re)
⊢ 0 ≤ 3 * (-(1 - ↑a).log).re + 4 * (-(1 - ↑a * z).log).re + (-(1 - ↑a * z ^ 2).log).re
Tactic:
have H₂ := hasSum_re <| hasSum_taylorSeries_neg_log hac₂
State after:
a : ℝ
ha₀ : 0 ≤ a
ha₁ : a < 1
z : ℂ
hz : ‖z‖ = 1
hac₀ : ‖↑a‖ < 1
hac₁ : ‖↑a * z‖ < 1
hac₂ : ‖↑a * z ^ 2‖ < 1
H₀ : HasSum (fun i => 3 * (↑a ^ i / ↑i).re) (3 * (-(1 - ↑a).log).re)
H₁ : HasSum (fun i => 4 * ((↑a * z) ^ i / ↑i).re) (4 * (-(1 - ↑a * z).log).re)
H₂ : HasSum (fun x => ((↑a * z ^ 2) ^ x / ↑x).re) (-(1 - ↑a * z ^ 2).log).re
⊢ 0 ≤ 3 * (-(1 - ↑a).log).re + 4 * (-(1 - ↑a * z).log).re + (-(1 - ↑a * z ^ 2).log).re

State before:
a : ℝ
ha₀ : 0 ≤ a
ha₁ : a < 1
z : ℂ
hz : ‖z‖ = 1
hac₀ : ‖↑a‖ < 1
hac₁ : ‖↑a * z‖ < 1
hac₂ : ‖↑a * z ^ 2‖ < 1
H₀ : HasSum (fun i => 3 * (↑a ^ i / ↑i).re) (3 * (-(1 - ↑a).log).re)
H₁ : HasSum (fun i => 4 * ((↑a * z) ^ i / ↑i).re) (4 * (-(1 - ↑a * z).log).re)
H₂ : HasSum (fun x => ((↑a * z ^ 2) ^ x / ↑x).re) (-(1 - ↑a * z ^ 2).log).re
⊢ 0 ≤ 3 * (-(1 - ↑a).log).re + 4 * (-(1 - ↑a * z).log).re + (-(1 - ↑a * z ^ 2).log).re
Tactic:
rw [← ((H₀.add H₁).add H₂).tsum_eq]
State after:
a : ℝ
ha₀ : 0 ≤ a
ha₁ : a < 1
z : ℂ
hz : ‖z‖ = 1
hac₀ : ‖↑a‖ < 1
hac₁ : ‖↑a * z‖ < 1
hac₂ : ‖↑a * z ^ 2‖ < 1
H₀ : HasSum (fun i => 3 * (↑a ^ i / ↑i).re) (3 * (-(1 - ↑a).log).re)
H₁ : HasSum (fun i => 4 * ((↑a * z) ^ i / ↑i).re) (4 * (-(1 - ↑a * z).log).re)
H₂ : HasSum (fun x => ((↑a * z ^ 2) ^ x / ↑x).re) (-(1 - ↑a * z ^ 2).log).re
⊢ 0 ≤ ∑' (b : ℕ), (3 * (↑a ^ b / ↑b).re + 4 * ((↑a * z) ^ b / ↑b).re + ((↑a * z ^ 2) ^ b / ↑b).re)

State before:
a : ℝ
ha₀ : 0 ≤ a
ha₁ : a < 1
z : ℂ
hz : ‖z‖ = 1
hac₀ : ‖↑a‖ < 1
hac₁ : ‖↑a * z‖ < 1
hac₂ : ‖↑a * z ^ 2‖ < 1
H₀ : HasSum (fun i => 3 * (↑a ^ i / ↑i).re) (3 * (-(1 - ↑a).log).re)
H₁ : HasSum (fun i => 4 * ((↑a * z) ^ i / ↑i).re) (4 * (-(1 - ↑a * z).log).re)
H₂ : HasSum (fun x => ((↑a * z ^ 2) ^ x / ↑x).re) (-(1 - ↑a * z ^ 2).log).re
⊢ 0 ≤ ∑' (b : ℕ), (3 * (↑a ^ b / ↑b).re + 4 * ((↑a * z) ^ b / ↑b).re + ((↑a * z ^ 2) ^ b / ↑b).re)
Tactic:
clear H₀ H₁ H₂
State after:
a : ℝ
ha₀ : 0 ≤ a
ha₁ : a < 1
z : ℂ
hz : ‖z‖ = 1
hac₀ : ‖↑a‖ < 1
hac₁ : ‖↑a * z‖ < 1
hac₂ : ‖↑a * z ^ 2‖ < 1
⊢ 0 ≤ ∑' (b : ℕ), (3 * (↑a ^ b / ↑b).re + 4 * ((↑a * z) ^ b / ↑b).re + ((↑a * z ^ 2) ^ b / ↑b).re)

State before:
a : ℝ
ha₀ : 0 ≤ a
ha₁ : a < 1
z : ℂ
hz : ‖z‖ = 1
hac₀ : ‖↑a‖ < 1
hac₁ : ‖↑a * z‖ < 1
hac₂ : ‖↑a * z ^ 2‖ < 1
⊢ 0 ≤ ∑' (b : ℕ), (3 * (↑a ^ b / ↑b).re + 4 * ((↑a * z) ^ b / ↑b).re + ((↑a * z ^ 2) ^ b / ↑b).re)
Tactic:
refine tsum_nonneg fun n ↦ ?_
State after:
a : ℝ
ha₀ : 0 ≤ a
ha₁ : a < 1
z : ℂ
hz : ‖z‖ = 1
hac₀ : ‖↑a‖ < 1
hac₁ : ‖↑a * z‖ < 1
hac₂ : ‖↑a * z ^ 2‖ < 1
n : ℕ
⊢ 0 ≤ 3 * (↑a ^ n / ↑n).re + 4 * ((↑a * z) ^ n / ↑n).re + ((↑a * z ^ 2) ^ n / ↑n).re

State before:
a : ℝ
ha₀ : 0 ≤ a
ha₁ : a < 1
z : ℂ
hz : ‖z‖ = 1
hac₀ : ‖↑a‖ < 1
hac₁ : ‖↑a * z‖ < 1
hac₂ : ‖↑a * z ^ 2‖ < 1
n : ℕ
⊢ 0 ≤ 3 * (↑a ^ n / ↑n).re + 4 * ((↑a * z) ^ n / ↑n).re + ((↑a * z ^ 2) ^ n / ↑n).re
Tactic:
simp only [mul_pow, ← ofReal_pow, div_natCast_re, ofReal_re, mul_re, ofReal_im, zero_mul,
  sub_zero]
State after:
a : ℝ
ha₀ : 0 ≤ a
ha₁ : a < 1
z : ℂ
hz : ‖z‖ = 1
hac₀ : ‖↑a‖ < 1
hac₁ : ‖↑a * z‖ < 1
hac₂ : ‖↑a * z ^ 2‖ < 1
n : ℕ
⊢ 0 ≤ 3 * (a ^ n / ↑n) + 4 * (a ^ n * (z ^ n).re / ↑n) + a ^ n * ((z ^ 2) ^ n).re / ↑n

State before:
a : ℝ
ha₀ : 0 ≤ a
ha₁ : a < 1
z : ℂ
hz : ‖z‖ = 1
hac₀ : ‖↑a‖ < 1
hac₁ : ‖↑a * z‖ < 1
hac₂ : ‖↑a * z ^ 2‖ < 1
n : ℕ
⊢ 0 ≤ 3 * (a ^ n / ↑n) + 4 * (a ^ n * (z ^ n).re / ↑n) + a ^ n * ((z ^ 2) ^ n).re / ↑n
Tactic:
rcases n.eq_zero_or_pos with rfl | hn
State after:
case inl
a : ℝ
ha₀ : 0 ≤ a
ha₁ : a < 1
z : ℂ
hz : ‖z‖ = 1
hac₀ : ‖↑a‖ < 1
hac₁ : ‖↑a * z‖ < 1
hac₂ : ‖↑a * z ^ 2‖ < 1
⊢ 0 ≤ 3 * (a ^ 0 / ↑0) + 4 * (a ^ 0 * (z ^ 0).re / ↑0) + a ^ 0 * ((z ^ 2) ^ 0).re / ↑0

case inr
a : ℝ
ha₀ : 0 ≤ a
ha₁ : a < 1
z : ℂ
hz : ‖z‖ = 1
hac₀ : ‖↑a‖ < 1
hac₁ : ‖↑a * z‖ < 1
hac₂ : ‖↑a * z ^ 2‖ < 1
n : ℕ
hn : n > 0
⊢ 0 ≤ 3 * (a ^ n / ↑n) + 4 * (a ^ n * (z ^ n).re / ↑n) + a ^ n * ((z ^ 2) ^ n).re / ↑n

State before:
case inr
a : ℝ
ha₀ : 0 ≤ a
ha₁ : a < 1
z : ℂ
hz : ‖z‖ = 1
hac₀ : ‖↑a‖ < 1
hac₁ : ‖↑a * z‖ < 1
hac₂ : ‖↑a * z ^ 2‖ < 1
n : ℕ
hn : n > 0
⊢ 0 ≤ 3 * (a ^ n / ↑n) + 4 * (a ^ n * (z ^ n).re / ↑n) + a ^ n * ((z ^ 2) ^ n).re / ↑n
Tactic:
field_simp
State after:
case inr
a : ℝ
ha₀ : 0 ≤ a
ha₁ : a < 1
z : ℂ
hz : ‖z‖ = 1
hac₀ : ‖↑a‖ < 1
hac₁ : ‖↑a * z‖ < 1
hac₂ : ‖↑a * z ^ 2‖ < 1
n : ℕ
hn : n > 0
⊢ 0 ≤ (3 * a ^ n + 4 * (a ^ n * (z ^ n).re) + a ^ n * ((z ^ 2) ^ n).re) / ↑n

State before:
case inr
a : ℝ
ha₀ : 0 ≤ a
ha₁ : a < 1
z : ℂ
hz : ‖z‖ = 1
hac₀ : ‖↑a‖ < 1
hac₁ : ‖↑a * z‖ < 1
hac₂ : ‖↑a * z ^ 2‖ < 1
n : ℕ
hn : n > 0
⊢ 0 ≤ (3 * a ^ n + 4 * (a ^ n * (z ^ n).re) + a ^ n * ((z ^ 2) ^ n).re) / ↑n
Tactic:
refine div_nonneg ?_ n.cast_nonneg
State after:
case inr
a : ℝ
ha₀ : 0 ≤ a
ha₁ : a < 1
z : ℂ
hz : ‖z‖ = 1
hac₀ : ‖↑a‖ < 1
hac₁ : ‖↑a * z‖ < 1
hac₂ : ‖↑a * z ^ 2‖ < 1
n : ℕ
hn : n > 0
⊢ 0 ≤ 3 * a ^ n + 4 * (a ^ n * (z ^ n).re) + a ^ n * ((z ^ 2) ^ n).re

State before:
case inr
a : ℝ
ha₀ : 0 ≤ a
ha₁ : a < 1
z : ℂ
hz : ‖z‖ = 1
hac₀ : ‖↑a‖ < 1
hac₁ : ‖↑a * z‖ < 1
hac₂ : ‖↑a * z ^ 2‖ < 1
n : ℕ
hn : n > 0
⊢ 0 ≤ 3 * a ^ n + 4 * (a ^ n * (z ^ n).re) + a ^ n * ((z ^ 2) ^ n).re
Tactic:
rw [← pow_mul, pow_mul', sq, mul_re, ← sq, ← sq, ← sq_abs_sub_sq_re, ← norm_eq_abs, norm_pow, hz]
State after:
case inr
a : ℝ
ha₀ : 0 ≤ a
ha₁ : a < 1
z : ℂ
hz : ‖z‖ = 1
hac₀ : ‖↑a‖ < 1
hac₁ : ‖↑a * z‖ < 1
hac₂ : ‖↑a * z ^ 2‖ < 1
n : ℕ
hn : n > 0
⊢ 0 ≤ 3 * a ^ n + 4 * (a ^ n * (z ^ n).re) + a ^ n * ((z ^ n).re ^ 2 - ((1 ^ n) ^ 2 - (z ^ n).re ^ 2))

State before:
case inr
a : ℝ
ha₀ : 0 ≤ a
ha₁ : a < 1
z : ℂ
hz : ‖z‖ = 1
hac₀ : ‖↑a‖ < 1
hac₁ : ‖↑a * z‖ < 1
hac₂ : ‖↑a * z ^ 2‖ < 1
n : ℕ
hn : n > 0
⊢ 0 ≤ 3 * a ^ n + 4 * (a ^ n * (z ^ n).re) + a ^ n * ((z ^ n).re ^ 2 - ((1 ^ n) ^ 2 - (z ^ n).re ^ 2))
Tactic:
calc
  0 ≤ 2 * a ^ n * ((z ^ n).re + 1) ^ 2 := by positivity
  _ = _  := by ring
State after:
no goals

State before:
a : ℝ
ha₀ : 0 ≤ a
ha₁ : a < 1
z : ℂ
hz : ‖z‖ = 1
⊢ ‖↑a‖ < 1
Tactic:
simp only [norm_eq_abs, abs_ofReal, _root_.abs_of_nonneg ha₀, ha₁]
State after:
no goals

State before:
a : ℝ
ha₀ : 0 ≤ a
ha₁ : a < 1
z : ℂ
hz : ‖z‖ = 1
hac₀ : ‖↑a‖ < 1
⊢ ‖↑a * z‖ < 1
Tactic:
rwa [norm_mul, hz, mul_one]
State after:
no goals

State before:
a : ℝ
ha₀ : 0 ≤ a
ha₁ : a < 1
z : ℂ
hz : ‖z‖ = 1
hac₀ : ‖↑a‖ < 1
hac₁ : ‖↑a * z‖ < 1
⊢ ‖↑a * z ^ 2‖ < 1
Tactic:
rwa [norm_mul, norm_pow, hz, one_pow, mul_one]
State after:
no goals

State before:
case inl
a : ℝ
ha₀ : 0 ≤ a
ha₁ : a < 1
z : ℂ
hz : ‖z‖ = 1
hac₀ : ‖↑a‖ < 1
hac₁ : ‖↑a * z‖ < 1
hac₂ : ‖↑a * z ^ 2‖ < 1
⊢ 0 ≤ 3 * (a ^ 0 / ↑0) + 4 * (a ^ 0 * (z ^ 0).re / ↑0) + a ^ 0 * ((z ^ 2) ^ 0).re / ↑0
Tactic:
simp
State after:
no goals

State before:
a : ℝ
ha₀ : 0 ≤ a
ha₁ : a < 1
z : ℂ
hz : ‖z‖ = 1
hac₀ : ‖↑a‖ < 1
hac₁ : ‖↑a * z‖ < 1
hac₂ : ‖↑a * z ^ 2‖ < 1
n : ℕ
hn : n > 0
⊢ 0 ≤ 2 * a ^ n * ((z ^ n).re + 1) ^ 2
Tactic:
positivity
State after:
no goals

State before:
a : ℝ
ha₀ : 0 ≤ a
ha₁ : a < 1
z : ℂ
hz : ‖z‖ = 1
hac₀ : ‖↑a‖ < 1
hac₁ : ‖↑a * z‖ < 1
hac₂ : ‖↑a * z ^ 2‖ < 1
n : ℕ
hn : n > 0
⊢ 2 * a ^ n * ((z ^ n).re + 1) ^ 2 =
    3 * a ^ n + 4 * (a ^ n * (z ^ n).re) + a ^ n * ((z ^ n).re ^ 2 - ((1 ^ n) ^ 2 - (z ^ n).re ^ 2))
Tactic:
ring
State after:
no goals