case zero

⊢ ConvexOn ℝ (Ici 0) fun x => x ^ Nat.zero

case succ
k : ℕ
IH : ConvexOn ℝ (Ici 0) fun x => x ^ k
⊢ ConvexOn ℝ (Ici 0) fun x => x ^ Nat.succ k
n : ℕ
⊢ ConvexOn ℝ (Ici 0) fun x => x ^ n
induction' n with k IH
case succ
k : ℕ
IH : ConvexOn ℝ (Ici 0) fun x => x ^ k
⊢ ∀ ⦃x : ℝ⦄,
    x ∈ Ici 0 →
      ∀ ⦃y : ℝ⦄,
        y ∈ Ici 0 →
          ∀ ⦃a b : ℝ⦄,
            0 ≤ a →
              0 ≤ b →
                a + b = 1 →
                  (fun x => x ^ Nat.succ k) (a • x + b • y) ≤
                    a • (fun x => x ^ Nat.succ k) x + b • (fun x => x ^ Nat.succ k) y
case succ
k : ℕ
IH : ConvexOn ℝ (Ici 0) fun x => x ^ k
⊢ ConvexOn ℝ (Ici 0) fun x => x ^ Nat.succ k
refine' ⟨convex_Ici _, _⟩
case succ
k : ℕ
IH : ConvexOn ℝ (Ici 0) fun x => x ^ k
a : ℝ
ha : 0 ≤ a
b : ℝ
hb : 0 ≤ b
μ ν : ℝ
hμ : 0 ≤ μ
hν : 0 ≤ ν
h : μ + ν = 1
⊢ (fun x => x ^ Nat.succ k) (μ • a + ν • b) ≤ μ • (fun x => x ^ Nat.succ k) a + ν • (fun x => x ^ Nat.succ k) b
case succ
k : ℕ
IH : ConvexOn ℝ (Ici 0) fun x => x ^ k
⊢ ∀ ⦃x : ℝ⦄,
    x ∈ Ici 0 →
      ∀ ⦃y : ℝ⦄,
        y ∈ Ici 0 →
          ∀ ⦃a b : ℝ⦄,
            0 ≤ a →
              0 ≤ b →
                a + b = 1 →
                  (fun x => x ^ Nat.succ k) (a • x + b • y) ≤
                    a • (fun x => x ^ Nat.succ k) x + b • (fun x => x ^ Nat.succ k) y
rintro a (ha : 0 ≤ a) b (hb : 0 ≤ b) μ ν hμ hν h
case succ
k : ℕ
IH : ConvexOn ℝ (Ici 0) fun x => x ^ k
a : ℝ
ha : 0 ≤ a
b : ℝ
hb : 0 ≤ b
μ ν : ℝ
hμ : 0 ≤ μ
hν : 0 ≤ ν
h : μ + ν = 1
H : (fun x => x ^ k) (μ • a + ν • b) ≤ μ • (fun x => x ^ k) a + ν • (fun x => x ^ k) b
⊢ (fun x => x ^ Nat.succ k) (μ • a + ν • b) ≤ μ • (fun x => x ^ Nat.succ k) a + ν • (fun x => x ^ Nat.succ k) b
case succ
k : ℕ
IH : ConvexOn ℝ (Ici 0) fun x => x ^ k
a : ℝ
ha : 0 ≤ a
b : ℝ
hb : 0 ≤ b
μ ν : ℝ
hμ : 0 ≤ μ
hν : 0 ≤ ν
h : μ + ν = 1
⊢ (fun x => x ^ Nat.succ k) (μ • a + ν • b) ≤ μ • (fun x => x ^ Nat.succ k) a + ν • (fun x => x ^ Nat.succ k) b
have H := IH.2 ha hb hμ hν h
no goals
case succ
k : ℕ
IH : ConvexOn ℝ (Ici 0) fun x => x ^ k
a : ℝ
ha : 0 ≤ a
b : ℝ
hb : 0 ≤ b
μ ν : ℝ
hμ : 0 ≤ μ
hν : 0 ≤ ν
h : μ + ν = 1
H : (fun x => x ^ k) (μ • a + ν • b) ≤ μ • (fun x => x ^ k) a + ν • (fun x => x ^ k) b
this : 0 ≤ (b ^ k - a ^ k) * (b - a) * μ * ν
⊢ (fun x => x ^ Nat.succ k) (μ • a + ν • b) ≤ μ • (fun x => x ^ Nat.succ k) a + ν • (fun x => x ^ Nat.succ k) b
calc
  (μ * a + ν * b) ^ k.succ = (μ * a + ν * b) * (μ * a + ν * b) ^ k := pow_succ _ _
  _ ≤ (μ * a + ν * b) * (μ * a ^ k + ν * b ^ k) := by gcongr; exact H
  _ ≤ (μ * a + ν * b) * (μ * a ^ k + ν * b ^ k) + (b ^ k - a ^ k) * (b - a) * μ * ν := by linarith
  _ = (μ + ν) * (μ * a ^ k.succ + ν * b ^ k.succ) := by rw [Nat.succ_eq_add_one]; ring
  _ = μ * a ^ k.succ + ν * b ^ k.succ := by rw [h]; ring
