n : ℕ
⊢ ConvexOn ℝ (Ioi 0) fun x => x ^ n
n : ℕ
⊢ ConvexOn ℝ (Ioi 0) fun x => x ^ ↑n
simp_rw [zpow_ofNat]
no goals
n : ℕ
⊢ ConvexOn ℝ (Ioi 0) fun x => x ^ n
exact (convexOn_pow n).subset Ioi_subset_Ici_self (convex_Ioi _)
n : ℕ
⊢ ConvexOn ℝ (Ioi 0) fun x => (x ^ (n + 1))⁻¹
n : ℕ
⊢ ConvexOn ℝ (Ioi 0) fun x => x ^ -[n+1]
simp_rw [zpow_negSucc]
n : ℕ
⊢ ∀ ⦃x : ℝ⦄,
    x ∈ Ioi 0 →
      ∀ ⦃y : ℝ⦄,
        y ∈ Ioi 0 →
          ∀ ⦃a b : ℝ⦄,
            0 ≤ a →
              0 ≤ b →
                a + b = 1 →
                  (fun x => (x ^ (n + 1))⁻¹) (a • x + b • y) ≤
                    a • (fun x => (x ^ (n + 1))⁻¹) x + b • (fun x => (x ^ (n + 1))⁻¹) y
n : ℕ
⊢ ConvexOn ℝ (Ioi 0) fun x => (x ^ (n + 1))⁻¹
refine' ⟨convex_Ioi _, _⟩
n : ℕ
a : ℝ
ha : 0 < a
b : ℝ
hb : 0 < b
μ ν : ℝ
hμ : 0 ≤ μ
hν : 0 ≤ ν
h : μ + ν = 1
⊢ (fun x => (x ^ (n + 1))⁻¹) (μ • a + ν • b) ≤ μ • (fun x => (x ^ (n + 1))⁻¹) a + ν • (fun x => (x ^ (n + 1))⁻¹) b
n : ℕ
⊢ ∀ ⦃x : ℝ⦄,
    x ∈ Ioi 0 →
      ∀ ⦃y : ℝ⦄,
        y ∈ Ioi 0 →
          ∀ ⦃a b : ℝ⦄,
            0 ≤ a →
              0 ≤ b →
                a + b = 1 →
                  (fun x => (x ^ (n + 1))⁻¹) (a • x + b • y) ≤
                    a • (fun x => (x ^ (n + 1))⁻¹) x + b • (fun x => (x ^ (n + 1))⁻¹) y
rintro a (ha : 0 < a) b (hb : 0 < b) μ ν hμ hν h
n : ℕ
a : ℝ
ha : 0 < a
b : ℝ
hb : 0 < b
μ ν : ℝ
hμ : 0 ≤ μ
hν : 0 ≤ ν
h : μ + ν = 1
⊢ 1 / (μ * a + ν * b) ^ (n + 1) ≤ (μ * b ^ (n + 1) + ν * a ^ (n + 1)) / (a ^ (n + 1) * b ^ (n + 1))
n : ℕ
a : ℝ
ha : 0 < a
b : ℝ
hb : 0 < b
μ ν : ℝ
hμ : 0 ≤ μ
hν : 0 ≤ ν
h : μ + ν = 1
⊢ (fun x => (x ^ (n + 1))⁻¹) (μ • a + ν • b) ≤ μ • (fun x => (x ^ (n + 1))⁻¹) a + ν • (fun x => (x ^ (n + 1))⁻¹) b
field_simp [ha.ne', hb.ne']
n : ℕ
a : ℝ
ha : 0 < a
b : ℝ
hb : 0 < b
μ ν : ℝ
hμ : 0 ≤ μ
hν : 0 ≤ ν
h : μ + ν = 1
⊢ 1 * (a ^ (n + 1) * b ^ (n + 1)) ≤ (μ * b ^ (n + 1) + ν * a ^ (n + 1)) * (μ * a + ν * b) ^ (n + 1)

case b0
n : ℕ
a : ℝ
ha : 0 < a
b : ℝ
hb : 0 < b
μ ν : ℝ
hμ : 0 ≤ μ
hν : 0 ≤ ν
h : μ + ν = 1
⊢ 0 < (μ * a + ν * b) ^ (n + 1)

