case pos
ι : Type u
s : Finset ι
f g : ι → ℝ≥0∞
p q : ℝ
hp : 1 ≤ p
H' : (∑ i in s, f i ^ p) ^ (1 / p) = ⊤ ∨ (∑ i in s, g i ^ p) ^ (1 / p) = ⊤
⊢ (∑ i in s, (f i + g i) ^ p) ^ (1 / p) ≤ (∑ i in s, f i ^ p) ^ (1 / p) + (∑ i in s, g i ^ p) ^ (1 / p)

case neg
ι : Type u
s : Finset ι
f g : ι → ℝ≥0∞
p q : ℝ
hp : 1 ≤ p
H' : ¬((∑ i in s, f i ^ p) ^ (1 / p) = ⊤ ∨ (∑ i in s, g i ^ p) ^ (1 / p) = ⊤)
⊢ (∑ i in s, (f i + g i) ^ p) ^ (1 / p) ≤ (∑ i in s, f i ^ p) ^ (1 / p) + (∑ i in s, g i ^ p) ^ (1 / p)
ι : Type u
s : Finset ι
f g : ι → ℝ≥0∞
p q : ℝ
hp : 1 ≤ p
⊢ (∑ i in s, (f i + g i) ^ p) ^ (1 / p) ≤ (∑ i in s, f i ^ p) ^ (1 / p) + (∑ i in s, g i ^ p) ^ (1 / p)
by_cases H' : (∑ i in s, f i ^ p) ^ (1 / p) = ⊤ ∨ (∑ i in s, g i ^ p) ^ (1 / p) = ⊤
case neg
ι : Type u
s : Finset ι
f g : ι → ℝ≥0∞
p q : ℝ
hp : 1 ≤ p
H' : ¬((∑ i in s, f i ^ p) ^ (1 / p) = ⊤ ∨ (∑ i in s, g i ^ p) ^ (1 / p) = ⊤)
pos : 0 < p
⊢ (∑ i in s, (f i + g i) ^ p) ^ (1 / p) ≤ (∑ i in s, f i ^ p) ^ (1 / p) + (∑ i in s, g i ^ p) ^ (1 / p)
case neg
ι : Type u
s : Finset ι
f g : ι → ℝ≥0∞
p q : ℝ
hp : 1 ≤ p
H' : ¬((∑ i in s, f i ^ p) ^ (1 / p) = ⊤ ∨ (∑ i in s, g i ^ p) ^ (1 / p) = ⊤)
⊢ (∑ i in s, (f i + g i) ^ p) ^ (1 / p) ≤ (∑ i in s, f i ^ p) ^ (1 / p) + (∑ i in s, g i ^ p) ^ (1 / p)
have pos : 0 < p := lt_of_lt_of_le zero_lt_one hp
case H'
ι : Type u
s : Finset ι
f g : ι → ℝ≥0∞
p q : ℝ
hp : 1 ≤ p
H' : ¬((∑ i in s, f i ^ p) ^ (1 / p) = ⊤ ∨ (∑ i in s, g i ^ p) ^ (1 / p) = ⊤)
pos : 0 < p
⊢ (∀ (i : ι), i ∈ s → f i ≠ ⊤) ∧ ∀ (i : ι), i ∈ s → g i ≠ ⊤

