-- Mathlib/NumberTheory/LSeries/Positivity.lean
/-- If all values of a `ℂ`-valued arithmetic function are nonnegative reals and `x` is a
real number in the domain of absolute convergence, then the `n`th iterated derivative
of the associated L-series is nonnegative real when `n` is even and nonpositive real
when `n` is odd. -/
lemma iteratedDeriv_alternating {a : ℕ → ℂ} (hn : 0 ≤ a) {x : ℝ}
    (h : LSeries.abscissaOfAbsConv a < x) (n : ℕ) :
    0 ≤ (-1) ^ n * iteratedDeriv n (LSeries a) x

Proof state:
case isFalse
a : ℕ → ℂ
hn : 0 ≤ a
x : ℝ
h : abscissaOfAbsConv a < ↑x
n k : ℕ
h✝ : ¬k = 0
⊢ 0 ≤ logMul^[n] a k

Tactic:
induction n with
| zero => simpa only [Function.iterate_zero, id_eq] using hn k
| succ n IH =>
    rw [Function.iterate_succ_apply']
    refine mul_nonneg ?_ IH
    simp only [← natCast_log, zero_le_real, Real.log_natCast_nonneg]

Result:
no goals

Proof state:
a : ℕ → ℂ
hn : 0 ≤ a
x : ℝ
h : abscissaOfAbsConv a < ↑x
n : ℕ
⊢ 0 ≤ ∑' (n_1 : ℕ), term (logMul^[n] a) (↑x) n_1

Tactic:
refine tsum_nonneg fun k ↦ ?_

Result:
a : ℕ → ℂ
hn : 0 ≤ a
x : ℝ
h : abscissaOfAbsConv a < ↑x
n k : ℕ
⊢ 0 ≤ term (logMul^[n] a) (↑x) k

Proof state:
case isFalse.succ
a : ℕ → ℂ
hn : 0 ≤ a
x : ℝ
h : abscissaOfAbsConv a < ↑x
k : ℕ
h✝ : ¬k = 0
n : ℕ
IH : 0 ≤ logMul^[n] a k
⊢ 0 ≤ log ↑k

Tactic:
simp only [← natCast_log, zero_le_real, Real.log_natCast_nonneg]

Result:
no goals

Proof state:
a : ℕ → ℂ
hn : 0 ≤ a
x : ℝ
h : abscissaOfAbsConv a < ↑x
n k : ℕ
⊢ 0 ≤ if k = 0 then 0 else logMul^[n] a k / ↑k ^ ↑x

Tactic:
split

Result:
case isTrue
a : ℕ → ℂ
hn : 0 ≤ a
x : ℝ
h : abscissaOfAbsConv a < ↑x
n k : ℕ
h✝ : k = 0
⊢ 0 ≤ 0

case isFalse
a : ℕ → ℂ
hn : 0 ≤ a
x : ℝ
h : abscissaOfAbsConv a < ↑x
n k : ℕ
h✝ : ¬k = 0
⊢ 0 ≤ logMul^[n] a k / ↑k ^ ↑x

Proof state:
a : ℕ → ℂ
hn : 0 ≤ a
x : ℝ
h : abscissaOfAbsConv a < ↑x
n k : ℕ
h✝ : ¬k = 0
⊢ k ≠ 0

Tactic:
assumption

Result:
no goals

Proof state:
a : ℕ → ℂ
hn : 0 ≤ a
x : ℝ
h : abscissaOfAbsConv a < ↑x
n k : ℕ
⊢ 0 ≤ term (logMul^[n] a) (↑x) k

Tactic:
rw [LSeries.term_def]

Result:
a : ℕ → ℂ
hn : 0 ≤ a
x : ℝ
h : abscissaOfAbsConv a < ↑x
n k : ℕ
⊢ 0 ≤ if k = 0 then 0 else logMul^[n] a k / ↑k ^ ↑x

Proof state:
case isFalse.succ
a : ℕ → ℂ
hn : 0 ≤ a
x : ℝ
h : abscissaOfAbsConv a < ↑x
k : ℕ
h✝ : ¬k = 0
n : ℕ
IH : 0 ≤ logMul^[n] a k
⊢ 0 ≤ logMul^[n + 1] a k

Tactic:
rw [Function.iterate_succ_apply']

Result:
case isFalse.succ
a : ℕ → ℂ
hn : 0 ≤ a
x : ℝ
h : abscissaOfAbsConv a < ↑x
k : ℕ
h✝ : ¬k = 0
n : ℕ
IH : 0 ≤ logMul^[n] a k
⊢ 0 ≤ logMul (logMul^[n] a) k

Proof state:
a : ℕ → ℂ
hn : 0 ≤ a
x : ℝ
h : abscissaOfAbsConv a < ↑x
n : ℕ
⊢ 0 ≤ (-1) ^ n * iteratedDeriv n (LSeries a) ↑x

Tactic:
rw [LSeries_iteratedDeriv _ h, LSeries, ← mul_assoc, ← pow_add, Even.neg_one_pow ⟨n, rfl⟩,
  one_mul]

Result:
a : ℕ → ℂ
hn : 0 ≤ a
x : ℝ
h : abscissaOfAbsConv a < ↑x
n : ℕ
⊢ 0 ≤ ∑' (n_1 : ℕ), term (logMul^[n] a) (↑x) n_1

Proof state:
case isFalse
a : ℕ → ℂ
hn : 0 ≤ a
x : ℝ
h : abscissaOfAbsConv a < ↑x
n k : ℕ
h✝ : ¬k = 0
⊢ 0 ≤ logMul^[n] a k / ↑k ^ ↑x

Tactic:
refine mul_nonneg ?_ <| (inv_natCast_cpow_ofReal_pos (by assumption) x).le

Result:
case isFalse
a : ℕ → ℂ
hn : 0 ≤ a
x : ℝ
h : abscissaOfAbsConv a < ↑x
n k : ℕ
h✝ : ¬k = 0
⊢ 0 ≤ logMul^[n] a k

Proof state:
case isFalse.succ
a : ℕ → ℂ
hn : 0 ≤ a
x : ℝ
h : abscissaOfAbsConv a < ↑x
k : ℕ
h✝ : ¬k = 0
n : ℕ
IH : 0 ≤ logMul^[n] a k
⊢ 0 ≤ logMul (logMul^[n] a) k

Tactic:
refine mul_nonneg ?_ IH

Result:
case isFalse.succ
a : ℕ → ℂ
hn : 0 ≤ a
x : ℝ
h : abscissaOfAbsConv a < ↑x
k : ℕ
h✝ : ¬k = 0
n : ℕ
IH : 0 ≤ logMul^[n] a k
⊢ 0 ≤ log ↑k

Proof state:
case isTrue
a : ℕ → ℂ
hn : 0 ≤ a
x : ℝ
h : abscissaOfAbsConv a < ↑x
n k : ℕ
h✝ : k = 0
⊢ 0 ≤ 0

Tactic:
exact le_rfl

Result:
no goals

Proof state:
case isFalse.zero
a : ℕ → ℂ
hn : 0 ≤ a
x : ℝ
h : abscissaOfAbsConv a < ↑x
k : ℕ
h✝ : ¬k = 0
⊢ 0 ≤ logMul^[0] a k

Tactic:
simpa only [Function.iterate_zero, id_eq] using hn k

Result:
no goals