case d0
n : ℕ
a : ℝ
ha : 0 < a
b : ℝ
hb : 0 < b
μ ν : ℝ
hμ : 0 ≤ μ
hν : 0 ≤ ν
h : μ + ν = 1
⊢ 0 < a ^ (n + 1) * b ^ (n + 1)
n : ℕ
a : ℝ
ha : 0 < a
b : ℝ
hb : 0 < b
μ ν : ℝ
hμ : 0 ≤ μ
hν : 0 ≤ ν
h : μ + ν = 1
⊢ 1 / (μ * a + ν * b) ^ (n + 1) ≤ (μ * b ^ (n + 1) + ν * a ^ (n + 1)) / (a ^ (n + 1) * b ^ (n + 1))
rw [div_le_div_iff]
case calc_1
n : ℕ
a : ℝ
ha : 0 < a
b : ℝ
hb : 0 < b
μ ν : ℝ
hμ : 0 ≤ μ
hν : 0 ≤ ν
h : μ + ν = 1
⊢ ((μ + ν) ^ 2 * (a * b)) ^ (n + 1) ≤ ((μ * b + ν * a) * (μ * a + ν * b)) ^ (n + 1)

case calc_2
n : ℕ
a : ℝ
ha : 0 < a
b : ℝ
hb : 0 < b
μ ν : ℝ
hμ : 0 ≤ μ
hν : 0 ≤ ν
h : μ + ν = 1
⊢ (μ * b + ν * a) ^ (n + 1) * (μ * a + ν * b) ^ (n + 1) ≤
    (μ * b ^ (n + 1) + ν * a ^ (n + 1)) * (μ * a + ν * b) ^ (n + 1)
n : ℕ
a : ℝ
ha : 0 < a
b : ℝ
hb : 0 < b
μ ν : ℝ
hμ : 0 ≤ μ
hν : 0 ≤ ν
h : μ + ν = 1
⊢ 1 * (a ^ (n + 1) * b ^ (n + 1)) ≤ (μ * b ^ (n + 1) + ν * a ^ (n + 1)) * (μ * a + ν * b) ^ (n + 1)
calc
  (1 : ℝ) * (a ^ (n + 1) * b ^ (n + 1)) = ((μ + ν) ^ 2 * (a * b)) ^ (n + 1) := by rw [h]; ring
  _ ≤ ((μ * b + ν * a) * (μ * a + ν * b)) ^ (n + 1) := ?_
  _ = (μ * b + ν * a) ^ (n + 1) * (μ * a + ν * b) ^ (n + 1) := by rw [mul_pow]
  _ ≤ (μ * b ^ (n + 1) + ν * a ^ (n + 1)) * (μ * a + ν * b) ^ (n + 1) := ?_