no goals
case zero

⊢ ConvexOn ℝ (Ici 0) fun x => x ^ Nat.zero
exact convexOn_const (1 : ℝ) (convex_Ici _)
case inl
k : ℕ
IH : ConvexOn ℝ (Ici 0) fun x => x ^ k
a : ℝ
ha : 0 ≤ a
b : ℝ
hb : 0 ≤ b
μ ν : ℝ
hμ : 0 ≤ μ
hν : 0 ≤ ν
h : μ + ν = 1
H : (fun x => x ^ k) (μ • a + ν • b) ≤ μ • (fun x => x ^ k) a + ν • (fun x => x ^ k) b
hab : a ≤ b
⊢ 0 ≤ (b ^ k - a ^ k) * (b - a) * μ * ν

case inr
k : ℕ
IH : ConvexOn ℝ (Ici 0) fun x => x ^ k
a : ℝ
ha : 0 ≤ a
b : ℝ
hb : 0 ≤ b
μ ν : ℝ
hμ : 0 ≤ μ
hν : 0 ≤ ν
h : μ + ν = 1
H : (fun x => x ^ k) (μ • a + ν • b) ≤ μ • (fun x => x ^ k) a + ν • (fun x => x ^ k) b
hab : b < a
⊢ 0 ≤ (b ^ k - a ^ k) * (b - a) * μ * ν
k : ℕ
IH : ConvexOn ℝ (Ici 0) fun x => x ^ k
a : ℝ
ha : 0 ≤ a
b : ℝ
hb : 0 ≤ b
μ ν : ℝ
hμ : 0 ≤ μ
hν : 0 ≤ ν
h : μ + ν = 1
H : (fun x => x ^ k) (μ • a + ν • b) ≤ μ • (fun x => x ^ k) a + ν • (fun x => x ^ k) b
⊢ 0 ≤ (b ^ k - a ^ k) * (b - a) * μ * ν
cases' le_or_lt a b with hab hab
case inl
k : ℕ
IH : ConvexOn ℝ (Ici 0) fun x => x ^ k
a : ℝ
ha : 0 ≤ a
b : ℝ
hb : 0 ≤ b
μ ν : ℝ
hμ : 0 ≤ μ
hν : 0 ≤ ν
h : μ + ν = 1
H : (fun x => x ^ k) (μ • a + ν • b) ≤ μ • (fun x => x ^ k) a + ν • (fun x => x ^ k) b
hab : a ≤ b
this : a ^ k ≤ b ^ k
⊢ 0 ≤ (b ^ k - a ^ k) * (b - a) * μ * ν
case inl
k : ℕ
IH : ConvexOn ℝ (Ici 0) fun x => x ^ k
a : ℝ
ha : 0 ≤ a
b : ℝ
hb : 0 ≤ b
μ ν : ℝ
hμ : 0 ≤ μ
hν : 0 ≤ ν
h : μ + ν = 1
H : (fun x => x ^ k) (μ • a + ν • b) ≤ μ • (fun x => x ^ k) a + ν • (fun x => x ^ k) b
hab : a ≤ b
⊢ 0 ≤ (b ^ k - a ^ k) * (b - a) * μ * ν
have : a ^ k ≤ b ^ k := by gcongr
case inl
k : ℕ
IH : ConvexOn ℝ (Ici 0) fun x => x ^ k
a : ℝ
ha : 0 ≤ a
b : ℝ
hb : 0 ≤ b
μ ν : ℝ
hμ : 0 ≤ μ
hν : 0 ≤ ν
h : μ + ν = 1
H : (fun x => x ^ k) (μ • a + ν • b) ≤ μ • (fun x => x ^ k) a + ν • (fun x => x ^ k) b
hab : a ≤ b
this✝ : a ^ k ≤ b ^ k
this : 0 ≤ (b ^ k - a ^ k) * (b - a)
⊢ 0 ≤ (b ^ k - a ^ k) * (b - a) * μ * ν
case inl
k : ℕ
IH : ConvexOn ℝ (Ici 0) fun x => x ^ k
a : ℝ
ha : 0 ≤ a
b : ℝ
hb : 0 ≤ b
μ ν : ℝ
hμ : 0 ≤ μ
hν : 0 ≤ ν
h : μ + ν = 1
H : (fun x => x ^ k) (μ • a + ν • b) ≤ μ • (fun x => x ^ k) a + ν • (fun x => x ^ k) b
hab : a ≤ b
this : a ^ k ≤ b ^ k
⊢ 0 ≤ (b ^ k - a ^ k) * (b - a) * μ * ν
have : 0 ≤ (b ^ k - a ^ k) * (b - a) := by nlinarith
no goals
case inl
k : ℕ
IH : ConvexOn ℝ (Ici 0) fun x => x ^ k
a : ℝ
ha : 0 ≤ a
b : ℝ
hb : 0 ≤ b
μ ν : ℝ
hμ : 0 ≤ μ
hν : 0 ≤ ν
h : μ + ν = 1
H : (fun x => x ^ k) (μ • a + ν • b) ≤ μ • (fun x => x ^ k) a + ν • (fun x => x ^ k) b
hab : a ≤ b
this✝ : a ^ k ≤ b ^ k
this : 0 ≤ (b ^ k - a ^ k) * (b - a)
⊢ 0 ≤ (b ^ k - a ^ k) * (b - a) * μ * ν
positivity
no goals
k : ℕ
IH : ConvexOn ℝ (Ici 0) fun x => x ^ k
a : ℝ
ha : 0 ≤ a
b : ℝ
hb : 0 ≤ b
μ ν : ℝ
hμ : 0 ≤ μ
hν : 0 ≤ ν
h : μ + ν = 1
H : (fun x => x ^ k) (μ • a + ν • b) ≤ μ • (fun x => x ^ k) a + ν • (fun x => x ^ k) b
hab : a ≤ b
⊢ a ^ k ≤ b ^ k
gcongr
no goals
k : ℕ
IH : ConvexOn ℝ (Ici 0) fun x => x ^ k
a : ℝ
ha : 0 ≤ a
b : ℝ
hb : 0 ≤ b
μ ν : ℝ
hμ : 0 ≤ μ
hν : 0 ≤ ν
h : μ + ν = 1
H : (fun x => x ^ k) (μ • a + ν • b) ≤ μ • (fun x => x ^ k) a + ν • (fun x => x ^ k) b
hab : a ≤ b
this : a ^ k ≤ b ^ k
⊢ 0 ≤ (b ^ k - a ^ k) * (b - a)
nlinarith
case inr
k : ℕ
IH : ConvexOn ℝ (Ici 0) fun x => x ^ k
a : ℝ
ha : 0 ≤ a
b : ℝ
hb : 0 ≤ b
μ ν : ℝ
hμ : 0 ≤ μ
hν : 0 ≤ ν
h : μ + ν = 1
H : (fun x => x ^ k) (μ • a + ν • b) ≤ μ • (fun x => x ^ k) a + ν • (fun x => x ^ k) b
hab : b < a
this : b ^ k ≤ a ^ k
⊢ 0 ≤ (b ^ k - a ^ k) * (b - a) * μ * ν
case inr
k : ℕ
IH : ConvexOn ℝ (Ici 0) fun x => x ^ k
a : ℝ
ha : 0 ≤ a
b : ℝ
hb : 0 ≤ b
μ ν : ℝ
hμ : 0 ≤ μ
hν : 0 ≤ ν
h : μ + ν = 1
H : (fun x => x ^ k) (μ • a + ν • b) ≤ μ • (fun x => x ^ k) a + ν • (fun x => x ^ k) b
hab : b < a
⊢ 0 ≤ (b ^ k - a ^ k) * (b - a) * μ * ν
have : b ^ k ≤ a ^ k := by gcongr
case inr
k : ℕ
IH : ConvexOn ℝ (Ici 0) fun x => x ^ k
a : ℝ
ha : 0 ≤ a
b : ℝ
hb : 0 ≤ b
μ ν : ℝ
hμ : 0 ≤ μ
hν : 0 ≤ ν
h : μ + ν = 1
H : (fun x => x ^ k) (μ • a + ν • b) ≤ μ • (fun x => x ^ k) a + ν • (fun x => x ^ k) b
hab : b < a
this✝ : b ^ k ≤ a ^ k
this : 0 ≤ (b ^ k - a ^ k) * (b - a)
⊢ 0 ≤ (b ^ k - a ^ k) * (b - a) * μ * ν
case inr
k : ℕ
IH : ConvexOn ℝ (Ici 0) fun x => x ^ k
a : ℝ
ha : 0 ≤ a
b : ℝ
hb : 0 ≤ b
μ ν : ℝ
hμ : 0 ≤ μ
hν : 0 ≤ ν
h : μ + ν = 1
H : (fun x => x ^ k) (μ • a + ν • b) ≤ μ • (fun x => x ^ k) a + ν • (fun x => x ^ k) b
hab : b < a
this : b ^ k ≤ a ^ k
⊢ 0 ≤ (b ^ k - a ^ k) * (b - a) * μ * ν
have : 0 ≤ (b ^ k - a ^ k) * (b - a) := by nlinarith
no goals
case inr
k : ℕ
IH : ConvexOn ℝ (Ici 0) fun x => x ^ k
a : ℝ
ha : 0 ≤ a
b : ℝ
hb : 0 ≤ b
μ ν : ℝ
hμ : 0 ≤ μ
hν : 0 ≤ ν
h : μ + ν = 1
H : (fun x => x ^ k) (μ • a + ν • b) ≤ μ • (fun x => x ^ k) a + ν • (fun x => x ^ k) b
hab : b < a
this✝ : b ^ k ≤ a ^ k
this : 0 ≤ (b ^ k - a ^ k) * (b - a)
⊢ 0 ≤ (b ^ k - a ^ k) * (b - a) * μ * ν
positivity
no goals
k : ℕ
IH : ConvexOn ℝ (Ici 0) fun x => x ^ k
a : ℝ
ha : 0 ≤ a
b : ℝ
hb : 0 ≤ b
μ ν : ℝ
hμ : 0 ≤ μ
hν : 0 ≤ ν
h : μ + ν = 1
H : (fun x => x ^ k) (μ • a + ν • b) ≤ μ • (fun x => x ^ k) a + ν • (fun x => x ^ k) b
hab : b < a
⊢ b ^ k ≤ a ^ k
gcongr
no goals
k : ℕ
IH : ConvexOn ℝ (Ici 0) fun x => x ^ k
a : ℝ
ha : 0 ≤ a
b : ℝ
hb : 0 ≤ b
μ ν : ℝ
hμ : 0 ≤ μ
hν : 0 ≤ ν
h : μ + ν = 1
H : (fun x => x ^ k) (μ • a + ν • b) ≤ μ • (fun x => x ^ k) a + ν • (fun x => x ^ k) b
hab : b < a
this : b ^ k ≤ a ^ k
⊢ 0 ≤ (b ^ k - a ^ k) * (b - a)
nlinarith
case h
k : ℕ
IH : ConvexOn ℝ (Ici 0) fun x => x ^ k
a : ℝ
ha : 0 ≤ a
b : ℝ
hb : 0 ≤ b
μ ν : ℝ
hμ : 0 ≤ μ
hν : 0 ≤ ν
h : μ + ν = 1
H : (fun x => x ^ k) (μ • a + ν • b) ≤ μ • (fun x => x ^ k) a + ν • (fun x => x ^ k) b
this : 0 ≤ (b ^ k - a ^ k) * (b - a) * μ * ν
⊢ (μ * a + ν * b) ^ k ≤ μ * a ^ k + ν * b ^ k
k : ℕ
IH : ConvexOn ℝ (Ici 0) fun x => x ^ k
a : ℝ
ha : 0 ≤ a
b : ℝ
hb : 0 ≤ b
μ ν : ℝ
hμ : 0 ≤ μ
hν : 0 ≤ ν
h : μ + ν = 1
H : (fun x => x ^ k) (μ • a + ν • b) ≤ μ • (fun x => x ^ k) a + ν • (fun x => x ^ k) b
this : 0 ≤ (b ^ k - a ^ k) * (b - a) * μ * ν
⊢ (μ * a + ν * b) * (μ * a + ν * b) ^ k ≤ (μ * a + ν * b) * (μ * a ^ k + ν * b ^ k)
gcongr
no goals
case h
k : ℕ
IH : ConvexOn ℝ (Ici 0) fun x => x ^ k
a : ℝ
ha : 0 ≤ a
b : ℝ
hb : 0 ≤ b
μ ν : ℝ
hμ : 0 ≤ μ
hν : 0 ≤ ν
h : μ + ν = 1
H : (fun x => x ^ k) (μ • a + ν • b) ≤ μ • (fun x => x ^ k) a + ν • (fun x => x ^ k) b
this : 0 ≤ (b ^ k - a ^ k) * (b - a) * μ * ν
⊢ (μ * a + ν * b) ^ k ≤ μ * a ^ k + ν * b ^ k
exact H
no goals
k : ℕ
IH : ConvexOn ℝ (Ici 0) fun x => x ^ k
a : ℝ
ha : 0 ≤ a
b : ℝ
hb : 0 ≤ b
μ ν : ℝ
hμ : 0 ≤ μ
hν : 0 ≤ ν
h : μ + ν = 1
H : (fun x => x ^ k) (μ • a + ν • b) ≤ μ • (fun x => x ^ k) a + ν • (fun x => x ^ k) b
this : 0 ≤ (b ^ k - a ^ k) * (b - a) * μ * ν
⊢ (μ * a + ν * b) * (μ * a ^ k + ν * b ^ k) ≤
    (μ * a + ν * b) * (μ * a ^ k + ν * b ^ k) + (b ^ k - a ^ k) * (b - a) * μ * ν
