[GOAL]
ι : Type u
s : Finset ι
f : ι → ℝ
n : ℕ
hf : ∀ (a : ι), a ∈ s → 0 ≤ f a
⊢ (∑ x in s, f x) ^ (n + 1) / ↑(card s) ^ n ≤ ∑ x in s, f x ^ (n + 1)
[PROOFSTEP]
rcases s.eq_empty_or_nonempty with (rfl | hs)
[GOAL]
case inl
ι : Type u
f : ι → ℝ
n : ℕ
hf : ∀ (a : ι), a ∈ ∅ → 0 ≤ f a
⊢ (∑ x in ∅, f x) ^ (n + 1) / ↑(card ∅) ^ n ≤ ∑ x in ∅, f x ^ (n + 1)
[PROOFSTEP]
simp_rw [Finset.sum_empty, zero_pow' _ (Nat.succ_ne_zero n), zero_div]
[GOAL]
case inl
ι : Type u
f : ι → ℝ
n : ℕ
hf : ∀ (a : ι), a ∈ ∅ → 0 ≤ f a
⊢ 0 ≤ 0
[PROOFSTEP]
rfl
[GOAL]
case inr
ι : Type u
s : Finset ι
f : ι → ℝ
n : ℕ
hf : ∀ (a : ι), a ∈ s → 0 ≤ f a
hs : Finset.Nonempty s
⊢ (∑ x in s, f x) ^ (n + 1) / ↑(card s) ^ n ≤ ∑ x in s, f x ^ (n + 1)
[PROOFSTEP]
have hs0 : 0 < (s.card : ℝ) := Nat.cast_pos.2 hs.card_pos
[GOAL]
case inr
ι : Type u
s : Finset ι
f : ι → ℝ
n : ℕ
hf : ∀ (a : ι), a ∈ s → 0 ≤ f a
hs : Finset.Nonempty s
hs0 : 0 < ↑(card s)
⊢ (∑ x in s, f x) ^ (n + 1) / ↑(card s) ^ n ≤ ∑ x in s, f x ^ (n + 1)
[PROOFSTEP]
suffices (∑ x in s, f x / s.card) ^ (n + 1) ≤ ∑ x in s, f x ^ (n + 1) / s.card by
  rwa [← Finset.sum_div, ← Finset.sum_div, div_pow, pow_succ' (s.card : ℝ), ← div_div, div_le_iff hs0, div_mul,
    div_self hs0.ne', div_one] at this 
[GOAL]
ι : Type u
s : Finset ι
f : ι → ℝ
n : ℕ
hf : ∀ (a : ι), a ∈ s → 0 ≤ f a
hs : Finset.Nonempty s
hs0 : 0 < ↑(card s)
this : (∑ x in s, f x / ↑(card s)) ^ (n + 1) ≤ ∑ x in s, f x ^ (n + 1) / ↑(card s)
⊢ (∑ x in s, f x) ^ (n + 1) / ↑(card s) ^ n ≤ ∑ x in s, f x ^ (n + 1)
[PROOFSTEP]
rwa [← Finset.sum_div, ← Finset.sum_div, div_pow, pow_succ' (s.card : ℝ), ← div_div, div_le_iff hs0, div_mul,
  div_self hs0.ne', div_one] at this 
[GOAL]
case inr
ι : Type u
s : Finset ι
f : ι → ℝ
n : ℕ
hf : ∀ (a : ι), a ∈ s → 0 ≤ f a
hs : Finset.Nonempty s
hs0 : 0 < ↑(card s)
⊢ (∑ x in s, f x / ↑(card s)) ^ (n + 1) ≤ ∑ x in s, f x ^ (n + 1) / ↑(card s)
[PROOFSTEP]
have :=
  @ConvexOn.map_sum_le ℝ ℝ ℝ ι _ _ _ _ _ _ (Set.Ici 0) (fun x => x ^ (n + 1)) s (fun _ => 1 / s.card) ((↑) ∘ f)
    (convexOn_pow (n + 1)) ?_ ?_ fun i hi => Set.mem_Ici.2 (hf i hi)
[GOAL]
case inr.refine_3
ι : Type u
s : Finset ι
f : ι → ℝ
n : ℕ
hf : ∀ (a : ι), a ∈ s → 0 ≤ f a
hs : Finset.Nonempty s
hs0 : 0 < ↑(card s)
this :
  (fun x => x ^ (n + 1)) (∑ i in s, (fun x => 1 / ↑(card s)) i • ((fun x => x) ∘ f) i) ≤
    ∑ i in s, (fun x => 1 / ↑(card s)) i • (fun x => x ^ (n + 1)) (((fun x => x) ∘ f) i)
⊢ (∑ x in s, f x / ↑(card s)) ^ (n + 1) ≤ ∑ x in s, f x ^ (n + 1) / ↑(card s)
[PROOFSTEP]
simpa only [inv_mul_eq_div, one_div, Algebra.id.smul_eq_mul] using this
[GOAL]
case inr.refine_1
ι : Type u
s : Finset ι
f : ι → ℝ
n : ℕ
hf : ∀ (a : ι), a ∈ s → 0 ≤ f a
hs : Finset.Nonempty s
hs0 : 0 < ↑(card s)
⊢ ∀ (i : ι), i ∈ s → 0 ≤ (fun x => 1 / ↑(card s)) i
[PROOFSTEP]
simp only [one_div, inv_nonneg, Nat.cast_nonneg, imp_true_iff]
[GOAL]
case inr.refine_2
ι : Type u
s : Finset ι
f : ι → ℝ
n : ℕ
hf : ∀ (a : ι), a ∈ s → 0 ≤ f a
hs : Finset.Nonempty s
hs0 : 0 < ↑(card s)
⊢ ∑ i in s, (fun x => 1 / ↑(card s)) i = 1
[PROOFSTEP]
simpa only [one_div, Finset.sum_const, nsmul_eq_mul] using mul_inv_cancel hs0.ne'
[GOAL]
ι : Type u
s : Finset ι
w z : ι → ℝ
hw : ∀ (i : ι), i ∈ s → 0 ≤ w i
hw' : ∑ i in s, w i = 1
hz : ∀ (i : ι), i ∈ s → 0 ≤ z i
p : ℝ
hp : 1 ≤ p
⊢ ∑ i in s, w i * z i ≤ (∑ i in s, w i * z i ^ p) ^ (1 / p)
[PROOFSTEP]
have : 0 < p := by positivity
[GOAL]
ι : Type u
s : Finset ι
w z : ι → ℝ
hw : ∀ (i : ι), i ∈ s → 0 ≤ w i
hw' : ∑ i in s, w i = 1
hz : ∀ (i : ι), i ∈ s → 0 ≤ z i
p : ℝ
hp : 1 ≤ p
⊢ 0 < p
[PROOFSTEP]
positivity
[GOAL]
ι : Type u
s : Finset ι
w z : ι → ℝ
hw : ∀ (i : ι), i ∈ s → 0 ≤ w i
hw' : ∑ i in s, w i = 1
hz : ∀ (i : ι), i ∈ s → 0 ≤ z i
p : ℝ
hp : 1 ≤ p
this : 0 < p
⊢ ∑ i in s, w i * z i ≤ (∑ i in s, w i * z i ^ p) ^ (1 / p)
[PROOFSTEP]
rw [← rpow_le_rpow_iff _ _ this, ← rpow_mul, one_div_mul_cancel (ne_of_gt this), rpow_one]
[GOAL]
ι : Type u
s : Finset ι
w z : ι → ℝ
hw : ∀ (i : ι), i ∈ s → 0 ≤ w i
hw' : ∑ i in s, w i = 1
hz : ∀ (i : ι), i ∈ s → 0 ≤ z i
p : ℝ
hp : 1 ≤ p
this : 0 < p
⊢ (∑ i in s, w i * z i) ^ p ≤ ∑ i in s, w i * z i ^ p
case hx
ι : Type u
s : Finset ι
w z : ι → ℝ
hw : ∀ (i : ι), i ∈ s → 0 ≤ w i
hw' : ∑ i in s, w i = 1
hz : ∀ (i : ι), i ∈ s → 0 ≤ z i
p : ℝ
hp : 1 ≤ p
this : 0 < p
⊢ 0 ≤ ∑ i in s, w i * z i ^ p
ι : Type u
s : Finset ι
w z : ι → ℝ
hw : ∀ (i : ι), i ∈ s → 0 ≤ w i
hw' : ∑ i in s, w i = 1
hz : ∀ (i : ι), i ∈ s → 0 ≤ z i
p : ℝ
hp : 1 ≤ p
this : 0 < p
⊢ 0 ≤ ∑ i in s, w i * z i
ι : Type u
s : Finset ι
w z : ι → ℝ
hw : ∀ (i : ι), i ∈ s → 0 ≤ w i
hw' : ∑ i in s, w i = 1
hz : ∀ (i : ι), i ∈ s → 0 ≤ z i
p : ℝ
hp : 1 ≤ p
this : 0 < p
⊢ 0 ≤ (∑ i in s, w i * z i ^ p) ^ (1 / p)
[PROOFSTEP]
exact rpow_arith_mean_le_arith_mean_rpow s w z hw hw' hz hp
[GOAL]
case hx
ι : Type u
s : Finset ι
w z : ι → ℝ
hw : ∀ (i : ι), i ∈ s → 0 ≤ w i
hw' : ∑ i in s, w i = 1
hz : ∀ (i : ι), i ∈ s → 0 ≤ z i
p : ℝ
hp : 1 ≤ p
this : 0 < p
⊢ 0 ≤ ∑ i in s, w i * z i ^ p
ι : Type u
s : Finset ι
w z : ι → ℝ
hw : ∀ (i : ι), i ∈ s → 0 ≤ w i
hw' : ∑ i in s, w i = 1
hz : ∀ (i : ι), i ∈ s → 0 ≤ z i
p : ℝ
hp : 1 ≤ p
this : 0 < p
⊢ 0 ≤ ∑ i in s, w i * z i
ι : Type u
s : Finset ι
w z : ι → ℝ
hw : ∀ (i : ι), i ∈ s → 0 ≤ w i
hw' : ∑ i in s, w i = 1
hz : ∀ (i : ι), i ∈ s → 0 ≤ z i
p : ℝ
hp : 1 ≤ p
this : 0 < p
⊢ 0 ≤ (∑ i in s, w i * z i ^ p) ^ (1 / p)
[PROOFSTEP]
all_goals
  apply_rules [sum_nonneg, rpow_nonneg_of_nonneg]
  intro i hi
  apply_rules [mul_nonneg, rpow_nonneg_of_nonneg, hw i hi, hz i hi]
[GOAL]
case hx
ι : Type u
s : Finset ι
w z : ι → ℝ
hw : ∀ (i : ι), i ∈ s → 0 ≤ w i
hw' : ∑ i in s, w i = 1
hz : ∀ (i : ι), i ∈ s → 0 ≤ z i
p : ℝ
hp : 1 ≤ p
this : 0 < p
⊢ 0 ≤ ∑ i in s, w i * z i ^ p
[PROOFSTEP]
apply_rules [sum_nonneg, rpow_nonneg_of_nonneg]
[GOAL]
case hx
ι : Type u
s : Finset ι
w z : ι → ℝ
hw : ∀ (i : ι), i ∈ s → 0 ≤ w i
hw' : ∑ i in s, w i = 1
hz : ∀ (i : ι), i ∈ s → 0 ≤ z i
p : ℝ
hp : 1 ≤ p
this : 0 < p
hw'_symm : 1 = ∑ i in s, w i
⊢ ∀ (i : ι), i ∈ s → 0 ≤ w i * z i ^ p
[PROOFSTEP]
intro i hi
[GOAL]
case hx
ι : Type u
s : Finset ι
w z : ι → ℝ
hw : ∀ (i : ι), i ∈ s → 0 ≤ w i
hw' : ∑ i in s, w i = 1
hz : ∀ (i : ι), i ∈ s → 0 ≤ z i
p : ℝ
hp : 1 ≤ p
this : 0 < p
hw'_symm : 1 = ∑ i in s, w i
i : ι
hi : i ∈ s
⊢ 0 ≤ w i * z i ^ p
[PROOFSTEP]
apply_rules [mul_nonneg, rpow_nonneg_of_nonneg, hw i hi, hz i hi]
[GOAL]
ι : Type u
s : Finset ι
w z : ι → ℝ
hw : ∀ (i : ι), i ∈ s → 0 ≤ w i
hw' : ∑ i in s, w i = 1
hz : ∀ (i : ι), i ∈ s → 0 ≤ z i
p : ℝ
hp : 1 ≤ p
this : 0 < p
⊢ 0 ≤ ∑ i in s, w i * z i
[PROOFSTEP]
apply_rules [sum_nonneg, rpow_nonneg_of_nonneg]
[GOAL]
ι : Type u
s : Finset ι
w z : ι → ℝ
hw : ∀ (i : ι), i ∈ s → 0 ≤ w i
hw' : ∑ i in s, w i = 1
hz : ∀ (i : ι), i ∈ s → 0 ≤ z i
p : ℝ
hp : 1 ≤ p
this : 0 < p
hw'_symm : 1 = ∑ i in s, w i
⊢ ∀ (i : ι), i ∈ s → 0 ≤ w i * z i
[PROOFSTEP]
intro i hi
[GOAL]
ι : Type u
s : Finset ι
w z : ι → ℝ
hw : ∀ (i : ι), i ∈ s → 0 ≤ w i
hw' : ∑ i in s, w i = 1
hz : ∀ (i : ι), i ∈ s → 0 ≤ z i
p : ℝ
hp : 1 ≤ p
this : 0 < p
hw'_symm : 1 = ∑ i in s, w i
i : ι
hi : i ∈ s
⊢ 0 ≤ w i * z i
[PROOFSTEP]
apply_rules [mul_nonneg, rpow_nonneg_of_nonneg, hw i hi, hz i hi]
[GOAL]
ι : Type u
s : Finset ι
w z : ι → ℝ
hw : ∀ (i : ι), i ∈ s → 0 ≤ w i
hw' : ∑ i in s, w i = 1
hz : ∀ (i : ι), i ∈ s → 0 ≤ z i
p : ℝ
hp : 1 ≤ p
this : 0 < p
⊢ 0 ≤ (∑ i in s, w i * z i ^ p) ^ (1 / p)
[PROOFSTEP]
apply_rules [sum_nonneg, rpow_nonneg_of_nonneg]
[GOAL]
case hx
ι : Type u
s : Finset ι
w z : ι → ℝ
hw : ∀ (i : ι), i ∈ s → 0 ≤ w i
hw' : ∑ i in s, w i = 1
hz : ∀ (i : ι), i ∈ s → 0 ≤ z i
p : ℝ
hp : 1 ≤ p
this : 0 < p
hw'_symm : 1 = ∑ i in s, w i
⊢ ∀ (i : ι), i ∈ s → 0 ≤ w i * z i ^ p
[PROOFSTEP]
intro i hi
[GOAL]
case hx
ι : Type u
s : Finset ι
w z : ι → ℝ
hw : ∀ (i : ι), i ∈ s → 0 ≤ w i
hw' : ∑ i in s, w i = 1
hz : ∀ (i : ι), i ∈ s → 0 ≤ z i
p : ℝ
hp : 1 ≤ p
this : 0 < p
hw'_symm : 1 = ∑ i in s, w i
i : ι
hi : i ∈ s
⊢ 0 ≤ w i * z i ^ p
[PROOFSTEP]
apply_rules [mul_nonneg, rpow_nonneg_of_nonneg, hw i hi, hz i hi]
[GOAL]
ι : Type u
s : Finset ι
w z : ι → ℝ≥0
hw' : ∑ i in s, w i = 1
n : ℕ
⊢ (∑ i in s, w i * z i) ^ n ≤ ∑ i in s, w i * z i ^ n
[PROOFSTEP]
exact_mod_cast
  Real.pow_arith_mean_le_arith_mean_pow s _ _ (fun i _ => (w i).coe_nonneg) (by exact_mod_cast hw')
    (fun i _ => (z i).coe_nonneg) n
[GOAL]
ι : Type u
s : Finset ι
w z : ι → ℝ≥0
hw' : ∑ i in s, w i = 1
n : ℕ
⊢ ∑ i in s, ↑(w i) = 1
[PROOFSTEP]
exact_mod_cast hw'
[GOAL]
ι : Type u
s : Finset ι
f : ι → ℝ≥0
n : ℕ
⊢ ↑((∑ x in s, f x) ^ (n + 1)) / ↑(card s) ^ n ≤ ↑(∑ x in s, f x ^ (n + 1))
[PROOFSTEP]
simpa only [← NNReal.coe_le_coe, NNReal.coe_sum, Nonneg.coe_div, NNReal.coe_pow] using
  @Real.pow_sum_div_card_le_sum_pow ι s (((↑) : ℝ≥0 → ℝ) ∘ f) n fun _ _ => NNReal.coe_nonneg _
[GOAL]
ι : Type u
s : Finset ι
w z : ι → ℝ≥0
hw' : ∑ i in s, w i = 1
p : ℝ
hp : 1 ≤ p
⊢ (∑ i in s, w i * z i) ^ p ≤ ∑ i in s, w i * z i ^ p
[PROOFSTEP]
exact_mod_cast
  Real.rpow_arith_mean_le_arith_mean_rpow s _ _ (fun i _ => (w i).coe_nonneg) (by exact_mod_cast hw')
    (fun i _ => (z i).coe_nonneg) hp
[GOAL]
ι : Type u
s : Finset ι
w z : ι → ℝ≥0
hw' : ∑ i in s, w i = 1
p : ℝ
hp : 1 ≤ p
⊢ ∑ i in s, ↑(w i) = 1
[PROOFSTEP]
exact_mod_cast hw'
[GOAL]
ι : Type u
s : Finset ι
w₁ w₂ z₁ z₂ : ℝ≥0
hw' : w₁ + w₂ = 1
p : ℝ
hp : 1 ≤ p
⊢ (w₁ * z₁ + w₂ * z₂) ^ p ≤ w₁ * z₁ ^ p + w₂ * z₂ ^ p
[PROOFSTEP]
have h := rpow_arith_mean_le_arith_mean_rpow univ ![w₁, w₂] ![z₁, z₂] ?_ hp
[GOAL]
case refine_2
ι : Type u
s : Finset ι
w₁ w₂ z₁ z₂ : ℝ≥0
hw' : w₁ + w₂ = 1
p : ℝ
hp : 1 ≤ p
h :
  (∑ i : Fin (Nat.succ (Nat.succ 0)), Matrix.vecCons w₁ ![w₂] i * Matrix.vecCons z₁ ![z₂] i) ^ p ≤
    ∑ i : Fin (Nat.succ (Nat.succ 0)), Matrix.vecCons w₁ ![w₂] i * Matrix.vecCons z₁ ![z₂] i ^ p
⊢ (w₁ * z₁ + w₂ * z₂) ^ p ≤ w₁ * z₁ ^ p + w₂ * z₂ ^ p
[PROOFSTEP]
simpa [Fin.sum_univ_succ] using h
[GOAL]
case refine_1
ι : Type u
s : Finset ι
w₁ w₂ z₁ z₂ : ℝ≥0
hw' : w₁ + w₂ = 1
p : ℝ
hp : 1 ≤ p
⊢ ∑ i : Fin (Nat.succ (Nat.succ 0)), Matrix.vecCons w₁ ![w₂] i = 1
[PROOFSTEP]
simp [hw', Fin.sum_univ_succ]
[GOAL]
ι : Type u
s : Finset ι
z₁ z₂ : ℝ≥0
p : ℝ
hp : 1 ≤ p
⊢ (z₁ + z₂) ^ p ≤ 2 ^ (p - 1) * (z₁ ^ p + z₂ ^ p)
[PROOFSTEP]
rcases eq_or_lt_of_le hp with (rfl | h'p)
[GOAL]
case inl
ι : Type u
s : Finset ι
z₁ z₂ : ℝ≥0
hp : 1 ≤ 1
⊢ (z₁ + z₂) ^ 1 ≤ 2 ^ (1 - 1) * (z₁ ^ 1 + z₂ ^ 1)
[PROOFSTEP]
simp only [rpow_one, sub_self, rpow_zero, one_mul]
[GOAL]
case inl
ι : Type u
s : Finset ι
z₁ z₂ : ℝ≥0
hp : 1 ≤ 1
⊢ z₁ + z₂ ≤ z₁ + z₂
[PROOFSTEP]
rfl
[GOAL]
case inr
ι : Type u
s : Finset ι
z₁ z₂ : ℝ≥0
p : ℝ
hp : 1 ≤ p
h'p : 1 < p
⊢ (z₁ + z₂) ^ p ≤ 2 ^ (p - 1) * (z₁ ^ p + z₂ ^ p)
[PROOFSTEP]
convert rpow_arith_mean_le_arith_mean2_rpow (1 / 2) (1 / 2) (2 * z₁) (2 * z₂) (add_halves 1) hp using 1
[GOAL]
case h.e'_3
ι : Type u
s : Finset ι
z₁ z₂ : ℝ≥0
p : ℝ
hp : 1 ≤ p
h'p : 1 < p
⊢ (z₁ + z₂) ^ p = (1 / 2 * (2 * z₁) + 1 / 2 * (2 * z₂)) ^ p
[PROOFSTEP]
simp only [one_div, inv_mul_cancel_left₀, Ne.def, mul_eq_zero, two_ne_zero, one_ne_zero, not_false_iff]
[GOAL]
case h.e'_4
ι : Type u
s : Finset ι
z₁ z₂ : ℝ≥0
p : ℝ
hp : 1 ≤ p
h'p : 1 < p
⊢ 2 ^ (p - 1) * (z₁ ^ p + z₂ ^ p) = 1 / 2 * (2 * z₁) ^ p + 1 / 2 * (2 * z₂) ^ p
[PROOFSTEP]
have A : p - 1 ≠ 0 := ne_of_gt (sub_pos.2 h'p)
[GOAL]
case h.e'_4
ι : Type u
s : Finset ι
z₁ z₂ : ℝ≥0
p : ℝ
hp : 1 ≤ p
h'p : 1 < p
A : p - 1 ≠ 0
⊢ 2 ^ (p - 1) * (z₁ ^ p + z₂ ^ p) = 1 / 2 * (2 * z₁) ^ p + 1 / 2 * (2 * z₂) ^ p
[PROOFSTEP]
simp only [mul_rpow, rpow_sub' _ A, div_eq_inv_mul, rpow_one, mul_one]
[GOAL]
case h.e'_4
ι : Type u
s : Finset ι
z₁ z₂ : ℝ≥0
p : ℝ
hp : 1 ≤ p
h'p : 1 < p
A : p - 1 ≠ 0
⊢ 2⁻¹ * 2 ^ p * (z₁ ^ p + z₂ ^ p) = 2⁻¹ * (2 ^ p * z₁ ^ p) + 2⁻¹ * (2 ^ p * z₂ ^ p)
[PROOFSTEP]
ring
[GOAL]
ι : Type u
s : Finset ι
w z : ι → ℝ≥0
hw' : ∑ i in s, w i = 1
p : ℝ
hp : 1 ≤ p
⊢ ∑ i in s, w i * z i ≤ (∑ i in s, w i * z i ^ p) ^ (1 / p)
[PROOFSTEP]
exact_mod_cast
  Real.arith_mean_le_rpow_mean s _ _ (fun i _ => (w i).coe_nonneg) (by exact_mod_cast hw') (fun i _ => (z i).coe_nonneg)
    hp
[GOAL]
ι : Type u
s : Finset ι
w z : ι → ℝ≥0
hw' : ∑ i in s, w i = 1
p : ℝ
hp : 1 ≤ p
⊢ ∑ i in s, ↑(w i) = 1
[PROOFSTEP]
exact_mod_cast hw'
[GOAL]
ι : Type u
s : Finset ι
p : ℝ
a b : ℝ≥0
hab : a + b ≤ 1
hp1 : 1 ≤ p
⊢ a ^ p + b ^ p ≤ 1
[PROOFSTEP]
have h_le_one : ∀ x : ℝ≥0, x ≤ 1 → x ^ p ≤ x := fun x hx => rpow_le_self_of_le_one hx hp1
[GOAL]
ι : Type u
s : Finset ι
p : ℝ
a b : ℝ≥0
hab : a + b ≤ 1
hp1 : 1 ≤ p
h_le_one : ∀ (x : ℝ≥0), x ≤ 1 → x ^ p ≤ x
⊢ a ^ p + b ^ p ≤ 1
[PROOFSTEP]
have ha : a ≤ 1 := (self_le_add_right a b).trans hab
[GOAL]
ι : Type u
s : Finset ι
p : ℝ
a b : ℝ≥0
hab : a + b ≤ 1
hp1 : 1 ≤ p
h_le_one : ∀ (x : ℝ≥0), x ≤ 1 → x ^ p ≤ x
ha : a ≤ 1
⊢ a ^ p + b ^ p ≤ 1
[PROOFSTEP]
have hb : b ≤ 1 := (self_le_add_left b a).trans hab
[GOAL]
ι : Type u
s : Finset ι
p : ℝ
a b : ℝ≥0
hab : a + b ≤ 1
hp1 : 1 ≤ p
h_le_one : ∀ (x : ℝ≥0), x ≤ 1 → x ^ p ≤ x
ha : a ≤ 1
hb : b ≤ 1
⊢ a ^ p + b ^ p ≤ 1
[PROOFSTEP]
exact (add_le_add (h_le_one a ha) (h_le_one b hb)).trans hab
[GOAL]
ι : Type u
s : Finset ι
p : ℝ
a b : ℝ≥0
hp1 : 1 ≤ p
⊢ a ^ p + b ^ p ≤ (a + b) ^ p
[PROOFSTEP]
have hp_pos : 0 < p := by positivity
[GOAL]
ι : Type u
s : Finset ι
p : ℝ
a b : ℝ≥0
hp1 : 1 ≤ p
⊢ 0 < p
[PROOFSTEP]
positivity
[GOAL]
ι : Type u
s : Finset ι
p : ℝ
a b : ℝ≥0
hp1 : 1 ≤ p
hp_pos : 0 < p
⊢ a ^ p + b ^ p ≤ (a + b) ^ p
[PROOFSTEP]
by_cases h_zero : a + b = 0
[GOAL]
case pos
ι : Type u
s : Finset ι
p : ℝ
a b : ℝ≥0
hp1 : 1 ≤ p
hp_pos : 0 < p
h_zero : a + b = 0
⊢ a ^ p + b ^ p ≤ (a + b) ^ p
[PROOFSTEP]
simp [add_eq_zero_iff.mp h_zero, hp_pos.ne']
[GOAL]
case neg
ι : Type u
s : Finset ι
p : ℝ
a b : ℝ≥0
hp1 : 1 ≤ p
hp_pos : 0 < p
h_zero : ¬a + b = 0
⊢ a ^ p + b ^ p ≤ (a + b) ^ p
[PROOFSTEP]
have h_nonzero : ¬(a = 0 ∧ b = 0) := by rwa [add_eq_zero_iff] at h_zero 
[GOAL]
ι : Type u
s : Finset ι
p : ℝ
a b : ℝ≥0
hp1 : 1 ≤ p
hp_pos : 0 < p
h_zero : ¬a + b = 0
⊢ ¬(a = 0 ∧ b = 0)
[PROOFSTEP]
rwa [add_eq_zero_iff] at h_zero 
[GOAL]
case neg
ι : Type u
s : Finset ι
p : ℝ
a b : ℝ≥0
hp1 : 1 ≤ p
hp_pos : 0 < p
h_zero : ¬a + b = 0
h_nonzero : ¬(a = 0 ∧ b = 0)
⊢ a ^ p + b ^ p ≤ (a + b) ^ p
[PROOFSTEP]
have h_add : a / (a + b) + b / (a + b) = 1 := by rw [div_add_div_same, div_self h_zero]
[GOAL]
ι : Type u
s : Finset ι
p : ℝ
a b : ℝ≥0
hp1 : 1 ≤ p
hp_pos : 0 < p
h_zero : ¬a + b = 0
h_nonzero : ¬(a = 0 ∧ b = 0)
⊢ a / (a + b) + b / (a + b) = 1
[PROOFSTEP]
rw [div_add_div_same, div_self h_zero]
[GOAL]
case neg
ι : Type u
s : Finset ι
p : ℝ
a b : ℝ≥0
hp1 : 1 ≤ p
hp_pos : 0 < p
h_zero : ¬a + b = 0
h_nonzero : ¬(a = 0 ∧ b = 0)
h_add : a / (a + b) + b / (a + b) = 1
⊢ a ^ p + b ^ p ≤ (a + b) ^ p
[PROOFSTEP]
have h := add_rpow_le_one_of_add_le_one (a / (a + b)) (b / (a + b)) h_add.le hp1
[GOAL]
case neg
ι : Type u
s : Finset ι
p : ℝ
a b : ℝ≥0
hp1 : 1 ≤ p
hp_pos : 0 < p
h_zero : ¬a + b = 0
h_nonzero : ¬(a = 0 ∧ b = 0)
h_add : a / (a + b) + b / (a + b) = 1
h : (a / (a + b)) ^ p + (b / (a + b)) ^ p ≤ 1
⊢ a ^ p + b ^ p ≤ (a + b) ^ p
[PROOFSTEP]
rw [div_rpow a (a + b), div_rpow b (a + b)] at h 
[GOAL]
case neg
ι : Type u
s : Finset ι
p : ℝ
a b : ℝ≥0
hp1 : 1 ≤ p
hp_pos : 0 < p
h_zero : ¬a + b = 0
h_nonzero : ¬(a = 0 ∧ b = 0)
h_add : a / (a + b) + b / (a + b) = 1
h : a ^ p / (a + b) ^ p + b ^ p / (a + b) ^ p ≤ 1
⊢ a ^ p + b ^ p ≤ (a + b) ^ p
[PROOFSTEP]
have hab_0 : (a + b) ^ p ≠ 0 := by simp [hp_pos, h_nonzero]
[GOAL]
ι : Type u
s : Finset ι
p : ℝ
a b : ℝ≥0
hp1 : 1 ≤ p
hp_pos : 0 < p
h_zero : ¬a + b = 0
h_nonzero : ¬(a = 0 ∧ b = 0)
h_add : a / (a + b) + b / (a + b) = 1
h : a ^ p / (a + b) ^ p + b ^ p / (a + b) ^ p ≤ 1
⊢ (a + b) ^ p ≠ 0
[PROOFSTEP]
simp [hp_pos, h_nonzero]
[GOAL]
case neg
ι : Type u
s : Finset ι
p : ℝ
a b : ℝ≥0
hp1 : 1 ≤ p
hp_pos : 0 < p
h_zero : ¬a + b = 0
h_nonzero : ¬(a = 0 ∧ b = 0)
h_add : a / (a + b) + b / (a + b) = 1
h : a ^ p / (a + b) ^ p + b ^ p / (a + b) ^ p ≤ 1
hab_0 : (a + b) ^ p ≠ 0
⊢ a ^ p + b ^ p ≤ (a + b) ^ p
[PROOFSTEP]
have hab_0' : 0 < (a + b) ^ p := zero_lt_iff.mpr hab_0
[GOAL]
case neg
ι : Type u
s : Finset ι
p : ℝ
a b : ℝ≥0
hp1 : 1 ≤ p
hp_pos : 0 < p
h_zero : ¬a + b = 0
h_nonzero : ¬(a = 0 ∧ b = 0)
h_add : a / (a + b) + b / (a + b) = 1
h : a ^ p / (a + b) ^ p + b ^ p / (a + b) ^ p ≤ 1
hab_0 : (a + b) ^ p ≠ 0
hab_0' : 0 < (a + b) ^ p
⊢ a ^ p + b ^ p ≤ (a + b) ^ p
[PROOFSTEP]
have h_mul : (a + b) ^ p * (a ^ p / (a + b) ^ p + b ^ p / (a + b) ^ p) ≤ (a + b) ^ p :=
  by
  nth_rw 4 [← mul_one ((a + b) ^ p)]
  exact (mul_le_mul_left hab_0').mpr h
[GOAL]
ι : Type u
s : Finset ι
p : ℝ
a b : ℝ≥0
hp1 : 1 ≤ p
hp_pos : 0 < p
h_zero : ¬a + b = 0
h_nonzero : ¬(a = 0 ∧ b = 0)
h_add : a / (a + b) + b / (a + b) = 1
h : a ^ p / (a + b) ^ p + b ^ p / (a + b) ^ p ≤ 1
hab_0 : (a + b) ^ p ≠ 0
hab_0' : 0 < (a + b) ^ p
⊢ (a + b) ^ p * (a ^ p / (a + b) ^ p + b ^ p / (a + b) ^ p) ≤ (a + b) ^ p
[PROOFSTEP]
nth_rw 4 [← mul_one ((a + b) ^ p)]
[GOAL]
ι : Type u
s : Finset ι
p : ℝ
a b : ℝ≥0
hp1 : 1 ≤ p
hp_pos : 0 < p
h_zero : ¬a + b = 0
h_nonzero : ¬(a = 0 ∧ b = 0)
h_add : a / (a + b) + b / (a + b) = 1
h : a ^ p / (a + b) ^ p + b ^ p / (a + b) ^ p ≤ 1
hab_0 : (a + b) ^ p ≠ 0
hab_0' : 0 < (a + b) ^ p
⊢ (a + b) ^ p * (a ^ p / (a + b) ^ p + b ^ p / (a + b) ^ p) ≤ (a + b) ^ p * 1
[PROOFSTEP]
exact (mul_le_mul_left hab_0').mpr h
[GOAL]
case neg
ι : Type u
s : Finset ι
p : ℝ
a b : ℝ≥0
hp1 : 1 ≤ p
hp_pos : 0 < p
h_zero : ¬a + b = 0
h_nonzero : ¬(a = 0 ∧ b = 0)
h_add : a / (a + b) + b / (a + b) = 1
h : a ^ p / (a + b) ^ p + b ^ p / (a + b) ^ p ≤ 1
hab_0 : (a + b) ^ p ≠ 0
hab_0' : 0 < (a + b) ^ p
h_mul : (a + b) ^ p * (a ^ p / (a + b) ^ p + b ^ p / (a + b) ^ p) ≤ (a + b) ^ p
⊢ a ^ p + b ^ p ≤ (a + b) ^ p
[PROOFSTEP]
rwa [div_eq_mul_inv, div_eq_mul_inv, mul_add, mul_comm (a ^ p), mul_comm (b ^ p), ← mul_assoc, ← mul_assoc,
  mul_inv_cancel hab_0, one_mul, one_mul] at h_mul 
[GOAL]
ι : Type u
s : Finset ι
p : ℝ
a b : ℝ≥0
hp1 : 1 ≤ p
⊢ (a ^ p + b ^ p) ^ (1 / p) ≤ a + b
[PROOFSTEP]
rw [← @NNReal.le_rpow_one_div_iff _ _ (1 / p) (by simp [lt_of_lt_of_le zero_lt_one hp1])]
[GOAL]
ι : Type u
s : Finset ι
p : ℝ
a b : ℝ≥0
hp1 : 1 ≤ p
⊢ 0 < 1 / p
[PROOFSTEP]
simp [lt_of_lt_of_le zero_lt_one hp1]
[GOAL]
ι : Type u
s : Finset ι
p : ℝ
a b : ℝ≥0
hp1 : 1 ≤ p
⊢ a ^ p + b ^ p ≤ (a + b) ^ (1 / (1 / p))
[PROOFSTEP]
rw [one_div_one_div]
[GOAL]
ι : Type u
s : Finset ι
p : ℝ
a b : ℝ≥0
hp1 : 1 ≤ p
⊢ a ^ p + b ^ p ≤ (a + b) ^ p
[PROOFSTEP]
exact add_rpow_le_rpow_add _ _ hp1
[GOAL]
ι : Type u
s : Finset ι
p q : ℝ
a b : ℝ≥0
hp_pos : 0 < p
hpq : p ≤ q
⊢ (a ^ q + b ^ q) ^ (1 / q) ≤ (a ^ p + b ^ p) ^ (1 / p)
[PROOFSTEP]
have h_rpow : ∀ a : ℝ≥0, a ^ q = (a ^ p) ^ (q / p) := fun a => by
  rw [← NNReal.rpow_mul, div_eq_inv_mul, ← mul_assoc, _root_.mul_inv_cancel hp_pos.ne.symm, one_mul]
[GOAL]
ι : Type u
s : Finset ι
p q : ℝ
a✝ b : ℝ≥0
hp_pos : 0 < p
hpq : p ≤ q
a : ℝ≥0
⊢ a ^ q = (a ^ p) ^ (q / p)
[PROOFSTEP]
rw [← NNReal.rpow_mul, div_eq_inv_mul, ← mul_assoc, _root_.mul_inv_cancel hp_pos.ne.symm, one_mul]
[GOAL]
ι : Type u
s : Finset ι
p q : ℝ
a b : ℝ≥0
hp_pos : 0 < p
hpq : p ≤ q
h_rpow : ∀ (a : ℝ≥0), a ^ q = (a ^ p) ^ (q / p)
⊢ (a ^ q + b ^ q) ^ (1 / q) ≤ (a ^ p + b ^ p) ^ (1 / p)
[PROOFSTEP]
have h_rpow_add_rpow_le_add : ((a ^ p) ^ (q / p) + (b ^ p) ^ (q / p)) ^ (1 / (q / p)) ≤ a ^ p + b ^ p :=
  by
  refine' rpow_add_rpow_le_add (a ^ p) (b ^ p) _
  rwa [one_le_div hp_pos]
[GOAL]
ι : Type u
s : Finset ι
p q : ℝ
a b : ℝ≥0
hp_pos : 0 < p
hpq : p ≤ q
h_rpow : ∀ (a : ℝ≥0), a ^ q = (a ^ p) ^ (q / p)
⊢ ((a ^ p) ^ (q / p) + (b ^ p) ^ (q / p)) ^ (1 / (q / p)) ≤ a ^ p + b ^ p
[PROOFSTEP]
refine' rpow_add_rpow_le_add (a ^ p) (b ^ p) _
[GOAL]
ι : Type u
s : Finset ι
p q : ℝ
a b : ℝ≥0
hp_pos : 0 < p
hpq : p ≤ q
h_rpow : ∀ (a : ℝ≥0), a ^ q = (a ^ p) ^ (q / p)
⊢ 1 ≤ q / p
[PROOFSTEP]
rwa [one_le_div hp_pos]
[GOAL]
ι : Type u
s : Finset ι
p q : ℝ
a b : ℝ≥0
hp_pos : 0 < p
hpq : p ≤ q
h_rpow : ∀ (a : ℝ≥0), a ^ q = (a ^ p) ^ (q / p)
h_rpow_add_rpow_le_add : ((a ^ p) ^ (q / p) + (b ^ p) ^ (q / p)) ^ (1 / (q / p)) ≤ a ^ p + b ^ p
⊢ (a ^ q + b ^ q) ^ (1 / q) ≤ (a ^ p + b ^ p) ^ (1 / p)
[PROOFSTEP]
rw [h_rpow a, h_rpow b, NNReal.le_rpow_one_div_iff hp_pos, ← NNReal.rpow_mul, mul_comm, mul_one_div]
[GOAL]
ι : Type u
s : Finset ι
p q : ℝ
a b : ℝ≥0
hp_pos : 0 < p
hpq : p ≤ q
h_rpow : ∀ (a : ℝ≥0), a ^ q = (a ^ p) ^ (q / p)
h_rpow_add_rpow_le_add : ((a ^ p) ^ (q / p) + (b ^ p) ^ (q / p)) ^ (1 / (q / p)) ≤ a ^ p + b ^ p
⊢ ((a ^ p) ^ (q / p) + (b ^ p) ^ (q / p)) ^ (p / q) ≤ a ^ p + b ^ p
[PROOFSTEP]
rwa [one_div_div] at h_rpow_add_rpow_le_add 
[GOAL]
ι : Type u
s : Finset ι
p : ℝ
a b : ℝ≥0
hp : 0 ≤ p
hp1 : p ≤ 1
⊢ (a + b) ^ p ≤ a ^ p + b ^ p
[PROOFSTEP]
rcases hp.eq_or_lt with (rfl | hp_pos)
[GOAL]
case inl
ι : Type u
s : Finset ι
a b : ℝ≥0
hp : 0 ≤ 0
hp1 : 0 ≤ 1
⊢ (a + b) ^ 0 ≤ a ^ 0 + b ^ 0
[PROOFSTEP]
simp
[GOAL]
case inr
ι : Type u
s : Finset ι
p : ℝ
a b : ℝ≥0
hp : 0 ≤ p
hp1 : p ≤ 1
hp_pos : 0 < p
⊢ (a + b) ^ p ≤ a ^ p + b ^ p
[PROOFSTEP]
have h := rpow_add_rpow_le a b hp_pos hp1
[GOAL]
case inr
ι : Type u
s : Finset ι
p : ℝ
a b : ℝ≥0
hp : 0 ≤ p
hp1 : p ≤ 1
hp_pos : 0 < p
h : (a ^ 1 + b ^ 1) ^ (1 / 1) ≤ (a ^ p + b ^ p) ^ (1 / p)
⊢ (a + b) ^ p ≤ a ^ p + b ^ p
[PROOFSTEP]
rw [one_div_one] at h 
[GOAL]
case inr
ι : Type u
s : Finset ι
p : ℝ
a b : ℝ≥0
hp : 0 ≤ p
hp1 : p ≤ 1
hp_pos : 0 < p
h : (a ^ 1 + b ^ 1) ^ 1 ≤ (a ^ p + b ^ p) ^ (1 / p)
⊢ (a + b) ^ p ≤ a ^ p + b ^ p
[PROOFSTEP]
repeat' rw [NNReal.rpow_one] at h 
[GOAL]
case inr
ι : Type u
s : Finset ι
p : ℝ
a b : ℝ≥0
hp : 0 ≤ p
hp1 : p ≤ 1
hp_pos : 0 < p
h : (a ^ 1 + b ^ 1) ^ 1 ≤ (a ^ p + b ^ p) ^ (1 / p)
⊢ (a + b) ^ p ≤ a ^ p + b ^ p
[PROOFSTEP]
rw [NNReal.rpow_one] at h 
[GOAL]
case inr
ι : Type u
s : Finset ι
p : ℝ
a b : ℝ≥0
hp : 0 ≤ p
hp1 : p ≤ 1
hp_pos : 0 < p
h : a ^ 1 + b ^ 1 ≤ (a ^ p + b ^ p) ^ (1 / p)
⊢ (a + b) ^ p ≤ a ^ p + b ^ p
[PROOFSTEP]
rw [NNReal.rpow_one] at h 
[GOAL]
case inr
ι : Type u
s : Finset ι
p : ℝ
a b : ℝ≥0
hp : 0 ≤ p
hp1 : p ≤ 1
hp_pos : 0 < p
h : a + b ^ 1 ≤ (a ^ p + b ^ p) ^ (1 / p)
⊢ (a + b) ^ p ≤ a ^ p + b ^ p
[PROOFSTEP]
rw [NNReal.rpow_one] at h 
[GOAL]
case inr
ι : Type u
s : Finset ι
p : ℝ
a b : ℝ≥0
hp : 0 ≤ p
hp1 : p ≤ 1
hp_pos : 0 < p
h : a + b ≤ (a ^ p + b ^ p) ^ (1 / p)
⊢ (a + b) ^ p ≤ a ^ p + b ^ p
[PROOFSTEP]
rw [NNReal.rpow_one] at h 
[GOAL]
case inr
ι : Type u
s : Finset ι
p : ℝ
a b : ℝ≥0
hp : 0 ≤ p
hp1 : p ≤ 1
hp_pos : 0 < p
h : a + b ≤ (a ^ p + b ^ p) ^ (1 / p)
⊢ (a + b) ^ p ≤ a ^ p + b ^ p
[PROOFSTEP]
exact (NNReal.le_rpow_one_div_iff hp_pos).mp h
[GOAL]
ι : Type u
s : Finset ι
w z : ι → ℝ≥0∞
hw' : ∑ i in s, w i = 1
p : ℝ
hp : 1 ≤ p
⊢ (∑ i in s, w i * z i) ^ p ≤ ∑ i in s, w i * z i ^ p
[PROOFSTEP]
have hp_pos : 0 < p
[GOAL]
case hp_pos
ι : Type u
s : Finset ι
w z : ι → ℝ≥0∞
hw' : ∑ i in s, w i = 1
p : ℝ
hp : 1 ≤ p
⊢ 0 < p
ι : Type u
s : Finset ι
w z : ι → ℝ≥0∞
hw' : ∑ i in s, w i = 1
p : ℝ
hp : 1 ≤ p
hp_pos : 0 < p
⊢ (∑ i in s, w i * z i) ^ p ≤ ∑ i in s, w i * z i ^ p
[PROOFSTEP]
positivity
[GOAL]
ι : Type u
s : Finset ι
w z : ι → ℝ≥0∞
hw' : ∑ i in s, w i = 1
p : ℝ
hp : 1 ≤ p
hp_pos : 0 < p
⊢ (∑ i in s, w i * z i) ^ p ≤ ∑ i in s, w i * z i ^ p
[PROOFSTEP]
have hp_nonneg : 0 ≤ p
[GOAL]
case hp_nonneg
ι : Type u
s : Finset ι
w z : ι → ℝ≥0∞
hw' : ∑ i in s, w i = 1
p : ℝ
hp : 1 ≤ p
hp_pos : 0 < p
⊢ 0 ≤ p
ι : Type u
s : Finset ι
w z : ι → ℝ≥0∞
hw' : ∑ i in s, w i = 1
p : ℝ
hp : 1 ≤ p
hp_pos : 0 < p
hp_nonneg : 0 ≤ p
⊢ (∑ i in s, w i * z i) ^ p ≤ ∑ i in s, w i * z i ^ p
[PROOFSTEP]
positivity
[GOAL]
ι : Type u
s : Finset ι
w z : ι → ℝ≥0∞
hw' : ∑ i in s, w i = 1
p : ℝ
hp : 1 ≤ p
hp_pos : 0 < p
hp_nonneg : 0 ≤ p
⊢ (∑ i in s, w i * z i) ^ p ≤ ∑ i in s, w i * z i ^ p
[PROOFSTEP]
have hp_not_neg : ¬p < 0 := by simp [hp_nonneg]
[GOAL]
ι : Type u
s : Finset ι
w z : ι → ℝ≥0∞
hw' : ∑ i in s, w i = 1
p : ℝ
hp : 1 ≤ p
hp_pos : 0 < p
hp_nonneg : 0 ≤ p
⊢ ¬p < 0
[PROOFSTEP]
simp [hp_nonneg]
[GOAL]
ι : Type u
s : Finset ι
w z : ι → ℝ≥0∞
hw' : ∑ i in s, w i = 1
p : ℝ
hp : 1 ≤ p
hp_pos : 0 < p
hp_nonneg : 0 ≤ p
hp_not_neg : ¬p < 0
⊢ (∑ i in s, w i * z i) ^ p ≤ ∑ i in s, w i * z i ^ p
[PROOFSTEP]
have h_top_iff_rpow_top : ∀ (i : ι), i ∈ s → (w i * z i = ⊤ ↔ w i * z i ^ p = ⊤) := by
  simp [ENNReal.mul_eq_top, hp_pos, hp_nonneg, hp_not_neg]
[GOAL]
ι : Type u
s : Finset ι
w z : ι → ℝ≥0∞
hw' : ∑ i in s, w i = 1
p : ℝ
hp : 1 ≤ p
hp_pos : 0 < p
hp_nonneg : 0 ≤ p
hp_not_neg : ¬p < 0
⊢ ∀ (i : ι), i ∈ s → (w i * z i = ⊤ ↔ w i * z i ^ p = ⊤)
[PROOFSTEP]
simp [ENNReal.mul_eq_top, hp_pos, hp_nonneg, hp_not_neg]
[GOAL]
ι : Type u
s : Finset ι
w z : ι → ℝ≥0∞
hw' : ∑ i in s, w i = 1
p : ℝ
hp : 1 ≤ p
hp_pos : 0 < p
hp_nonneg : 0 ≤ p
hp_not_neg : ¬p < 0
h_top_iff_rpow_top : ∀ (i : ι), i ∈ s → (w i * z i = ⊤ ↔ w i * z i ^ p = ⊤)
⊢ (∑ i in s, w i * z i) ^ p ≤ ∑ i in s, w i * z i ^ p
[PROOFSTEP]
refine' le_of_top_imp_top_of_toNNReal_le _ _
[GOAL]
case refine'_1
ι : Type u
s : Finset ι
w z : ι → ℝ≥0∞
hw' : ∑ i in s, w i = 1
p : ℝ
hp : 1 ≤ p
hp_pos : 0 < p
hp_nonneg : 0 ≤ p
hp_not_neg : ¬p < 0
h_top_iff_rpow_top : ∀ (i : ι), i ∈ s → (w i * z i = ⊤ ↔ w i * z i ^ p = ⊤)
⊢ (∑ i in s, w i * z i) ^ p = ⊤ → ∑ i in s, w i * z i ^ p = ⊤
[PROOFSTEP]
rw [rpow_eq_top_iff, sum_eq_top_iff, sum_eq_top_iff]
[GOAL]
case refine'_1
ι : Type u
s : Finset ι
w z : ι → ℝ≥0∞
hw' : ∑ i in s, w i = 1
p : ℝ
hp : 1 ≤ p
hp_pos : 0 < p
hp_nonneg : 0 ≤ p
hp_not_neg : ¬p < 0
h_top_iff_rpow_top : ∀ (i : ι), i ∈ s → (w i * z i = ⊤ ↔ w i * z i ^ p = ⊤)
⊢ ∑ i in s, w i * z i = 0 ∧ p < 0 ∨ (∃ a, a ∈ s ∧ w a * z a = ⊤) ∧ 0 < p → ∃ a, a ∈ s ∧ w a * z a ^ p = ⊤
[PROOFSTEP]
intro h
[GOAL]
case refine'_1
ι : Type u
s : Finset ι
w z : ι → ℝ≥0∞
hw' : ∑ i in s, w i = 1
p : ℝ
hp : 1 ≤ p
hp_pos : 0 < p
hp_nonneg : 0 ≤ p
hp_not_neg : ¬p < 0
h_top_iff_rpow_top : ∀ (i : ι), i ∈ s → (w i * z i = ⊤ ↔ w i * z i ^ p = ⊤)
h : ∑ i in s, w i * z i = 0 ∧ p < 0 ∨ (∃ a, a ∈ s ∧ w a * z a = ⊤) ∧ 0 < p
⊢ ∃ a, a ∈ s ∧ w a * z a ^ p = ⊤
[PROOFSTEP]
simp only [and_false_iff, hp_not_neg, false_or_iff] at h 
[GOAL]
case refine'_1
ι : Type u
s : Finset ι
w z : ι → ℝ≥0∞
hw' : ∑ i in s, w i = 1
p : ℝ
hp : 1 ≤ p
hp_pos : 0 < p
hp_nonneg : 0 ≤ p
hp_not_neg : ¬p < 0
h_top_iff_rpow_top : ∀ (i : ι), i ∈ s → (w i * z i = ⊤ ↔ w i * z i ^ p = ⊤)
h : (∃ a, a ∈ s ∧ w a * z a = ⊤) ∧ 0 < p
⊢ ∃ a, a ∈ s ∧ w a * z a ^ p = ⊤
[PROOFSTEP]
rcases h.left with ⟨a, H, ha⟩
[GOAL]
case refine'_1.intro.intro
ι : Type u
s : Finset ι
w z : ι → ℝ≥0∞
hw' : ∑ i in s, w i = 1
p : ℝ
hp : 1 ≤ p
hp_pos : 0 < p
hp_nonneg : 0 ≤ p
hp_not_neg : ¬p < 0
h_top_iff_rpow_top : ∀ (i : ι), i ∈ s → (w i * z i = ⊤ ↔ w i * z i ^ p = ⊤)
h : (∃ a, a ∈ s ∧ w a * z a = ⊤) ∧ 0 < p
a : ι
H : a ∈ s
ha : w a * z a = ⊤
⊢ ∃ a, a ∈ s ∧ w a * z a ^ p = ⊤
[PROOFSTEP]
use a, H
[GOAL]
case right
ι : Type u
s : Finset ι
w z : ι → ℝ≥0∞
hw' : ∑ i in s, w i = 1
p : ℝ
hp : 1 ≤ p
hp_pos : 0 < p
hp_nonneg : 0 ≤ p
hp_not_neg : ¬p < 0
h_top_iff_rpow_top : ∀ (i : ι), i ∈ s → (w i * z i = ⊤ ↔ w i * z i ^ p = ⊤)
h : (∃ a, a ∈ s ∧ w a * z a = ⊤) ∧ 0 < p
a : ι
H : a ∈ s
ha : w a * z a = ⊤
⊢ w a * z a ^ p = ⊤
[PROOFSTEP]
rwa [← h_top_iff_rpow_top a H]
[GOAL]
case refine'_2
ι : Type u
s : Finset ι
w z : ι → ℝ≥0∞
hw' : ∑ i in s, w i = 1
p : ℝ
hp : 1 ≤ p
hp_pos : 0 < p
hp_nonneg : 0 ≤ p
hp_not_neg : ¬p < 0
h_top_iff_rpow_top : ∀ (i : ι), i ∈ s → (w i * z i = ⊤ ↔ w i * z i ^ p = ⊤)
⊢ (∑ i in s, w i * z i) ^ p ≠ ⊤ →
    ∑ i in s, w i * z i ^ p ≠ ⊤ →
      ENNReal.toNNReal ((∑ i in s, w i * z i) ^ p) ≤ ENNReal.toNNReal (∑ i in s, w i * z i ^ p)
[PROOFSTEP]
intro h_top_rpow_sum
  _
    -- show hypotheses needed to put the `.toNNReal` inside the sums.
[GOAL]
case refine'_2
ι : Type u
s : Finset ι
w z : ι → ℝ≥0∞
hw' : ∑ i in s, w i = 1
p : ℝ
hp : 1 ≤ p
hp_pos : 0 < p
hp_nonneg : 0 ≤ p
hp_not_neg : ¬p < 0
h_top_iff_rpow_top : ∀ (i : ι), i ∈ s → (w i * z i = ⊤ ↔ w i * z i ^ p = ⊤)
h_top_rpow_sum : (∑ i in s, w i * z i) ^ p ≠ ⊤
a✝ : ∑ i in s, w i * z i ^ p ≠ ⊤
⊢ ENNReal.toNNReal ((∑ i in s, w i * z i) ^ p) ≤ ENNReal.toNNReal (∑ i in s, w i * z i ^ p)
[PROOFSTEP]
have h_top : ∀ a : ι, a ∈ s → w a * z a ≠ ⊤ :=
  haveI h_top_sum : ∑ i : ι in s, w i * z i ≠ ⊤ := by
    intro h
    rw [h, top_rpow_of_pos hp_pos] at h_top_rpow_sum 
    exact h_top_rpow_sum rfl
  fun a ha => (lt_top_of_sum_ne_top h_top_sum ha).ne
[GOAL]
ι : Type u
s : Finset ι
w z : ι → ℝ≥0∞
hw' : ∑ i in s, w i = 1
p : ℝ
hp : 1 ≤ p
hp_pos : 0 < p
hp_nonneg : 0 ≤ p
hp_not_neg : ¬p < 0
h_top_iff_rpow_top : ∀ (i : ι), i ∈ s → (w i * z i = ⊤ ↔ w i * z i ^ p = ⊤)
h_top_rpow_sum : (∑ i in s, w i * z i) ^ p ≠ ⊤
a✝ : ∑ i in s, w i * z i ^ p ≠ ⊤
⊢ ∑ i in s, w i * z i ≠ ⊤
[PROOFSTEP]
intro h
[GOAL]
ι : Type u
s : Finset ι
w z : ι → ℝ≥0∞
hw' : ∑ i in s, w i = 1
p : ℝ
hp : 1 ≤ p
hp_pos : 0 < p
hp_nonneg : 0 ≤ p
hp_not_neg : ¬p < 0
h_top_iff_rpow_top : ∀ (i : ι), i ∈ s → (w i * z i = ⊤ ↔ w i * z i ^ p = ⊤)
h_top_rpow_sum : (∑ i in s, w i * z i) ^ p ≠ ⊤
a✝ : ∑ i in s, w i * z i ^ p ≠ ⊤
h : ∑ i in s, w i * z i = ⊤
⊢ False
[PROOFSTEP]
rw [h, top_rpow_of_pos hp_pos] at h_top_rpow_sum 
[GOAL]
ι : Type u
s : Finset ι
w z : ι → ℝ≥0∞
hw' : ∑ i in s, w i = 1
p : ℝ
hp : 1 ≤ p
hp_pos : 0 < p
hp_nonneg : 0 ≤ p
hp_not_neg : ¬p < 0
h_top_iff_rpow_top : ∀ (i : ι), i ∈ s → (w i * z i = ⊤ ↔ w i * z i ^ p = ⊤)
h_top_rpow_sum : ⊤ ≠ ⊤
a✝ : ∑ i in s, w i * z i ^ p ≠ ⊤
h : ∑ i in s, w i * z i = ⊤
⊢ False
[PROOFSTEP]
exact h_top_rpow_sum rfl
[GOAL]
case refine'_2
ι : Type u
s : Finset ι
w z : ι → ℝ≥0∞
hw' : ∑ i in s, w i = 1
p : ℝ
hp : 1 ≤ p
hp_pos : 0 < p
hp_nonneg : 0 ≤ p
hp_not_neg : ¬p < 0
h_top_iff_rpow_top : ∀ (i : ι), i ∈ s → (w i * z i = ⊤ ↔ w i * z i ^ p = ⊤)
h_top_rpow_sum : (∑ i in s, w i * z i) ^ p ≠ ⊤
a✝ : ∑ i in s, w i * z i ^ p ≠ ⊤
h_top : ∀ (a : ι), a ∈ s → w a * z a ≠ ⊤
⊢ ENNReal.toNNReal ((∑ i in s, w i * z i) ^ p) ≤ ENNReal.toNNReal (∑ i in s, w i * z i ^ p)
[PROOFSTEP]
have h_top_rpow : ∀ a : ι, a ∈ s → w a * z a ^ p ≠ ⊤ :=
  by
  intro i hi
  specialize h_top i hi
  rwa [Ne.def, ← h_top_iff_rpow_top i hi]
    -- put the `.toNNReal` inside the sums.
[GOAL]
ι : Type u
s : Finset ι
w z : ι → ℝ≥0∞
hw' : ∑ i in s, w i = 1
p : ℝ
hp : 1 ≤ p
hp_pos : 0 < p
hp_nonneg : 0 ≤ p
hp_not_neg : ¬p < 0
h_top_iff_rpow_top : ∀ (i : ι), i ∈ s → (w i * z i = ⊤ ↔ w i * z i ^ p = ⊤)
h_top_rpow_sum : (∑ i in s, w i * z i) ^ p ≠ ⊤
a✝ : ∑ i in s, w i * z i ^ p ≠ ⊤
h_top : ∀ (a : ι), a ∈ s → w a * z a ≠ ⊤
⊢ ∀ (a : ι), a ∈ s → w a * z a ^ p ≠ ⊤
[PROOFSTEP]
intro i hi
[GOAL]
ι : Type u
s : Finset ι
w z : ι → ℝ≥0∞
hw' : ∑ i in s, w i = 1
p : ℝ
hp : 1 ≤ p
hp_pos : 0 < p
hp_nonneg : 0 ≤ p
hp_not_neg : ¬p < 0
h_top_iff_rpow_top : ∀ (i : ι), i ∈ s → (w i * z i = ⊤ ↔ w i * z i ^ p = ⊤)
h_top_rpow_sum : (∑ i in s, w i * z i) ^ p ≠ ⊤
a✝ : ∑ i in s, w i * z i ^ p ≠ ⊤
h_top : ∀ (a : ι), a ∈ s → w a * z a ≠ ⊤
i : ι
hi : i ∈ s
⊢ w i * z i ^ p ≠ ⊤
[PROOFSTEP]
specialize h_top i hi
[GOAL]
ι : Type u
s : Finset ι
w z : ι → ℝ≥0∞
hw' : ∑ i in s, w i = 1
p : ℝ
hp : 1 ≤ p
hp_pos : 0 < p
hp_nonneg : 0 ≤ p
hp_not_neg : ¬p < 0
h_top_iff_rpow_top : ∀ (i : ι), i ∈ s → (w i * z i = ⊤ ↔ w i * z i ^ p = ⊤)
h_top_rpow_sum : (∑ i in s, w i * z i) ^ p ≠ ⊤
a✝ : ∑ i in s, w i * z i ^ p ≠ ⊤
i : ι
hi : i ∈ s
h_top : w i * z i ≠ ⊤
⊢ w i * z i ^ p ≠ ⊤
[PROOFSTEP]
rwa [Ne.def, ← h_top_iff_rpow_top i hi]
  -- put the `.toNNReal` inside the sums.
[GOAL]
case refine'_2
ι : Type u
s : Finset ι
w z : ι → ℝ≥0∞
hw' : ∑ i in s, w i = 1
p : ℝ
hp : 1 ≤ p
hp_pos : 0 < p
hp_nonneg : 0 ≤ p
hp_not_neg : ¬p < 0
h_top_iff_rpow_top : ∀ (i : ι), i ∈ s → (w i * z i = ⊤ ↔ w i * z i ^ p = ⊤)
h_top_rpow_sum : (∑ i in s, w i * z i) ^ p ≠ ⊤
a✝ : ∑ i in s, w i * z i ^ p ≠ ⊤
h_top : ∀ (a : ι), a ∈ s → w a * z a ≠ ⊤
h_top_rpow : ∀ (a : ι), a ∈ s → w a * z a ^ p ≠ ⊤
⊢ ENNReal.toNNReal ((∑ i in s, w i * z i) ^ p) ≤ ENNReal.toNNReal (∑ i in s, w i * z i ^ p)
[PROOFSTEP]
simp_rw [toNNReal_sum h_top_rpow, ← toNNReal_rpow, toNNReal_sum h_top, toNNReal_mul, ← toNNReal_rpow]
  -- use corresponding nnreal result
[GOAL]
case refine'_2
ι : Type u
s : Finset ι
w z : ι → ℝ≥0∞
hw' : ∑ i in s, w i = 1
p : ℝ
hp : 1 ≤ p
hp_pos : 0 < p
hp_nonneg : 0 ≤ p
hp_not_neg : ¬p < 0
h_top_iff_rpow_top : ∀ (i : ι), i ∈ s → (w i * z i = ⊤ ↔ w i * z i ^ p = ⊤)
h_top_rpow_sum : (∑ i in s, w i * z i) ^ p ≠ ⊤
a✝ : ∑ i in s, w i * z i ^ p ≠ ⊤
h_top : ∀ (a : ι), a ∈ s → w a * z a ≠ ⊤
h_top_rpow : ∀ (a : ι), a ∈ s → w a * z a ^ p ≠ ⊤
⊢ (∑ x in s, ENNReal.toNNReal (w x) * ENNReal.toNNReal (z x)) ^ p ≤
    ∑ x in s, ENNReal.toNNReal (w x) * ENNReal.toNNReal (z x) ^ p
[PROOFSTEP]
refine' NNReal.rpow_arith_mean_le_arith_mean_rpow s (fun i => (w i).toNNReal) (fun i => (z i).toNNReal) _ hp
[GOAL]
case refine'_2
ι : Type u
s : Finset ι
w z : ι → ℝ≥0∞
hw' : ∑ i in s, w i = 1
p : ℝ
hp : 1 ≤ p
hp_pos : 0 < p
hp_nonneg : 0 ≤ p
hp_not_neg : ¬p < 0
h_top_iff_rpow_top : ∀ (i : ι), i ∈ s → (w i * z i = ⊤ ↔ w i * z i ^ p = ⊤)
h_top_rpow_sum : (∑ i in s, w i * z i) ^ p ≠ ⊤
a✝ : ∑ i in s, w i * z i ^ p ≠ ⊤
h_top : ∀ (a : ι), a ∈ s → w a * z a ≠ ⊤
h_top_rpow : ∀ (a : ι), a ∈ s → w a * z a ^ p ≠ ⊤
⊢ ∑ i in s, (fun i => ENNReal.toNNReal (w i)) i = 1
[PROOFSTEP]
have h_sum_nnreal : ∑ i in s, w i = ↑(∑ i in s, (w i).toNNReal) :=
  by
  rw [coe_finset_sum]
  refine' sum_congr rfl fun i hi => (coe_toNNReal _).symm
  refine' (lt_top_of_sum_ne_top _ hi).ne
  exact hw'.symm ▸ ENNReal.one_ne_top
[GOAL]
ι : Type u
s : Finset ι
w z : ι → ℝ≥0∞
hw' : ∑ i in s, w i = 1
p : ℝ
hp : 1 ≤ p
hp_pos : 0 < p
hp_nonneg : 0 ≤ p
hp_not_neg : ¬p < 0
h_top_iff_rpow_top : ∀ (i : ι), i ∈ s → (w i * z i = ⊤ ↔ w i * z i ^ p = ⊤)
h_top_rpow_sum : (∑ i in s, w i * z i) ^ p ≠ ⊤
a✝ : ∑ i in s, w i * z i ^ p ≠ ⊤
h_top : ∀ (a : ι), a ∈ s → w a * z a ≠ ⊤
h_top_rpow : ∀ (a : ι), a ∈ s → w a * z a ^ p ≠ ⊤
⊢ ∑ i in s, w i = ↑(∑ i in s, ENNReal.toNNReal (w i))
[PROOFSTEP]
rw [coe_finset_sum]
[GOAL]
ι : Type u
s : Finset ι
w z : ι → ℝ≥0∞
hw' : ∑ i in s, w i = 1
p : ℝ
hp : 1 ≤ p
hp_pos : 0 < p
hp_nonneg : 0 ≤ p
hp_not_neg : ¬p < 0
h_top_iff_rpow_top : ∀ (i : ι), i ∈ s → (w i * z i = ⊤ ↔ w i * z i ^ p = ⊤)
h_top_rpow_sum : (∑ i in s, w i * z i) ^ p ≠ ⊤
a✝ : ∑ i in s, w i * z i ^ p ≠ ⊤
h_top : ∀ (a : ι), a ∈ s → w a * z a ≠ ⊤
h_top_rpow : ∀ (a : ι), a ∈ s → w a * z a ^ p ≠ ⊤
⊢ ∑ i in s, w i = ∑ a in s, ↑(ENNReal.toNNReal (w a))
[PROOFSTEP]
refine' sum_congr rfl fun i hi => (coe_toNNReal _).symm
[GOAL]
ι : Type u
s : Finset ι
w z : ι → ℝ≥0∞
hw' : ∑ i in s, w i = 1
p : ℝ
hp : 1 ≤ p
hp_pos : 0 < p
hp_nonneg : 0 ≤ p
hp_not_neg : ¬p < 0
h_top_iff_rpow_top : ∀ (i : ι), i ∈ s → (w i * z i = ⊤ ↔ w i * z i ^ p = ⊤)
h_top_rpow_sum : (∑ i in s, w i * z i) ^ p ≠ ⊤
a✝ : ∑ i in s, w i * z i ^ p ≠ ⊤
h_top : ∀ (a : ι), a ∈ s → w a * z a ≠ ⊤
h_top_rpow : ∀ (a : ι), a ∈ s → w a * z a ^ p ≠ ⊤
i : ι
hi : i ∈ s
⊢ w i ≠ ⊤
[PROOFSTEP]
refine' (lt_top_of_sum_ne_top _ hi).ne
[GOAL]
ι : Type u
s : Finset ι
w z : ι → ℝ≥0∞
hw' : ∑ i in s, w i = 1
p : ℝ
hp : 1 ≤ p
hp_pos : 0 < p
hp_nonneg : 0 ≤ p
hp_not_neg : ¬p < 0
h_top_iff_rpow_top : ∀ (i : ι), i ∈ s → (w i * z i = ⊤ ↔ w i * z i ^ p = ⊤)
h_top_rpow_sum : (∑ i in s, w i * z i) ^ p ≠ ⊤
a✝ : ∑ i in s, w i * z i ^ p ≠ ⊤
h_top : ∀ (a : ι), a ∈ s → w a * z a ≠ ⊤
h_top_rpow : ∀ (a : ι), a ∈ s → w a * z a ^ p ≠ ⊤
i : ι
hi : i ∈ s
⊢ ∑ x in s, w x ≠ ⊤
[PROOFSTEP]
exact hw'.symm ▸ ENNReal.one_ne_top
[GOAL]
case refine'_2
ι : Type u
s : Finset ι
w z : ι → ℝ≥0∞
hw' : ∑ i in s, w i = 1
p : ℝ
hp : 1 ≤ p
hp_pos : 0 < p
hp_nonneg : 0 ≤ p
hp_not_neg : ¬p < 0
h_top_iff_rpow_top : ∀ (i : ι), i ∈ s → (w i * z i = ⊤ ↔ w i * z i ^ p = ⊤)
h_top_rpow_sum : (∑ i in s, w i * z i) ^ p ≠ ⊤
a✝ : ∑ i in s, w i * z i ^ p ≠ ⊤
h_top : ∀ (a : ι), a ∈ s → w a * z a ≠ ⊤
h_top_rpow : ∀ (a : ι), a ∈ s → w a * z a ^ p ≠ ⊤
h_sum_nnreal : ∑ i in s, w i = ↑(∑ i in s, ENNReal.toNNReal (w i))
⊢ ∑ i in s, (fun i => ENNReal.toNNReal (w i)) i = 1
[PROOFSTEP]
rwa [← coe_eq_coe, ← h_sum_nnreal]
[GOAL]
ι : Type u
s : Finset ι
w₁ w₂ z₁ z₂ : ℝ≥0∞
hw' : w₁ + w₂ = 1
p : ℝ
hp : 1 ≤ p
⊢ (w₁ * z₁ + w₂ * z₂) ^ p ≤ w₁ * z₁ ^ p + w₂ * z₂ ^ p
[PROOFSTEP]
have h := rpow_arith_mean_le_arith_mean_rpow univ ![w₁, w₂] ![z₁, z₂] ?_ hp
[GOAL]
case refine_2
ι : Type u
s : Finset ι
w₁ w₂ z₁ z₂ : ℝ≥0∞
hw' : w₁ + w₂ = 1
p : ℝ
hp : 1 ≤ p
h :
  (∑ i : Fin (Nat.succ (Nat.succ 0)), Matrix.vecCons w₁ ![w₂] i * Matrix.vecCons z₁ ![z₂] i) ^ p ≤
    ∑ i : Fin (Nat.succ (Nat.succ 0)), Matrix.vecCons w₁ ![w₂] i * Matrix.vecCons z₁ ![z₂] i ^ p
⊢ (w₁ * z₁ + w₂ * z₂) ^ p ≤ w₁ * z₁ ^ p + w₂ * z₂ ^ p
[PROOFSTEP]
simpa [Fin.sum_univ_succ] using h
[GOAL]
case refine_1
ι : Type u
s : Finset ι
w₁ w₂ z₁ z₂ : ℝ≥0∞
hw' : w₁ + w₂ = 1
p : ℝ
hp : 1 ≤ p
⊢ ∑ i : Fin (Nat.succ (Nat.succ 0)), Matrix.vecCons w₁ ![w₂] i = 1
[PROOFSTEP]
simp [hw', Fin.sum_univ_succ]
[GOAL]
ι : Type u
s : Finset ι
z₁ z₂ : ℝ≥0∞
p : ℝ
hp : 1 ≤ p
⊢ (z₁ + z₂) ^ p ≤ 2 ^ (p - 1) * (z₁ ^ p + z₂ ^ p)
[PROOFSTEP]
rcases eq_or_lt_of_le hp with (rfl | h'p)
[GOAL]
case inl
ι : Type u
s : Finset ι
z₁ z₂ : ℝ≥0∞
hp : 1 ≤ 1
⊢ (z₁ + z₂) ^ 1 ≤ 2 ^ (1 - 1) * (z₁ ^ 1 + z₂ ^ 1)
[PROOFSTEP]
simp only [rpow_one, sub_self, rpow_zero, one_mul, le_refl]
[GOAL]
case inr
ι : Type u
s : Finset ι
z₁ z₂ : ℝ≥0∞
p : ℝ
hp : 1 ≤ p
h'p : 1 < p
⊢ (z₁ + z₂) ^ p ≤ 2 ^ (p - 1) * (z₁ ^ p + z₂ ^ p)
[PROOFSTEP]
convert rpow_arith_mean_le_arith_mean2_rpow (1 / 2) (1 / 2) (2 * z₁) (2 * z₂) (ENNReal.add_halves 1) hp using 1
[GOAL]
case h.e'_3
ι : Type u
s : Finset ι
z₁ z₂ : ℝ≥0∞
p : ℝ
hp : 1 ≤ p
h'p : 1 < p
⊢ (z₁ + z₂) ^ p = (1 / 2 * (2 * z₁) + 1 / 2 * (2 * z₂)) ^ p
[PROOFSTEP]
simp [← mul_assoc, ENNReal.inv_mul_cancel two_ne_zero two_ne_top]
[GOAL]
case h.e'_4
ι : Type u
s : Finset ι
z₁ z₂ : ℝ≥0∞
p : ℝ
hp : 1 ≤ p
h'p : 1 < p
⊢ 2 ^ (p - 1) * (z₁ ^ p + z₂ ^ p) = 1 / 2 * (2 * z₁) ^ p + 1 / 2 * (2 * z₂) ^ p
[PROOFSTEP]
have _ : p - 1 ≠ 0 := ne_of_gt (sub_pos.2 h'p)
[GOAL]
case h.e'_4
ι : Type u
s : Finset ι
z₁ z₂ : ℝ≥0∞
p : ℝ
hp : 1 ≤ p
h'p : 1 < p
x✝ : p - 1 ≠ 0
⊢ 2 ^ (p - 1) * (z₁ ^ p + z₂ ^ p) = 1 / 2 * (2 * z₁) ^ p + 1 / 2 * (2 * z₂) ^ p
[PROOFSTEP]
simp only [mul_rpow_of_nonneg _ _ (zero_le_one.trans hp), rpow_sub _ _ two_ne_zero two_ne_top, ENNReal.div_eq_inv_mul,
  rpow_one, mul_one]
[GOAL]
case h.e'_4
ι : Type u
s : Finset ι
z₁ z₂ : ℝ≥0∞
p : ℝ
hp : 1 ≤ p
h'p : 1 < p
x✝ : p - 1 ≠ 0
⊢ 2⁻¹ * 2 ^ p * (z₁ ^ p + z₂ ^ p) = 2⁻¹ * (2 ^ p * z₁ ^ p) + 2⁻¹ * (2 ^ p * z₂ ^ p)
[PROOFSTEP]
ring
[GOAL]
ι : Type u
s : Finset ι
p : ℝ
a b : ℝ≥0∞
hp1 : 1 ≤ p
⊢ a ^ p + b ^ p ≤ (a + b) ^ p
[PROOFSTEP]
have hp_pos : 0 < p := by positivity
[GOAL]
ι : Type u
s : Finset ι
p : ℝ
a b : ℝ≥0∞
hp1 : 1 ≤ p
⊢ 0 < p
[PROOFSTEP]
positivity
[GOAL]
ι : Type u
s : Finset ι
p : ℝ
a b : ℝ≥0∞
hp1 : 1 ≤ p
hp_pos : 0 < p
⊢ a ^ p + b ^ p ≤ (a + b) ^ p
[PROOFSTEP]
by_cases h_top : a + b = ⊤
[GOAL]
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
[PROOFSTEP]
rw [← @ENNReal.rpow_eq_top_iff_of_pos (a + b) p hp_pos] at h_top 
[GOAL]
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
[PROOFSTEP]
rw [h_top]
[GOAL]
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 ≤ ⊤
[PROOFSTEP]
exact le_top
[GOAL]
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
[PROOFSTEP]
obtain ⟨ha_top, hb_top⟩ := add_ne_top.mp h_top
[GOAL]
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
[PROOFSTEP]
lift a to ℝ≥0 using ha_top
[GOAL]
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
[PROOFSTEP]
lift b to ℝ≥0 using hb_top
[GOAL]
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
[PROOFSTEP]
simpa [← ENNReal.coe_rpow_of_nonneg _ hp_pos.le] using ENNReal.coe_le_coe.2 (NNReal.add_rpow_le_rpow_add a b hp1)
[GOAL]
ι : Type u
s : Finset ι
p : ℝ
a b : ℝ≥0∞
hp1 : 1 ≤ p
⊢ (a ^ p + b ^ p) ^ (1 / p) ≤ a + b
[PROOFSTEP]
rw [← @ENNReal.le_rpow_one_div_iff _ _ (1 / p) (by simp [lt_of_lt_of_le zero_lt_one hp1])]
[GOAL]
ι : Type u
s : Finset ι
p : ℝ
a b : ℝ≥0∞
hp1 : 1 ≤ p
⊢ 0 < 1 / p
[PROOFSTEP]
simp [lt_of_lt_of_le zero_lt_one hp1]
[GOAL]
ι : Type u
s : Finset ι
p : ℝ
a b : ℝ≥0∞
hp1 : 1 ≤ p
⊢ a ^ p + b ^ p ≤ (a + b) ^ (1 / (1 / p))
[PROOFSTEP]
rw [one_div_one_div]
[GOAL]
ι : Type u
s : Finset ι
p : ℝ
a b : ℝ≥0∞
hp1 : 1 ≤ p
⊢ a ^ p + b ^ p ≤ (a + b) ^ p
[PROOFSTEP]
exact add_rpow_le_rpow_add _ _ hp1
[GOAL]
ι : Type u
s : Finset ι
p q : ℝ
a b : ℝ≥0∞
hp_pos : 0 < p
hpq : p ≤ q
⊢ (a ^ q + b ^ q) ^ (1 / q) ≤ (a ^ p + b ^ p) ^ (1 / p)
[PROOFSTEP]
have h_rpow : ∀ a : ℝ≥0∞, a ^ q = (a ^ p) ^ (q / p) := fun a => by
  rw [← ENNReal.rpow_mul, _root_.mul_div_cancel' _ hp_pos.ne']
[GOAL]
ι : Type u
s : Finset ι
p q : ℝ
a✝ b : ℝ≥0∞
hp_pos : 0 < p
hpq : p ≤ q
a : ℝ≥0∞
⊢ a ^ q = (a ^ p) ^ (q / p)
[PROOFSTEP]
rw [← ENNReal.rpow_mul, _root_.mul_div_cancel' _ hp_pos.ne']
[GOAL]
ι : Type u
s : Finset ι
p q : ℝ
a b : ℝ≥0∞
hp_pos : 0 < p
hpq : p ≤ q
h_rpow : ∀ (a : ℝ≥0∞), a ^ q = (a ^ p) ^ (q / p)
⊢ (a ^ q + b ^ q) ^ (1 / q) ≤ (a ^ p + b ^ p) ^ (1 / p)
[PROOFSTEP]
have h_rpow_add_rpow_le_add : ((a ^ p) ^ (q / p) + (b ^ p) ^ (q / p)) ^ (1 / (q / p)) ≤ a ^ p + b ^ p :=
  by
  refine' rpow_add_rpow_le_add (a ^ p) (b ^ p) _
  rwa [one_le_div hp_pos]
[GOAL]
ι : Type u
s : Finset ι
p q : ℝ
a b : ℝ≥0∞
hp_pos : 0 < p
hpq : p ≤ q
h_rpow : ∀ (a : ℝ≥0∞), a ^ q = (a ^ p) ^ (q / p)
⊢ ((a ^ p) ^ (q / p) + (b ^ p) ^ (q / p)) ^ (1 / (q / p)) ≤ a ^ p + b ^ p
[PROOFSTEP]
refine' rpow_add_rpow_le_add (a ^ p) (b ^ p) _
[GOAL]
ι : Type u
s : Finset ι
p q : ℝ
a b : ℝ≥0∞
hp_pos : 0 < p
hpq : p ≤ q
h_rpow : ∀ (a : ℝ≥0∞), a ^ q = (a ^ p) ^ (q / p)
⊢ 1 ≤ q / p
[PROOFSTEP]
rwa [one_le_div hp_pos]
[GOAL]
ι : Type u
s : Finset ι
p q : ℝ
a b : ℝ≥0∞
hp_pos : 0 < p
hpq : p ≤ q
h_rpow : ∀ (a : ℝ≥0∞), a ^ q = (a ^ p) ^ (q / p)
h_rpow_add_rpow_le_add : ((a ^ p) ^ (q / p) + (b ^ p) ^ (q / p)) ^ (1 / (q / p)) ≤ a ^ p + b ^ p
⊢ (a ^ q + b ^ q) ^ (1 / q) ≤ (a ^ p + b ^ p) ^ (1 / p)
[PROOFSTEP]
rw [h_rpow a, h_rpow b, ENNReal.le_rpow_one_div_iff hp_pos, ← ENNReal.rpow_mul, mul_comm, mul_one_div]
[GOAL]
ι : Type u
s : Finset ι
p q : ℝ
a b : ℝ≥0∞
hp_pos : 0 < p
hpq : p ≤ q
h_rpow : ∀ (a : ℝ≥0∞), a ^ q = (a ^ p) ^ (q / p)
h_rpow_add_rpow_le_add : ((a ^ p) ^ (q / p) + (b ^ p) ^ (q / p)) ^ (1 / (q / p)) ≤ a ^ p + b ^ p
⊢ ((a ^ p) ^ (q / p) + (b ^ p) ^ (q / p)) ^ (p / q) ≤ a ^ p + b ^ p
[PROOFSTEP]
rwa [one_div_div] at h_rpow_add_rpow_le_add 
[GOAL]
ι : Type u
s : Finset ι
p : ℝ
a b : ℝ≥0∞
hp : 0 ≤ p
hp1 : p ≤ 1
⊢ (a + b) ^ p ≤ a ^ p + b ^ p
[PROOFSTEP]
rcases hp.eq_or_lt with (rfl | hp_pos)
[GOAL]
case inl
ι : Type u
s : Finset ι
a b : ℝ≥0∞
hp : 0 ≤ 0
hp1 : 0 ≤ 1
⊢ (a + b) ^ 0 ≤ a ^ 0 + b ^ 0
[PROOFSTEP]
simp
[GOAL]
case inr
ι : Type u
s : Finset ι
p : ℝ
a b : ℝ≥0∞
hp : 0 ≤ p
hp1 : p ≤ 1
hp_pos : 0 < p
⊢ (a + b) ^ p ≤ a ^ p + b ^ p
[PROOFSTEP]
have h := rpow_add_rpow_le a b hp_pos hp1
[GOAL]
case inr
ι : Type u
s : Finset ι
p : ℝ
a b : ℝ≥0∞
hp : 0 ≤ p
hp1 : p ≤ 1
hp_pos : 0 < p
h : (a ^ 1 + b ^ 1) ^ (1 / 1) ≤ (a ^ p + b ^ p) ^ (1 / p)
⊢ (a + b) ^ p ≤ a ^ p + b ^ p
[PROOFSTEP]
rw [one_div_one] at h 
[GOAL]
case inr
ι : Type u
s : Finset ι
p : ℝ
a b : ℝ≥0∞
hp : 0 ≤ p
hp1 : p ≤ 1
hp_pos : 0 < p
h : (a ^ 1 + b ^ 1) ^ 1 ≤ (a ^ p + b ^ p) ^ (1 / p)
⊢ (a + b) ^ p ≤ a ^ p + b ^ p
[PROOFSTEP]
repeat' rw [ENNReal.rpow_one] at h 
[GOAL]
case inr
ι : Type u
s : Finset ι
p : ℝ
a b : ℝ≥0∞
hp : 0 ≤ p
hp1 : p ≤ 1
hp_pos : 0 < p
h : (a ^ 1 + b ^ 1) ^ 1 ≤ (a ^ p + b ^ p) ^ (1 / p)
⊢ (a + b) ^ p ≤ a ^ p + b ^ p
[PROOFSTEP]
rw [ENNReal.rpow_one] at h 
[GOAL]
case inr
ι : Type u
s : Finset ι
p : ℝ
a b : ℝ≥0∞
hp : 0 ≤ p
hp1 : p ≤ 1
hp_pos : 0 < p
h : a ^ 1 + b ^ 1 ≤ (a ^ p + b ^ p) ^ (1 / p)
⊢ (a + b) ^ p ≤ a ^ p + b ^ p
[PROOFSTEP]
rw [ENNReal.rpow_one] at h 
[GOAL]
case inr
ι : Type u
s : Finset ι
p : ℝ
a b : ℝ≥0∞
hp : 0 ≤ p
hp1 : p ≤ 1
hp_pos : 0 < p
h : a + b ^ 1 ≤ (a ^ p + b ^ p) ^ (1 / p)
⊢ (a + b) ^ p ≤ a ^ p + b ^ p
[PROOFSTEP]
rw [ENNReal.rpow_one] at h 
[GOAL]
case inr
ι : Type u
s : Finset ι
p : ℝ
a b : ℝ≥0∞
hp : 0 ≤ p
hp1 : p ≤ 1
hp_pos : 0 < p
h : a + b ≤ (a ^ p + b ^ p) ^ (1 / p)
⊢ (a + b) ^ p ≤ a ^ p + b ^ p
[PROOFSTEP]
rw [ENNReal.rpow_one] at h 
[GOAL]
case inr
ι : Type u
s : Finset ι
p : ℝ
a b : ℝ≥0∞
hp : 0 ≤ p
hp1 : p ≤ 1
hp_pos : 0 < p
h : a + b ≤ (a ^ p + b ^ p) ^ (1 / p)
⊢ (a + b) ^ p ≤ a ^ p + b ^ p
[PROOFSTEP]
exact (ENNReal.le_rpow_one_div_iff hp_pos).mp h
