n : ℕ
hn : Even n
⊢ ∀ ⦃x : ℝ⦄,
    x ∈ univ →
      ∀ ⦃y : ℝ⦄,
        y ∈ univ →
          ∀ ⦃a b : ℝ⦄,
            0 ≤ a →
              0 ≤ b → a + b = 1 → (fun x => x ^ n) (a • x + b • y) ≤ a • (fun x => x ^ n) x + b • (fun x => x ^ n) y
n : ℕ
hn : Even n
⊢ ConvexOn ℝ univ fun x => x ^ n
refine' ⟨convex_univ, _⟩
n : ℕ
hn : Even n
a b μ ν : ℝ
hμ : 0 ≤ μ
hν : 0 ≤ ν
h : μ + ν = 1
⊢ (fun x => x ^ n) (μ • a + ν • b) ≤ μ • (fun x => x ^ n) a + ν • (fun x => x ^ n) b
n : ℕ
hn : Even n
⊢ ∀ ⦃x : ℝ⦄,
    x ∈ univ →
      ∀ ⦃y : ℝ⦄,
        y ∈ univ →
          ∀ ⦃a b : ℝ⦄,
            0 ≤ a →
              0 ≤ b → a + b = 1 → (fun x => x ^ n) (a • x + b • y) ≤ a • (fun x => x ^ n) x + b • (fun x => x ^ n) y
rintro a - b - μ ν hμ hν h
case intro
a b μ ν : ℝ
hμ : 0 ≤ μ
hν : 0 ≤ ν
h : μ + ν = 1
k : ℕ
hn : Even (2 • k)
⊢ (fun x => x ^ (2 • k)) (μ • a + ν • b) ≤ μ • (fun x => x ^ (2 • k)) a + ν • (fun x => x ^ (2 • k)) b
n : ℕ
hn : Even n
a b μ ν : ℝ
hμ : 0 ≤ μ
hν : 0 ≤ ν
h : μ + ν = 1
⊢ (fun x => x ^ n) (μ • a + ν • b) ≤ μ • (fun x => x ^ n) a + ν • (fun x => x ^ n) b
obtain ⟨k, rfl⟩ := hn.exists_two_nsmul _
case intro
a b μ ν : ℝ
hμ : 0 ≤ μ
hν : 0 ≤ ν
h : μ + ν = 1
k : ℕ
hn : Even (2 • k)
this : 0 ≤ (a - b) ^ 2 * μ * ν
⊢ (fun x => x ^ (2 • k)) (μ • a + ν • b) ≤ μ • (fun x => x ^ (2 • k)) a + ν • (fun x => x ^ (2 • k)) b
case intro
a b μ ν : ℝ
hμ : 0 ≤ μ
hν : 0 ≤ ν
h : μ + ν = 1
k : ℕ
hn : Even (2 • k)
⊢ (fun x => x ^ (2 • k)) (μ • a + ν • b) ≤ μ • (fun x => x ^ (2 • k)) a + ν • (fun x => x ^ (2 • k)) b
have : (0 : ℝ) ≤ (a - b) ^ 2 * μ * ν := by positivity
case intro
a b μ ν : ℝ
hμ : 0 ≤ μ
hν : 0 ≤ ν
h : μ + ν = 1
k : ℕ
hn : Even (2 • k)
this : 0 ≤ (a - b) ^ 2 * μ * ν
⊢ (μ * a ^ 2 + ν * b ^ 2) ^ k ≤ μ * (a ^ 2) ^ k + ν * (b ^ 2) ^ k
case intro
a b μ ν : ℝ
hμ : 0 ≤ μ
hν : 0 ≤ ν
h : μ + ν = 1
k : ℕ
hn : Even (2 • k)
this : 0 ≤ (a - b) ^ 2 * μ * ν
⊢ (fun x => x ^ (2 • k)) (μ • a + ν • b) ≤ μ • (fun x => x ^ (2 • k)) a + ν • (fun x => x ^ (2 • k)) b
calc
  (μ * a + ν * b) ^ (2 * k) = ((μ * a + ν * b) ^ 2) ^ k := by rw [pow_mul]
  _ ≤ ((μ + ν) * (μ * a ^ 2 + ν * b ^ 2)) ^ k := by gcongr; linarith
  _ = (μ * a ^ 2 + ν * b ^ 2) ^ k := by rw [h]; ring
  _ ≤ μ * (a ^ 2) ^ k + ν * (b ^ 2) ^ k := ?_
  _ ≤ μ * a ^ (2 * k) + ν * b ^ (2 * k) := by ring_nf; rfl