n : ℕ
a : ℝ
ha : 0 < a
b : ℝ
hb : 0 < b
μ ν : ℝ
hμ : 0 ≤ μ
hν : 0 ≤ ν
h : μ + ν = 1
⊢ 1 * (a ^ (n + 1) * b ^ (n + 1)) = (1 ^ 2 * (a * b)) ^ (n + 1)
n : ℕ
a : ℝ
ha : 0 < a
b : ℝ
hb : 0 < b
μ ν : ℝ
hμ : 0 ≤ μ
hν : 0 ≤ ν
h : μ + ν = 1
⊢ 1 * (a ^ (n + 1) * b ^ (n + 1)) = ((μ + ν) ^ 2 * (a * b)) ^ (n + 1)
rw [h]
no goals
n : ℕ
a : ℝ
ha : 0 < a
b : ℝ
hb : 0 < b
μ ν : ℝ
hμ : 0 ≤ μ
hν : 0 ≤ ν
h : μ + ν = 1
⊢ 1 * (a ^ (n + 1) * b ^ (n + 1)) = (1 ^ 2 * (a * b)) ^ (n + 1)
ring
no goals
n : ℕ
a : ℝ
ha : 0 < a
b : ℝ
hb : 0 < b
μ ν : ℝ
hμ : 0 ≤ μ
hν : 0 ≤ ν
h : μ + ν = 1
⊢ ((μ * b + ν * a) * (μ * a + ν * b)) ^ (n + 1) = (μ * b + ν * a) ^ (n + 1) * (μ * a + ν * b) ^ (n + 1)
rw [mul_pow]
case calc_1.hab
n : ℕ
a : ℝ
ha : 0 < a
b : ℝ
hb : 0 < b
μ ν : ℝ
hμ : 0 ≤ μ
hν : 0 ≤ ν
h : μ + ν = 1
⊢ (μ + ν) ^ 2 * (a * b) ≤ (μ * b + ν * a) * (μ * a + ν * b)
case calc_1
n : ℕ
a : ℝ
ha : 0 < a
b : ℝ
hb : 0 < b
μ ν : ℝ
hμ : 0 ≤ μ
hν : 0 ≤ ν
h : μ + ν = 1
⊢ ((μ + ν) ^ 2 * (a * b)) ^ (n + 1) ≤ ((μ * b + ν * a) * (μ * a + ν * b)) ^ (n + 1)
gcongr (?_ : ℝ) ^ _
case calc_1.hab
n : ℕ
a : ℝ
ha : 0 < a
b : ℝ
hb : 0 < b
μ ν : ℝ
hμ : 0 ≤ μ
hν : 0 ≤ ν
h : μ + ν = 1
this : 0 ≤ μ * ν * (a - b) ^ 2
⊢ (μ + ν) ^ 2 * (a * b) ≤ (μ * b + ν * a) * (μ * a + ν * b)
case calc_1.hab
n : ℕ
a : ℝ
ha : 0 < a
b : ℝ
hb : 0 < b
μ ν : ℝ
hμ : 0 ≤ μ
hν : 0 ≤ ν
h : μ + ν = 1
⊢ (μ + ν) ^ 2 * (a * b) ≤ (μ * b + ν * a) * (μ * a + ν * b)
have : (0 : ℝ) ≤ μ * ν * (a - b) ^ 2 := by positivity
no goals
case calc_1.hab
n : ℕ
a : ℝ
ha : 0 < a
b : ℝ
hb : 0 < b
μ ν : ℝ
hμ : 0 ≤ μ
hν : 0 ≤ ν
h : μ + ν = 1
this : 0 ≤ μ * ν * (a - b) ^ 2
⊢ (μ + ν) ^ 2 * (a * b) ≤ (μ * b + ν * a) * (μ * a + ν * b)
linarith
no goals
n : ℕ
a : ℝ
ha : 0 < a
b : ℝ
hb : 0 < b
μ ν : ℝ
hμ : 0 ≤ μ
hν : 0 ≤ ν
h : μ + ν = 1
⊢ 0 ≤ μ * ν * (a - b) ^ 2
positivity
case calc_2.h
n : ℕ
a : ℝ
ha : 0 < a
b : ℝ
hb : 0 < b
μ ν : ℝ
hμ : 0 ≤ μ
hν : 0 ≤ ν
h : μ + ν = 1
⊢ (μ * b + ν * a) ^ (n + 1) ≤ μ * b ^ (n + 1) + ν * a ^ (n + 1)
case calc_2
n : ℕ
a : ℝ
ha : 0 < a
b : ℝ
hb : 0 < b
μ ν : ℝ
hμ : 0 ≤ μ
hν : 0 ≤ ν
h : μ + ν = 1
⊢ (μ * b + ν * a) ^ (n + 1) * (μ * a + ν * b) ^ (n + 1) ≤
    (μ * b ^ (n + 1) + ν * a ^ (n + 1)) * (μ * a + ν * b) ^ (n + 1)
gcongr
no goals
case calc_2.h
n : ℕ
a : ℝ
ha : 0 < a
b : ℝ
hb : 0 < b
μ ν : ℝ
hμ : 0 ≤ μ
hν : 0 ≤ ν
h : μ + ν = 1
⊢ (μ * b + ν * a) ^ (n + 1) ≤ μ * b ^ (n + 1) + ν * a ^ (n + 1)
apply (convexOn_pow (n + 1)).2 hb.le ha.le hμ hν h
case b0
n : ℕ
a : ℝ
ha : 0 < a
b : ℝ
hb : 0 < b
μ ν : ℝ
hμ : 0 ≤ μ
hν : 0 ≤ ν
h : μ + ν = 1
this : 0 < μ * a + ν * b
⊢ 0 < (μ * a + ν * b) ^ (n + 1)
case b0
n : ℕ
a : ℝ
ha : 0 < a
b : ℝ
hb : 0 < b
μ ν : ℝ
hμ : 0 ≤ μ
hν : 0 ≤ ν
h : μ + ν = 1
⊢ 0 < (μ * a + ν * b) ^ (n + 1)
have : 0 < μ * a + ν * b := by cases le_or_lt a b <;> nlinarith
no goals
case b0
n : ℕ
a : ℝ
ha : 0 < a
b : ℝ
hb : 0 < b
μ ν : ℝ
hμ : 0 ≤ μ
hν : 0 ≤ ν
h : μ + ν = 1
this : 0 < μ * a + ν * b
⊢ 0 < (μ * a + ν * b) ^ (n + 1)
positivity
no goals
n : ℕ
a : ℝ
ha : 0 < a
b : ℝ
hb : 0 < b
μ ν : ℝ
hμ : 0 ≤ μ
hν : 0 ≤ ν
h : μ + ν = 1
⊢ 0 < μ * a + ν * b
cases le_or_lt a b <;> nlinarith
no goals
case d0
n : ℕ
a : ℝ
ha : 0 < a
b : ℝ
hb : 0 < b
μ ν : ℝ
hμ : 0 ≤ μ
hν : 0 ≤ ν
h : μ + ν = 1
⊢ 0 < a ^ (n + 1) * b ^ (n + 1)
positivity