linarith
k : ℕ
IH : ConvexOn ℝ (Ici 0) fun x => x ^ k
a : ℝ
ha : 0 ≤ a
b : ℝ
hb : 0 ≤ b
μ ν : ℝ
hμ : 0 ≤ μ
hν : 0 ≤ ν
h : μ + ν = 1
H : (fun x => x ^ k) (μ • a + ν • b) ≤ μ • (fun x => x ^ k) a + ν • (fun x => x ^ k) b
this : 0 ≤ (b ^ k - a ^ k) * (b - a) * μ * ν
⊢ (μ * a + ν * b) * (μ * a ^ k + ν * b ^ k) + (b ^ k - a ^ k) * (b - a) * μ * ν =
    (μ + ν) * (μ * a ^ (k + 1) + ν * b ^ (k + 1))
k : ℕ
IH : ConvexOn ℝ (Ici 0) fun x => x ^ k
a : ℝ
ha : 0 ≤ a
b : ℝ
hb : 0 ≤ b
μ ν : ℝ
hμ : 0 ≤ μ
hν : 0 ≤ ν
h : μ + ν = 1
H : (fun x => x ^ k) (μ • a + ν • b) ≤ μ • (fun x => x ^ k) a + ν • (fun x => x ^ k) b
this : 0 ≤ (b ^ k - a ^ k) * (b - a) * μ * ν
⊢ (μ * a + ν * b) * (μ * a ^ k + ν * b ^ k) + (b ^ k - a ^ k) * (b - a) * μ * ν =
    (μ + ν) * (μ * a ^ Nat.succ k + ν * b ^ Nat.succ k)
