-- Mathlib/Analysis/SpecialFunctions/Log/PosLog.lean
theorem posLog_sum {α : Type*} (s : Finset α) (f : α → ℝ) :
    log⁺ (∑ t ∈ s, f t) ≤ log (s.card) + ∑ t ∈ s, log⁺ (f t)

Proof state:
case neg
α : Type u_1
s : Finset α
f : α → ℝ
hs : ¬s = ∅
⊢ log⁺ (∑ t ∈ s, f t) ≤ log ↑s.card + ∑ t ∈ s, log⁺ (f t)

Tactic:
obtain ⟨t_max, ht_max⟩ := s.exists_max_image (fun t ↦ |f t|)
  (Finset.nonempty_iff_ne_empty.mpr hs)

Result:
case neg.intro
α : Type u_1
s : Finset α
f : α → ℝ
hs : ¬s = ∅
t_max : α
ht_max : t_max ∈ s ∧ ∀ x' ∈ s, |f x'| ≤ |f t_max|
⊢ log⁺ (∑ t ∈ s, f t) ≤ log ↑s.card + ∑ t ∈ s, log⁺ (f t)

Proof state:
α : Type u_1
s : Finset α
f : α → ℝ
⊢ log⁺ (∑ t ∈ s, f t) ≤ log ↑s.card + ∑ t ∈ s, log⁺ (f t)

Tactic:
by_cases hs : s = ∅

Result:
case pos
α : Type u_1
s : Finset α
f : α → ℝ
hs : s = ∅
⊢ log⁺ (∑ t ∈ s, f t) ≤ log ↑s.card + ∑ t ∈ s, log⁺ (f t)

case neg
α : Type u_1
s : Finset α
f : α → ℝ
hs : ¬s = ∅
⊢ log⁺ (∑ t ∈ s, f t) ≤ log ↑s.card + ∑ t ∈ s, log⁺ (f t)

Proof state:
α : Type u_1
s : Finset α
f : α → ℝ
hs : ¬s = ∅
t_max : α
ht_max : t_max ∈ s ∧ ∀ x' ∈ s, |f x'| ≤ |f t_max|
⊢ ∑ t ∈ s, |f t| ∈ Set.Ici 0

Tactic:
simp [Finset.sum_nonneg]

Result:
no goals

Proof state:
α : Type u_1
s : Finset α
f : α → ℝ
hs : ¬s = ∅
t_max : α
ht_max : t_max ∈ s ∧ ∀ x' ∈ s, |f x'| ≤ |f t_max|
⊢ log⁺ (∑ t ∈ s, |f t|) ≤ log⁺ (∑ t ∈ s, |f t_max|)

Tactic:
apply monotoneOn_posLog (by simp [Finset.sum_nonneg]) (by simp [Finset.sum_nonneg]; positivity)

Result:
α : Type u_1
s : Finset α
f : α → ℝ
hs : ¬s = ∅
t_max : α
ht_max : t_max ∈ s ∧ ∀ x' ∈ s, |f x'| ≤ |f t_max|
⊢ ∑ t ∈ s, |f t| ≤ ∑ t ∈ s, |f t_max|

Proof state:
α : Type u_1
s : Finset α
f : α → ℝ
hs : ¬s = ∅
t_max : α
ht_max : t_max ∈ s ∧ ∀ x' ∈ s, |f x'| ≤ |f t_max|
⊢ log ↑s.card + log⁺ |f t_max| ≤ log ↑s.card + ∑ t ∈ s, log⁺ (f t)

Tactic:
gcongr

Result:
case bc
α : Type u_1
s : Finset α
f : α → ℝ
hs : ¬s = ∅
t_max : α
ht_max : t_max ∈ s ∧ ∀ x' ∈ s, |f x'| ≤ |f t_max|
⊢ log⁺ |f t_max| ≤ ∑ t ∈ s, log⁺ (f t)

Proof state:
α : Type u_1
s : Finset α
f : α → ℝ
hs : ¬s = ∅
t_max : α
ht_max : t_max ∈ s ∧ ∀ x' ∈ s, |f x'| ≤ |f t_max|
⊢ log⁺ (∑ t ∈ s, f t) = log⁺ |∑ t ∈ s, f t|

Tactic:
rw [Real.posLog_abs]

Result:
no goals

Proof state:
α : Type u_1
s : Finset α
f : α → ℝ
hs : ¬s = ∅
t_max : α
ht_max : t_max ∈ s ∧ ∀ x' ∈ s, |f x'| ≤ |f t_max|
⊢ 0 ≤ ↑s.card * |f t_max|

Tactic:
positivity

Result:
no goals

Proof state:
α : Type u_1
s : Finset α
f : α → ℝ
hs : ¬s = ∅
t_max : α
ht_max : t_max ∈ s ∧ ∀ x' ∈ s, |f x'| ≤ |f t_max|
⊢ |∑ t ∈ s, f t| ≤ ∑ t ∈ s, |f t|

Tactic:
simp [Finset.abs_sum_le_sum_abs]

Result:
no goals

Proof state:
case bc
α : Type u_1
s : Finset α
f : α → ℝ
hs : ¬s = ∅
t_max : α
ht_max : t_max ∈ s ∧ ∀ x' ∈ s, |f x'| ≤ |f t_max|
⊢ log⁺ (f t_max) ≤ ∑ t ∈ s, log⁺ (f t)

