ι : Type u
s : Finset ι
p : ℝ
a b : ℝ≥0∞
hp1 : 1 ≤ p
hp_pos : 0 < p
⊢ a ^ p + b ^ p ≤ (a + b) ^ p
ι : Type u
s : Finset ι
p : ℝ
a b : ℝ≥0∞
hp1 : 1 ≤ p
⊢ a ^ p + b ^ p ≤ (a + b) ^ p
have hp_pos : 0 < p := by positivity
case pos
ι : Type u
s : Finset ι
p : ℝ
a b : ℝ≥0∞
hp1 : 1 ≤ p
hp_pos : 0 < p
h_top : a + b = ⊤
⊢ a ^ p + b ^ p ≤ (a + b) ^ p

case neg
ι : Type u
s : Finset ι
p : ℝ
a b : ℝ≥0∞
hp1 : 1 ≤ p
hp_pos : 0 < p
h_top : ¬a + b = ⊤
⊢ a ^ p + b ^ p ≤ (a + b) ^ p
ι : Type u
s : Finset ι
p : ℝ
a b : ℝ≥0∞
hp1 : 1 ≤ p
hp_pos : 0 < p
⊢ a ^ p + b ^ p ≤ (a + b) ^ p
by_cases h_top : a + b = ⊤
case neg.intro
ι : Type u
s : Finset ι
p : ℝ
a b : ℝ≥0∞
hp1 : 1 ≤ p
hp_pos : 0 < p
h_top : ¬a + b = ⊤
ha_top : a ≠ ⊤
hb_top : b ≠ ⊤
⊢ a ^ p + b ^ p ≤ (a + b) ^ p
case neg
ι : Type u
s : Finset ι
p : ℝ
a b : ℝ≥0∞
hp1 : 1 ≤ p
hp_pos : 0 < p
h_top : ¬a + b = ⊤
⊢ a ^ p + b ^ p ≤ (a + b) ^ p
obtain ⟨ha_top, hb_top⟩ := add_ne_top.mp h_top
case neg.intro.intro
ι : Type u
s : Finset ι
p : ℝ
b : ℝ≥0∞
hp1 : 1 ≤ p
hp_pos : 0 < p
hb_top : b ≠ ⊤
a : ℝ≥0
h_top : ¬↑a + b = ⊤
⊢ ↑a ^ p + b ^ p ≤ (↑a + b) ^ p
case neg.intro
ι : Type u
s : Finset ι
p : ℝ
a b : ℝ≥0∞
hp1 : 1 ≤ p
hp_pos : 0 < p
h_top : ¬a + b = ⊤
ha_top : a ≠ ⊤
hb_top : b ≠ ⊤
⊢ a ^ p + b ^ p ≤ (a + b) ^ p
lift a to ℝ≥0 using ha_top
case neg.intro.intro.intro
ι : Type u
s : Finset ι
p : ℝ
hp1 : 1 ≤ p
hp_pos : 0 < p
a b : ℝ≥0
h_top : ¬↑a + ↑b = ⊤
⊢ ↑a ^ p + ↑b ^ p ≤ (↑a + ↑b) ^ p
case neg.intro.intro
ι : Type u
s : Finset ι
p : ℝ
b : ℝ≥0∞
hp1 : 1 ≤ p
hp_pos : 0 < p
hb_top : b ≠ ⊤
a : ℝ≥0
h_top : ¬↑a + b = ⊤
⊢ ↑a ^ p + b ^ p ≤ (↑a + b) ^ p
lift b to ℝ≥0 using hb_top
no goals
case neg.intro.intro.intro
ι : Type u
s : Finset ι
p : ℝ
hp1 : 1 ≤ p
hp_pos : 0 < p
a b : ℝ≥0
h_top : ¬↑a + ↑b = ⊤
⊢ ↑a ^ p + ↑b ^ p ≤ (↑a + ↑b) ^ p
simpa [← ENNReal.coe_rpow_of_nonneg _ hp_pos.le] using
  ENNReal.coe_le_coe.2 (NNReal.add_rpow_le_rpow_add a b hp1)
no goals
ι : Type u
s : Finset ι
p : ℝ
a b : ℝ≥0∞
hp1 : 1 ≤ p
⊢ 0 < p
positivity
case pos
ι : Type u
s : Finset ι
p : ℝ
a b : ℝ≥0∞
hp1 : 1 ≤ p
hp_pos : 0 < p
h_top : (a + b) ^ p = ⊤
⊢ a ^ p + b ^ p ≤ (a + b) ^ p
case pos
ι : Type u
s : Finset ι
p : ℝ
a b : ℝ≥0∞
hp1 : 1 ≤ p
hp_pos : 0 < p
h_top : a + b = ⊤
⊢ a ^ p + b ^ p ≤ (a + b) ^ p
rw [← @ENNReal.rpow_eq_top_iff_of_pos (a + b) p hp_pos] at h_top
case pos
ι : Type u
s : Finset ι
p : ℝ
a b : ℝ≥0∞
hp1 : 1 ≤ p
hp_pos : 0 < p
h_top : (a + b) ^ p = ⊤
⊢ a ^ p + b ^ p ≤ ⊤
case pos
ι : Type u
s : Finset ι
p : ℝ
a b : ℝ≥0∞
hp1 : 1 ≤ p
hp_pos : 0 < p
h_top : (a + b) ^ p = ⊤
⊢ a ^ p + b ^ p ≤ (a + b) ^ p
rw [h_top]
no goals
case pos
ι : Type u
s : Finset ι
p : ℝ
a b : ℝ≥0∞
hp1 : 1 ≤ p
hp_pos : 0 < p
h_top : (a + b) ^ p = ⊤
⊢ a ^ p + b ^ p ≤ ⊤
exact le_top