no goals
case intro
a b μ ν : ℝ
hμ : 0 ≤ μ
hν : 0 ≤ ν
h : μ + ν = 1
k : ℕ
hn : Even (2 • k)
this : 0 ≤ (a - b) ^ 2 * μ * ν
⊢ (μ * a ^ 2 + ν * b ^ 2) ^ k ≤ μ * (a ^ 2) ^ k + ν * (b ^ 2) ^ k
refine' (convexOn_pow k).2 _ _ hμ hν h <;> rw [mem_Ici] <;> positivity
no goals
a b μ ν : ℝ
hμ : 0 ≤ μ
hν : 0 ≤ ν
h : μ + ν = 1
k : ℕ
hn : Even (2 • k)
⊢ 0 ≤ (a - b) ^ 2 * μ * ν
positivity
no goals
a b μ ν : ℝ
hμ : 0 ≤ μ
hν : 0 ≤ ν
h : μ + ν = 1
k : ℕ
hn : Even (2 • k)
this : 0 ≤ (a - b) ^ 2 * μ * ν
⊢ (μ * a + ν * b) ^ (2 * k) = ((μ * a + ν * b) ^ 2) ^ k
rw [pow_mul]
case hab
a b μ ν : ℝ
hμ : 0 ≤ μ
hν : 0 ≤ ν
h : μ + ν = 1
k : ℕ
hn : Even (2 • k)
this : 0 ≤ (a - b) ^ 2 * μ * ν
⊢ (μ * a + ν * b) ^ 2 ≤ (μ + ν) * (μ * a ^ 2 + ν * b ^ 2)
a b μ ν : ℝ
hμ : 0 ≤ μ
hν : 0 ≤ ν
h : μ + ν = 1
k : ℕ
hn : Even (2 • k)
this : 0 ≤ (a - b) ^ 2 * μ * ν
⊢ ((μ * a + ν * b) ^ 2) ^ k ≤ ((μ + ν) * (μ * a ^ 2 + ν * b ^ 2)) ^ k
gcongr
no goals
case hab
a b μ ν : ℝ
hμ : 0 ≤ μ
hν : 0 ≤ ν
h : μ + ν = 1
k : ℕ
hn : Even (2 • k)
this : 0 ≤ (a - b) ^ 2 * μ * ν
⊢ (μ * a + ν * b) ^ 2 ≤ (μ + ν) * (μ * a ^ 2 + ν * b ^ 2)
linarith
a b μ ν : ℝ
hμ : 0 ≤ μ
hν : 0 ≤ ν
h : μ + ν = 1
k : ℕ
hn : Even (2 • k)
this : 0 ≤ (a - b) ^ 2 * μ * ν
⊢ (1 * (μ * a ^ 2 + ν * b ^ 2)) ^ k = (μ * a ^ 2 + ν * b ^ 2) ^ k
a b μ ν : ℝ
hμ : 0 ≤ μ
hν : 0 ≤ ν
h : μ + ν = 1
k : ℕ
hn : Even (2 • k)
this : 0 ≤ (a - b) ^ 2 * μ * ν
⊢ ((μ + ν) * (μ * a ^ 2 + ν * b ^ 2)) ^ k = (μ * a ^ 2 + ν * b ^ 2) ^ k
rw [h]
no goals
a b μ ν : ℝ
hμ : 0 ≤ μ
hν : 0 ≤ ν
h : μ + ν = 1
k : ℕ
hn : Even (2 • k)
this : 0 ≤ (a - b) ^ 2 * μ * ν
⊢ (1 * (μ * a ^ 2 + ν * b ^ 2)) ^ k = (μ * a ^ 2 + ν * b ^ 2) ^ k
ring
a b μ ν : ℝ
hμ : 0 ≤ μ
hν : 0 ≤ ν
h : μ + ν = 1
k : ℕ
hn : Even (2 • k)
this : 0 ≤ (a - b) ^ 2 * μ * ν
⊢ μ * a ^ (k * 2) + ν * b ^ (k * 2) ≤ μ * a ^ (k * 2) + ν * b ^ (k * 2)
a b μ ν : ℝ
hμ : 0 ≤ μ
hν : 0 ≤ ν
h : μ + ν = 1
k : ℕ
hn : Even (2 • k)
this : 0 ≤ (a - b) ^ 2 * μ * ν
⊢ μ * (a ^ 2) ^ k + ν * (b ^ 2) ^ k ≤ μ * a ^ (2 * k) + ν * b ^ (2 * k)
ring_nf
no goals
a b μ ν : ℝ
hμ : 0 ≤ μ
hν : 0 ≤ ν
h : μ + ν = 1
k : ℕ
hn : Even (2 • k)
this : 0 ≤ (a - b) ^ 2 * μ * ν
⊢ μ * a ^ (k * 2) + ν * b ^ (k * 2) ≤ μ * a ^ (k * 2) + ν * b ^ (k * 2)
rfl