-- Mathlib/Analysis/SpecialFunctions/Log/Summable.lean
lemma Complex.tendstoUniformlyOn_tsum_nat_log_one_add {α : Type*} {f : ℕ → α → ℂ} (K : Set α)
    {u : ℕ → ℝ} (hu : Summable u) (h : ∀ᶠ n in atTop, ∀ x ∈ K, ‖f n x‖ ≤ u n) :
    TendstoUniformlyOn (fun (n : ℕ) (a : α) => ∑ i ∈ Finset.range n,
    (Complex.log (1 + f i a))) (fun a => ∑' i : ℕ, Complex.log (1 + f i a)) atTop K

Proof state:
α : Type u_2
f : ℕ → α → ℂ
K : Set α
u : ℕ → ℝ
hu : Summable u
h : ∀ᶠ (n : ℕ) in atTop, ∀ x ∈ K, ‖f n x‖ ≤ u n
⊢ ∀ᶠ (n : ℕ) in atTop, ∀ x ∈ K, ‖log (1 + f n x)‖ ≤ 3 / 2 * u n

Tactic:
obtain ⟨N, hN⟩ := Metric.tendsto_atTop.mp (Summable.tendsto_atTop_zero hu) (1/2) (one_half_pos)

Result:
case intro
α : Type u_2
f : ℕ → α → ℂ
K : Set α
u : ℕ → ℝ
hu : Summable u
h : ∀ᶠ (n : ℕ) in atTop, ∀ x ∈ K, ‖f n x‖ ≤ u n
N : ℕ
hN : ∀ n ≥ N, dist (u n) 0 < 1 / 2
⊢ ∀ᶠ (n : ℕ) in atTop, ∀ x ∈ K, ‖log (1 + f n x)‖ ≤ 3 / 2 * u n

Proof state:
α : Type u_2
f : ℕ → α → ℂ
K : Set α
u : ℕ → ℝ
hu : Summable u
N : ℕ
hN : ∀ (n : ℕ), N ≤ n → dist (u n) 0 < 1 / 2
N2 : ℕ
hN2 : ∀ (b : ℕ), N2 ≤ b → ∀ x ∈ K, ‖f b x‖ ≤ u b
n : ℕ
hn : N ⊔ N2 ≤ n
x : α
hx : x ∈ K
⊢ ‖f n x‖ ≤ 1 / 2

Tactic:
apply le_trans (le_trans (hN2 n (le_of_max_le_right hn) x hx)
(by simpa using Real.le_norm_self (u n))) (hN n (le_of_max_le_left hn)).le

Result:
no goals

Proof state:
α : Type u_2
f : ℕ → α → ℂ
K : Set α
u : ℕ → ℝ
hu : Summable u
N : ℕ
hN : ∀ (n : ℕ), N ≤ n → dist (u n) 0 < 1 / 2
N2 : ℕ
hN2 : ∀ (b : ℕ), N2 ≤ b → ∀ x ∈ K, ‖f b x‖ ≤ u b
n : ℕ
hn : N ⊔ N2 ≤ n
x : α
hx : x ∈ K
⊢ u n ≤ dist (u n) 0

Tactic:
simpa using Real.le_norm_self (u n)

Result:
no goals

Proof state:
α : Type u_2
f : ℕ → α → ℂ
K : Set α
u : ℕ → ℝ
hu : Summable u
h : ∀ᶠ (n : ℕ) in atTop, ∀ x ∈ K, ‖f n x‖ ≤ u n
⊢ TendstoUniformlyOn (fun n a => ∑ i ∈ Finset.range n, log (1 + f i a)) (fun a => ∑' (i : ℕ), log (1 + f i a)) atTop K

Tactic:
apply tendstoUniformlyOn_tsum_nat_eventually (hu.mul_left (3/2))

Result:
α : Type u_2
f : ℕ → α → ℂ
K : Set α
u : ℕ → ℝ
hu : Summable u
h : ∀ᶠ (n : ℕ) in atTop, ∀ x ∈ K, ‖f n x‖ ≤ u n
⊢ ∀ᶠ (n : ℕ) in atTop, ∀ x ∈ K, ‖log (1 + f n x)‖ ≤ 3 / 2 * u n

Proof state:
case intro.intro
α : Type u_2
f : ℕ → α → ℂ
K : Set α
u : ℕ → ℝ
hu : Summable u
N : ℕ
hN : ∀ (n : ℕ), N ≤ n → dist (u n) 0 < 1 / 2
N2 : ℕ
hN2 : ∀ (b : ℕ), N2 ≤ b → ∀ x ∈ K, ‖f b x‖ ≤ u b
n : ℕ
hn : N ⊔ N2 ≤ n
x : α
hx : x ∈ K
⊢ 3 / 2 * ‖f n x‖ ≤ 3 / 2 * u n

Tactic:
simp only [Nat.ofNat_pos, div_pos_iff_of_pos_left, mul_le_mul_left]

Result:
case intro.intro
α : Type u_2
f : ℕ → α → ℂ
K : Set α
u : ℕ → ℝ
hu : Summable u
N : ℕ
hN : ∀ (n : ℕ), N ≤ n → dist (u n) 0 < 1 / 2
N2 : ℕ
hN2 : ∀ (b : ℕ), N2 ≤ b → ∀ x ∈ K, ‖f b x‖ ≤ u b
n : ℕ
hn : N ⊔ N2 ≤ n
x : α
hx : x ∈ K
⊢ ‖f n x‖ ≤ u n

Proof state:
case intro
α : Type u_2
f : ℕ → α → ℂ
K : Set α
u : ℕ → ℝ
hu : Summable u
N : ℕ
h : ∃ a, ∀ (b : ℕ), a ≤ b → ∀ x ∈ K, ‖f b x‖ ≤ u b
hN : ∀ (n : ℕ), N ≤ n → dist (u n) 0 < 1 / 2
⊢ ∃ a, ∀ (b : ℕ), a ≤ b → ∀ x ∈ K, ‖log (1 + f b x)‖ ≤ 3 / 2 * u b

Tactic:
obtain ⟨N2, hN2⟩ := h

Result:
case intro.intro
α : Type u_2
f : ℕ → α → ℂ
K : Set α
u : ℕ → ℝ
hu : Summable u
N : ℕ
hN : ∀ (n : ℕ), N ≤ n → dist (u n) 0 < 1 / 2
N2 : ℕ
hN2 : ∀ (b : ℕ), N2 ≤ b → ∀ x ∈ K, ‖f b x‖ ≤ u b
⊢ ∃ a, ∀ (b : ℕ), a ≤ b → ∀ x ∈ K, ‖log (1 + f b x)‖ ≤ 3 / 2 * u b

Proof state:
case intro.intro
α : Type u_2
f : ℕ → α → ℂ
K : Set α
u : ℕ → ℝ
hu : Summable u
N : ℕ
hN : ∀ (n : ℕ), N ≤ n → dist (u n) 0 < 1 / 2
N2 : ℕ
hN2 : ∀ (b : ℕ), N2 ≤ b → ∀ x ∈ K, ‖f b x‖ ≤ u b
⊢ ∃ a, ∀ (b : ℕ), a ≤ b → ∀ x ∈ K, ‖log (1 + f b x)‖ ≤ 3 / 2 * u b

Tactic:
refine ⟨max N N2, fun n hn x hx => ?_⟩

Result:
case intro.intro
α : Type u_2
f : ℕ → α → ℂ
K : Set α
u : ℕ → ℝ
hu : Summable u
N : ℕ
hN : ∀ (n : ℕ), N ≤ n → dist (u n) 0 < 1 / 2
N2 : ℕ
hN2 : ∀ (b : ℕ), N2 ≤ b → ∀ x ∈ K, ‖f b x‖ ≤ u b
n : ℕ
hn : N ⊔ N2 ≤ n
x : α
hx : x ∈ K
⊢ ‖log (1 + f n x)‖ ≤ 3 / 2 * u n

Proof state:
case intro.intro
α : Type u_2
f : ℕ → α → ℂ
K : Set α
u : ℕ → ℝ
hu : Summable u
N : ℕ
hN : ∀ (n : ℕ), N ≤ n → dist (u n) 0 < 1 / 2
N2 : ℕ
hN2 : ∀ (b : ℕ), N2 ≤ b → ∀ x ∈ K, ‖f b x‖ ≤ u b
n : ℕ
hn : N ⊔ N2 ≤ n
x : α
hx : x ∈ K
⊢ ‖log (1 + f n x)‖ ≤ 3 / 2 * u n

Tactic:
apply le_trans (Complex.norm_log_one_add_half_le_self (z := (f n x)) ?_)

Result:
case intro.intro
α : Type u_2
f : ℕ → α → ℂ
K : Set α
u : ℕ → ℝ
hu : Summable u
N : ℕ
hN : ∀ (n : ℕ), N ≤ n → dist (u n) 0 < 1 / 2
N2 : ℕ
hN2 : ∀ (b : ℕ), N2 ≤ b → ∀ x ∈ K, ‖f b x‖ ≤ u b
n : ℕ
hn : N ⊔ N2 ≤ n
x : α
hx : x ∈ K
⊢ 3 / 2 * ‖f n x‖ ≤ 3 / 2 * u n

α : Type u_2
f : ℕ → α → ℂ
K : Set α
u : ℕ → ℝ
hu : Summable u
N : ℕ
hN : ∀ (n : ℕ), N ≤ n → dist (u n) 0 < 1 / 2
N2 : ℕ
hN2 : ∀ (b : ℕ), N2 ≤ b → ∀ x ∈ K, ‖f b x‖ ≤ u b
n : ℕ
hn : N ⊔ N2 ≤ n
x : α
hx : x ∈ K
⊢ ‖f n x‖ ≤ 1 / 2

Proof state:
case intro.intro
α : Type u_2
f : ℕ → α → ℂ
K : Set α
u : ℕ → ℝ
hu : Summable u
N : ℕ
hN : ∀ (n : ℕ), N ≤ n → dist (u n) 0 < 1 / 2
N2 : ℕ
hN2 : ∀ (b : ℕ), N2 ≤ b → ∀ x ∈ K, ‖f b x‖ ≤ u b
n : ℕ
hn : N ⊔ N2 ≤ n
x : α
hx : x ∈ K
⊢ ‖f n x‖ ≤ u n

Tactic:
exact hN2 n (le_of_max_le_right hn) x hx

Result:
no goals

Proof state:
case intro
α : Type u_2
f : ℕ → α → ℂ
K : Set α
u : ℕ → ℝ
hu : Summable u
h : ∀ᶠ (n : ℕ) in atTop, ∀ x ∈ K, ‖f n x‖ ≤ u n
N : ℕ
hN : ∀ n ≥ N, dist (u n) 0 < 1 / 2
⊢ ∀ᶠ (n : ℕ) in atTop, ∀ x ∈ K, ‖log (1 + f n x)‖ ≤ 3 / 2 * u n

Tactic:
simp only [eventually_atTop, ge_iff_le] at *

Result:
case intro
α : Type u_2
f : ℕ → α → ℂ
K : Set α
u : ℕ → ℝ
hu : Summable u
N : ℕ
h : ∃ a, ∀ (b : ℕ), a ≤ b → ∀ x ∈ K, ‖f b x‖ ≤ u b
hN : ∀ (n : ℕ), N ≤ n → dist (u n) 0 < 1 / 2
⊢ ∃ a, ∀ (b : ℕ), a ≤ b → ∀ x ∈ K, ‖log (1 + f b x)‖ ≤ 3 / 2 * u b