-- Mathlib/Analysis/Convex/Mul.lean
/-- `x^m`, `m : ℤ` is convex on `(0, +∞)` for all `m`. -/
lemma convexOn_zpow : ∀ n : ℤ, ConvexOn 𝕜 (Ioi 0) fun x : 𝕜 ↦ x ^ n
  | (n : ℕ) => by
    simp_rw [zpow_natCast]
    exact (convexOn_pow n).subset Ioi_subset_Ici_self (convex_Ioi _)
  | -[n+1] => by
    simp_rw [zpow_negSucc, ← inv_pow]
    refine (convexOn_iff_forall_pos.2 ⟨convex_Ioi _, ?_⟩).pow (fun x (hx : 0 < x) ↦ by positivity) _
    rintro x (hx : 0 < x) y (hy : 0 < y) a b ha hb hab
    field_simp
    rw [div_le_div_iff₀, ← sub_nonneg]
    · calc
        0 ≤ a * b * (x - y) ^ 2

Proof state:
𝕜 : Type u_1
inst✝ : LinearOrderedField 𝕜
n : ℕ
x : 𝕜
hx : 0 < x
y : 𝕜
hy : 0 < y
a b : 𝕜
ha : 0 < a
hb : 0 < b
hab : a + b = 1
⊢ 1 / (a * x + b * y) ≤ (a * y + b * x) / (x * y)

Tactic:
rw [div_le_div_iff₀, ← sub_nonneg]

Result:
𝕜 : Type u_1
inst✝ : LinearOrderedField 𝕜
n : ℕ
x : 𝕜
hx : 0 < x
y : 𝕜
hy : 0 < y
a b : 𝕜
ha : 0 < a
hb : 0 < b
hab : a + b = 1
⊢ 0 ≤ (a * y + b * x) * (a * x + b * y) - 1 * (x * y)

case hb
𝕜 : Type u_1
inst✝ : LinearOrderedField 𝕜
n : ℕ
x : 𝕜
hx : 0 < x
y : 𝕜
hy : 0 < y
a b : 𝕜
ha : 0 < a
hb : 0 < b
hab : a + b = 1
⊢ 0 < a * x + b * y

case hd
𝕜 : Type u_1
inst✝ : LinearOrderedField 𝕜
n : ℕ
x : 𝕜
hx : 0 < x
y : 𝕜
hy : 0 < y
a b : 𝕜
ha : 0 < a
hb : 0 < b
hab : a + b = 1
⊢ 0 < x * y

Proof state:
𝕜 : Type u_1
inst✝ : LinearOrderedField 𝕜
n : ℕ
x : 𝕜
hx : 0 < x
y : 𝕜
hy : 0 < y
a b : 𝕜
ha : 0 < a
hb : 0 < b
hab : a + b = 1
⊢ (a • x + b • y)⁻¹ ≤ a • x⁻¹ + b • y⁻¹

Tactic:
field_simp

Result:
𝕜 : Type u_1
inst✝ : LinearOrderedField 𝕜
n : ℕ
x : 𝕜
hx : 0 < x
y : 𝕜
hy : 0 < y
a b : 𝕜
ha : 0 < a
hb : 0 < b
hab : a + b = 1
⊢ 1 / (a * x + b * y) ≤ (a * y + b * x) / (x * y)

Proof state:
𝕜 : Type u_1
inst✝ : LinearOrderedField 𝕜
n : ℕ
⊢ ConvexOn 𝕜 (Ioi 0) fun x => x ^ -[n+1]

Tactic:
simp_rw [zpow_negSucc, ← inv_pow]

Result:
𝕜 : Type u_1
inst✝ : LinearOrderedField 𝕜
n : ℕ
⊢ ConvexOn 𝕜 (Ioi 0) fun x => x⁻¹ ^ (n + 1)

Proof state:
𝕜 : Type u_1
inst✝ : LinearOrderedField 𝕜
n : ℕ
x : 𝕜
hx : 0 < x
y : 𝕜
hy : 0 < y
b : 𝕜
hb : 0 < b
ha : 0 < 1 - b
hab : 1 - b + b = 1
⊢ (1 - b) * b * (x - y) ^ 2 = ((1 - b) * y + b * x) * ((1 - b) * x + b * y) - 1 * (x * y)

Tactic:
ring

Result:
no goals

Proof state:
𝕜 : Type u_1
inst✝ : LinearOrderedField 𝕜
n : ℕ
⊢ ConvexOn 𝕜 (Ioi 0) fun x => x ^ ↑n

Tactic:
simp_rw [zpow_natCast]

Result:
𝕜 : Type u_1
inst✝ : LinearOrderedField 𝕜
n : ℕ
⊢ ConvexOn 𝕜 (Ioi 0) fun x => x ^ n

Proof state:
𝕜 : Type u_1
inst✝ : LinearOrderedField 𝕜
n : ℕ
x : 𝕜
hx : 0 < x
y : 𝕜
hy : 0 < y
a b : 𝕜
ha : 0 < a
hb : 0 < b
hab : a + b = 1
⊢ 0 ≤ (a * y + b * x) * (a * x + b * y) - 1 * (x * y)