case neg
ι : Type u
s : Finset ι
f g : ι → ℝ≥0∞
p q : ℝ
hp : 1 ≤ p
pos : 0 < p
H' : (∀ (i : ι), i ∈ s → f i ≠ ⊤) ∧ ∀ (i : ι), i ∈ s → g i ≠ ⊤
⊢ (∑ i in s, (f i + g i) ^ p) ^ (1 / p) ≤ (∑ i in s, f i ^ p) ^ (1 / p) + (∑ i in s, g i ^ p) ^ (1 / p)
case neg
ι : Type u
s : Finset ι
f g : ι → ℝ≥0∞
p q : ℝ
hp : 1 ≤ p
H' : ¬((∑ i in s, f i ^ p) ^ (1 / p) = ⊤ ∨ (∑ i in s, g i ^ p) ^ (1 / p) = ⊤)
pos : 0 < p
⊢ (∑ i in s, (f i + g i) ^ p) ^ (1 / p) ≤ (∑ i in s, f i ^ p) ^ (1 / p) + (∑ i in s, g i ^ p) ^ (1 / p)
replace H' : (∀ i ∈ s, f i ≠ ⊤) ∧ ∀ i ∈ s, g i ≠ ⊤
case neg
ι : Type u
s : Finset ι
f g : ι → ℝ≥0∞
p q : ℝ
hp : 1 ≤ p
pos : 0 < p
H' : (∀ (i : ι), i ∈ s → f i ≠ ⊤) ∧ ∀ (i : ι), i ∈ s → g i ≠ ⊤
this :
  ↑((∑ i in s, ((fun i => ENNReal.toNNReal (f i)) i + (fun i => ENNReal.toNNReal (g i)) i) ^ p) ^ (1 / p)) ≤
    ↑((∑ i in s, (fun i => ENNReal.toNNReal (f i)) i ^ p) ^ (1 / p) +
        (∑ i in s, (fun i => ENNReal.toNNReal (g i)) i ^ p) ^ (1 / p))
⊢ (∑ i in s, (f i + g i) ^ p) ^ (1 / p) ≤ (∑ i in s, f i ^ p) ^ (1 / p) + (∑ i in s, g i ^ p) ^ (1 / p)
case neg
ι : Type u
s : Finset ι
f g : ι → ℝ≥0∞
p q : ℝ
hp : 1 ≤ p
pos : 0 < p
H' : (∀ (i : ι), i ∈ s → f i ≠ ⊤) ∧ ∀ (i : ι), i ∈ s → g i ≠ ⊤
⊢ (∑ i in s, (f i + g i) ^ p) ^ (1 / p) ≤ (∑ i in s, f i ^ p) ^ (1 / p) + (∑ i in s, g i ^ p) ^ (1 / p)
have :=
  ENNReal.coe_le_coe.2
    (@NNReal.Lp_add_le _ s (fun i => ENNReal.toNNReal (f i)) (fun i => ENNReal.toNNReal (g i)) _
      hp)
case neg
ι : Type u
s : Finset ι
f g : ι → ℝ≥0∞
p q : ℝ
hp : 1 ≤ p
pos : 0 < p
H' : (∀ (i : ι), i ∈ s → f i ≠ ⊤) ∧ ∀ (i : ι), i ∈ s → g i ≠ ⊤
this :
  (∑ x in s, (↑(ENNReal.toNNReal (f x)) + ↑(ENNReal.toNNReal (g x))) ^ p) ^ (1 / p) ≤
    (∑ x in s, ↑(ENNReal.toNNReal (f x)) ^ p) ^ (1 / p) + (∑ x in s, ↑(ENNReal.toNNReal (g x)) ^ p) ^ (1 / p)
⊢ (∑ i in s, (f i + g i) ^ p) ^ (1 / p) ≤ (∑ i in s, f i ^ p) ^ (1 / p) + (∑ i in s, g i ^ p) ^ (1 / p)
case neg
ι : Type u
s : Finset ι
f g : ι → ℝ≥0∞
p q : ℝ
hp : 1 ≤ p
pos : 0 < p
H' : (∀ (i : ι), i ∈ s → f i ≠ ⊤) ∧ ∀ (i : ι), i ∈ s → g i ≠ ⊤
this :
  ↑((∑ i in s, ((fun i => ENNReal.toNNReal (f i)) i + (fun i => ENNReal.toNNReal (g i)) i) ^ p) ^ (1 / p)) ≤
    ↑((∑ i in s, (fun i => ENNReal.toNNReal (f i)) i ^ p) ^ (1 / p) +
        (∑ i in s, (fun i => ENNReal.toNNReal (g i)) i ^ p) ^ (1 / p))