rw [Nat.succ_eq_add_one]
no goals
k : ℕ
IH : ConvexOn ℝ (Ici 0) fun x => x ^ k
a : ℝ
ha : 0 ≤ a
b : ℝ
hb : 0 ≤ b
μ ν : ℝ
hμ : 0 ≤ μ
hν : 0 ≤ ν
h : μ + ν = 1
H : (fun x => x ^ k) (μ • a + ν • b) ≤ μ • (fun x => x ^ k) a + ν • (fun x => x ^ k) b
this : 0 ≤ (b ^ k - a ^ k) * (b - a) * μ * ν
⊢ (μ * a + ν * b) * (μ * a ^ k + ν * b ^ k) + (b ^ k - a ^ k) * (b - a) * μ * ν =
    (μ + ν) * (μ * a ^ (k + 1) + ν * b ^ (k + 1))
ring
k : ℕ
IH : ConvexOn ℝ (Ici 0) fun x => x ^ k
a : ℝ
ha : 0 ≤ a
b : ℝ
hb : 0 ≤ b
μ ν : ℝ
hμ : 0 ≤ μ
hν : 0 ≤ ν
h : μ + ν = 1
H : (fun x => x ^ k) (μ • a + ν • b) ≤ μ • (fun x => x ^ k) a + ν • (fun x => x ^ k) b
this : 0 ≤ (b ^ k - a ^ k) * (b - a) * μ * ν
⊢ 1 * (μ * a ^ Nat.succ k + ν * b ^ Nat.succ k) = μ * a ^ Nat.succ k + ν * b ^ Nat.succ k
k : ℕ
IH : ConvexOn ℝ (Ici 0) fun x => x ^ k
a : ℝ
ha : 0 ≤ a
b : ℝ
hb : 0 ≤ b
μ ν : ℝ
hμ : 0 ≤ μ
hν : 0 ≤ ν
h : μ + ν = 1
H : (fun x => x ^ k) (μ • a + ν • b) ≤ μ • (fun x => x ^ k) a + ν • (fun x => x ^ k) b
this : 0 ≤ (b ^ k - a ^ k) * (b - a) * μ * ν
⊢ (μ + ν) * (μ * a ^ Nat.succ k + ν * b ^ Nat.succ k) = μ * a ^ Nat.succ k + ν * b ^ Nat.succ k
rw [h]
no goals
k : ℕ
IH : ConvexOn ℝ (Ici 0) fun x => x ^ k
a : ℝ
ha : 0 ≤ a
b : ℝ
hb : 0 ≤ b
μ ν : ℝ
hμ : 0 ≤ μ
hν : 0 ≤ ν
h : μ + ν = 1
H : (fun x => x ^ k) (μ • a + ν • b) ≤ μ • (fun x => x ^ k) a + ν • (fun x => x ^ k) b
this : 0 ≤ (b ^ k - a ^ k) * (b - a) * μ * ν
⊢ 1 * (μ * a ^ Nat.succ k + ν * b ^ Nat.succ k) = μ * a ^ Nat.succ k + ν * b ^ Nat.succ k
ring