Tactic:
apply Finset.single_le_sum (fun _ _ ↦ posLog_nonneg) ht_max.1

Result:
no goals

Proof state:
α : Type u_1
s : Finset α
f : α → ℝ
hs : ¬s = ∅
t_max : α
ht_max : t_max ∈ s ∧ ∀ x' ∈ s, |f x'| ≤ |f t_max|
⊢ |∑ t ∈ s, f t| ∈ Set.Ici 0

Tactic:
simp

Result:
no goals

Proof state:
α : Type u_1
s : Finset α
f : α → ℝ
hs : ¬s = ∅
t_max : α
ht_max : t_max ∈ s ∧ ∀ x' ∈ s, |f x'| ≤ |f t_max|
⊢ log⁺ |∑ t ∈ s, f t| ≤ log⁺ (∑ t ∈ s, |f t|)

Tactic:
apply monotoneOn_posLog (by simp) (by simp [Finset.sum_nonneg])

Result:
α : Type u_1
s : Finset α
f : α → ℝ
hs : ¬s = ∅
t_max : α
ht_max : t_max ∈ s ∧ ∀ x' ∈ s, |f x'| ≤ |f t_max|
⊢ |∑ t ∈ s, f t| ≤ ∑ t ∈ s, |f t|

Proof state:
α : Type u_1
s : Finset α
f : α → ℝ
hs : ¬s = ∅
t_max : α
ht_max : t_max ∈ s ∧ ∀ x' ∈ s, |f x'| ≤ |f t_max|
⊢ ∑ t ∈ s, |f t| ≤ ∑ t ∈ s, |f t_max|

Tactic:
apply Finset.sum_le_sum (fun i ih ↦ ht_max.2 i ih)

Result:
no goals

Proof state:
case neg.intro
α : Type u_1
s : Finset α
f : α → ℝ
hs : ¬s = ∅
t_max : α
ht_max : t_max ∈ s ∧ ∀ x' ∈ s, |f x'| ≤ |f t_max|
⊢ log⁺ (∑ t ∈ s, f t) ≤ log ↑s.card + ∑ t ∈ s, log⁺ (f t)

Tactic:
calc log⁺ (∑ t ∈ s, f t)
_ = log⁺ |∑ t ∈ s, f t| := by
  rw [Real.posLog_abs]
_ ≤ log⁺ (∑ t ∈ s, |f t|) := by
  apply monotoneOn_posLog (by simp) (by simp [Finset.sum_nonneg])
  simp [Finset.abs_sum_le_sum_abs]
_ ≤ log⁺ (∑ t ∈ s, |f t_max|) := by
  apply monotoneOn_posLog (by simp [Finset.sum_nonneg]) (by simp [Finset.sum_nonneg]; positivity)
  apply Finset.sum_le_sum (fun i ih ↦ ht_max.2 i ih)
_ = log⁺ (s.card * |f t_max|) := by
  simp [Finset.sum_const]
_ ≤ log s.card + log⁺ |f t_max| := posLog_nat_mul
_ ≤ log s.card + ∑ t ∈ s, log⁺ (f t) := by
  gcongr
  rw [posLog_abs]
  apply Finset.single_le_sum (fun _ _ ↦ posLog_nonneg) ht_max.1

Result:
no goals

Proof state:
case bc
α : Type u_1
s : Finset α
f : α → ℝ
hs : ¬s = ∅
t_max : α
ht_max : t_max ∈ s ∧ ∀ x' ∈ s, |f x'| ≤ |f t_max|
⊢ log⁺ |f t_max| ≤ ∑ t ∈ s, log⁺ (f t)

Tactic:
rw [posLog_abs]

Result:
case bc
α : Type u_1
s : Finset α
f : α → ℝ
hs : ¬s = ∅
t_max : α
ht_max : t_max ∈ s ∧ ∀ x' ∈ s, |f x'| ≤ |f t_max|
⊢ log⁺ (f t_max) ≤ ∑ t ∈ s, log⁺ (f t)

Proof state:
case pos
α : Type u_1
s : Finset α
f : α → ℝ
hs : s = ∅
⊢ log⁺ (∑ t ∈ s, f t) ≤ log ↑s.card + ∑ t ∈ s, log⁺ (f t)

Tactic:
simp [hs, posLog]

Result:
no goals

Proof state:
α : Type u_1
s : Finset α
f : α → ℝ
hs : ¬s = ∅
t_max : α
ht_max : t_max ∈ s ∧ ∀ x' ∈ s, |f x'| ≤ |f t_max|
⊢ ∑ t ∈ s, |f t_max| ∈ Set.Ici 0

Tactic:
simp [Finset.sum_nonneg]

Result:
α : Type u_1
s : Finset α
f : α → ℝ
hs : ¬s = ∅
t_max : α
ht_max : t_max ∈ s ∧ ∀ x' ∈ s, |f x'| ≤ |f t_max|
⊢ 0 ≤ ↑s.card * |f t_max|

Proof state:
α : Type u_1
s : Finset α
f : α → ℝ
hs : ¬s = ∅
t_max : α
ht_max : t_max ∈ s ∧ ∀ x' ∈ s, |f x'| ≤ |f t_max|
⊢ log⁺ (∑ t ∈ s, |f t_max|) = log⁺ (↑s.card * |f t_max|)

Tactic:
simp [Finset.sum_const]

Result:
no goals