⊢ (∑ i in s, (f i + g i) ^ p) ^ (1 / p) ≤ (∑ i in s, f i ^ p) ^ (1 / p) + (∑ i in s, g i ^ p) ^ (1 / p)
push_cast [← ENNReal.coe_rpow_of_nonneg, le_of_lt pos, le_of_lt (one_div_pos.2 pos)] at this
no goals
case pos
ι : Type u
s : Finset ι
f g : ι → ℝ≥0∞
p q : ℝ
hp : 1 ≤ p
H' : (∑ i in s, f i ^ p) ^ (1 / p) = ⊤ ∨ (∑ i in s, g i ^ p) ^ (1 / p) = ⊤
⊢ (∑ i in s, (f i + g i) ^ p) ^ (1 / p) ≤ (∑ i in s, f i ^ p) ^ (1 / p) + (∑ i in s, g i ^ p) ^ (1 / p)
cases' H' with H' H' <;> simp [H', -one_div]
no goals
case H'
ι : Type u
s : Finset ι
f g : ι → ℝ≥0∞
p q : ℝ
hp : 1 ≤ p
H' : ¬((∑ i in s, f i ^ p) ^ (1 / p) = ⊤ ∨ (∑ i in s, g i ^ p) ^ (1 / p) = ⊤)
pos : 0 < p
⊢ (∀ (i : ι), i ∈ s → f i ≠ ⊤) ∧ ∀ (i : ι), i ∈ s → g i ≠ ⊤
simpa [ENNReal.rpow_eq_top_iff, asymm pos, pos, ENNReal.sum_eq_top_iff, not_or] using H'
case h.e'_4.h.e'_6.e_a
ι : Type u
s : Finset ι
f g : ι → ℝ≥0∞
p q : ℝ
hp : 1 ≤ p
pos : 0 < p
H' : (∀ (i : ι), i ∈ s → f i ≠ ⊤) ∧ ∀ (i : ι), i ∈ s → g i ≠ ⊤
this :
  (∑ x in s, (↑(ENNReal.toNNReal (f x)) + ↑(ENNReal.toNNReal (g x))) ^ p) ^ (1 / p) ≤
    (∑ x in s, ↑(ENNReal.toNNReal (f x)) ^ p) ^ (1 / p) + (∑ x in s, ↑(ENNReal.toNNReal (g x)) ^ p) ^ (1 / p)
i : ι
hi : i ∈ s
⊢ g i ^ p = ↑(ENNReal.toNNReal (g i)) ^ p
case h.e'_4.h.e'_6.e_a
ι : Type u
s : Finset ι
f g : ι → ℝ≥0∞
p q : ℝ
hp : 1 ≤ p
pos : 0 < p
H' : (∀ (i : ι), i ∈ s → f i ≠ ⊤) ∧ ∀ (i : ι), i ∈ s → g i ≠ ⊤
this :
  (∑ x in s, (↑(ENNReal.toNNReal (f x)) + ↑(ENNReal.toNNReal (g x))) ^ p) ^ (1 / p) ≤
    (∑ x in s, ↑(ENNReal.toNNReal (f x)) ^ p) ^ (1 / p) + (∑ x in s, ↑(ENNReal.toNNReal (g x)) ^ p) ^ (1 / p)
⊢ ∑ i in s, g i ^ p = ∑ x in s, ↑(ENNReal.toNNReal (g x)) ^ p
refine Finset.sum_congr rfl fun i hi => ?_
no goals
case h.e'_4.h.e'_6.e_a
ι : Type u
s : Finset ι
f g : ι → ℝ≥0∞
p q : ℝ
hp : 1 ≤ p
pos : 0 < p
H' : (∀ (i : ι), i ∈ s → f i ≠ ⊤) ∧ ∀ (i : ι), i ∈ s → g i ≠ ⊤
this :
  (∑ x in s, (↑(ENNReal.toNNReal (f x)) + ↑(ENNReal.toNNReal (g x))) ^ p) ^ (1 / p) ≤
    (∑ x in s, ↑(ENNReal.toNNReal (f x)) ^ p) ^ (1 / p) + (∑ x in s, ↑(ENNReal.toNNReal (g x)) ^ p) ^ (1 / p)
i : ι
hi : i ∈ s
⊢ g i ^ p = ↑(ENNReal.toNNReal (g i)) ^ p
simp [H'.1 i hi, H'.2 i hi]