Tactic:
calc
  0 ≤ a * b * (x - y) ^ 2 := by positivity
  _ = _ := by obtain rfl := eq_sub_of_add_eq hab; ring

Result:
no goals

Proof state:
𝕜 : Type u_1
inst✝ : LinearOrderedField 𝕜
n : ℕ
⊢ ∀ ⦃x : 𝕜⦄,
    x ∈ Ioi 0 → ∀ ⦃y : 𝕜⦄, y ∈ Ioi 0 → ∀ ⦃a b : 𝕜⦄, 0 < a → 0 < b → a + b = 1 → (a • x + b • y)⁻¹ ≤ a • x⁻¹ + b • y⁻¹

Tactic:
rintro x (hx : 0 < x) y (hy : 0 < y) a b ha hb hab

Result:
𝕜 : Type u_1
inst✝ : LinearOrderedField 𝕜
n : ℕ
x : 𝕜
hx : 0 < x
y : 𝕜
hy : 0 < y
a b : 𝕜
ha : 0 < a
hb : 0 < b
hab : a + b = 1
⊢ (a • x + b • y)⁻¹ ≤ a • x⁻¹ + b • y⁻¹

Proof state:
case hb
𝕜 : Type u_1
inst✝ : LinearOrderedField 𝕜
n : ℕ
x : 𝕜
hx : 0 < x
y : 𝕜
hy : 0 < y
a b : 𝕜
ha : 0 < a
hb : 0 < b
hab : a + b = 1
⊢ 0 < a * x + b * y

case hd
𝕜 : Type u_1
inst✝ : LinearOrderedField 𝕜
n : ℕ
x : 𝕜
hx : 0 < x
y : 𝕜
hy : 0 < y
a b : 𝕜
ha : 0 < a
hb : 0 < b
hab : a + b = 1
⊢ 0 < x * y

Tactic:
all_goals positivity

Result:
no goals

Proof state:
𝕜 : Type u_1
inst✝ : LinearOrderedField 𝕜
n : ℕ
⊢ ConvexOn 𝕜 (Ioi 0) fun x => x ^ n

Tactic:
exact (convexOn_pow n).subset Ioi_subset_Ici_self (convex_Ioi _)

Result:
no goals

Proof state:
𝕜 : Type u_1
inst✝ : LinearOrderedField 𝕜
n : ℕ
x : 𝕜
hx : 0 < x
y : 𝕜
hy : 0 < y
a b : 𝕜
ha : 0 < a
hb : 0 < b
hab : a + b = 1
⊢ a * b * (x - y) ^ 2 = (a * y + b * x) * (a * x + b * y) - 1 * (x * y)

Tactic:
obtain rfl := eq_sub_of_add_eq hab

Result:
𝕜 : Type u_1
inst✝ : LinearOrderedField 𝕜
n : ℕ
x : 𝕜
hx : 0 < x
y : 𝕜
hy : 0 < y
b : 𝕜
hb : 0 < b
ha : 0 < 1 - b
hab : 1 - b + b = 1
⊢ (1 - b) * b * (x - y) ^ 2 = ((1 - b) * y + b * x) * ((1 - b) * x + b * y) - 1 * (x * y)

Proof state:
𝕜 : Type u_1
inst✝ : LinearOrderedField 𝕜
n : ℕ
x : 𝕜
hx : 0 < x
y : 𝕜
hy : 0 < y
a b : 𝕜
ha : 0 < a
hb : 0 < b
hab : a + b = 1
⊢ 0 ≤ a * b * (x - y) ^ 2

Tactic:
positivity

Result:
no goals

Proof state:
𝕜 : Type u_1
inst✝ : LinearOrderedField 𝕜
n : ℕ
x : 𝕜
hx : 0 < x
⊢ 0 ≤ x⁻¹

Tactic:
positivity

Result:
no goals

Proof state:
case hd
𝕜 : Type u_1
inst✝ : LinearOrderedField 𝕜
n : ℕ
x : 𝕜
hx : 0 < x
y : 𝕜
hy : 0 < y
a b : 𝕜
ha : 0 < a
hb : 0 < b
hab : a + b = 1
⊢ 0 < x * y

Tactic:
positivity

Result:
no goals

Proof state:
𝕜 : Type u_1
inst✝ : LinearOrderedField 𝕜
n : ℕ
⊢ ConvexOn 𝕜 (Ioi 0) fun x => x⁻¹ ^ (n + 1)

Tactic:
refine (convexOn_iff_forall_pos.2 ⟨convex_Ioi _, ?_⟩).pow (fun x (hx : 0 < x) ↦ by positivity) _

Result:
𝕜 : Type u_1
inst✝ : LinearOrderedField 𝕜
n : ℕ
⊢ ∀ ⦃x : 𝕜⦄,
    x ∈ Ioi 0 → ∀ ⦃y : 𝕜⦄, y ∈ Ioi 0 → ∀ ⦃a b : 𝕜⦄, 0 < a → 0 < b → a + b = 1 → (a • x + b • y)⁻¹ ≤ a • x⁻¹ + b • y⁻¹