[GOAL]
p : ℝ
hp₀ : 0 < p
hp₁ : p < 1
⊢ StrictConcaveOn ℝ≥0 univ fun x => x ^ p
[PROOFSTEP]
have hp₀' : 0 < 1 / p := by positivity
[GOAL]
p : ℝ
hp₀ : 0 < p
hp₁ : p < 1
⊢ 0 < 1 / p
[PROOFSTEP]
positivity
[GOAL]
p : ℝ
hp₀ : 0 < p
hp₁ : p < 1
hp₀' : 0 < 1 / p
⊢ StrictConcaveOn ℝ≥0 univ fun x => x ^ p
[PROOFSTEP]
have hp₁' : 1 < 1 / p := by rw [one_lt_div hp₀]; exact hp₁
[GOAL]
p : ℝ
hp₀ : 0 < p
hp₁ : p < 1
hp₀' : 0 < 1 / p
⊢ 1 < 1 / p
[PROOFSTEP]
rw [one_lt_div hp₀]
[GOAL]
p : ℝ
hp₀ : 0 < p
hp₁ : p < 1
hp₀' : 0 < 1 / p
⊢ p < 1
[PROOFSTEP]
exact hp₁
[GOAL]
p : ℝ
hp₀ : 0 < p
hp₁ : p < 1
hp₀' : 0 < 1 / p
hp₁' : 1 < 1 / p
⊢ StrictConcaveOn ℝ≥0 univ fun x => x ^ p
[PROOFSTEP]
let f := NNReal.orderIsoRpow (1 / p) hp₀'
[GOAL]
p : ℝ
hp₀ : 0 < p
hp₁ : p < 1
hp₀' : 0 < 1 / p
hp₁' : 1 < 1 / p
f : ℝ≥0 ≃o ℝ≥0 := orderIsoRpow (1 / p) hp₀'
⊢ StrictConcaveOn ℝ≥0 univ fun x => x ^ p
[PROOFSTEP]
have h₁ : StrictConvexOn ℝ≥0 univ f :=
  by
  refine ⟨convex_univ, fun x _ y _ hxy a b ha hb hab => ?_⟩
  exact
    (strictConvexOn_rpow hp₁').2 (by positivity : 0 ≤ x) (by positivity : 0 ≤ y) (by simp [hxy]) ha hb
      (by simp; norm_cast)
[GOAL]
p : ℝ
hp₀ : 0 < p
hp₁ : p < 1
hp₀' : 0 < 1 / p
hp₁' : 1 < 1 / p
f : ℝ≥0 ≃o ℝ≥0 := orderIsoRpow (1 / p) hp₀'
⊢ StrictConvexOn ℝ≥0 univ ↑f
[PROOFSTEP]
refine ⟨convex_univ, fun x _ y _ hxy a b ha hb hab => ?_⟩
[GOAL]
p : ℝ
hp₀ : 0 < p
hp₁ : p < 1
hp₀' : 0 < 1 / p
hp₁' : 1 < 1 / p
f : ℝ≥0 ≃o ℝ≥0 := orderIsoRpow (1 / p) hp₀'
x : ℝ≥0
x✝¹ : x ∈ univ
y : ℝ≥0
x✝ : y ∈ univ
hxy : x ≠ y
a b : ℝ≥0
ha : 0 < a
hb : 0 < b
hab : a + b = 1
⊢ ↑f (a • x + b • y) < a • ↑f x + b • ↑f y
[PROOFSTEP]
exact
  (strictConvexOn_rpow hp₁').2 (by positivity : 0 ≤ x) (by positivity : 0 ≤ y) (by simp [hxy]) ha hb
    (by simp; norm_cast)
[GOAL]
p : ℝ
hp₀ : 0 < p
hp₁ : p < 1
hp₀' : 0 < 1 / p
hp₁' : 1 < 1 / p
f : ℝ≥0 ≃o ℝ≥0 := orderIsoRpow (1 / p) hp₀'
x : ℝ≥0
x✝¹ : x ∈ univ
y : ℝ≥0
x✝ : y ∈ univ
hxy : x ≠ y
a b : ℝ≥0
ha : 0 < a
hb : 0 < b
hab : a + b = 1
⊢ 0 ≤ x
[PROOFSTEP]
positivity
[GOAL]
p : ℝ
hp₀ : 0 < p
hp₁ : p < 1
hp₀' : 0 < 1 / p
hp₁' : 1 < 1 / p
f : ℝ≥0 ≃o ℝ≥0 := orderIsoRpow (1 / p) hp₀'
x : ℝ≥0
x✝¹ : x ∈ univ
y : ℝ≥0
x✝ : y ∈ univ
hxy : x ≠ y
a b : ℝ≥0
ha : 0 < a
hb : 0 < b
hab : a + b = 1
⊢ 0 ≤ y
[PROOFSTEP]
positivity
[GOAL]
p : ℝ
hp₀ : 0 < p
hp₁ : p < 1
hp₀' : 0 < 1 / p
hp₁' : 1 < 1 / p
f : ℝ≥0 ≃o ℝ≥0 := orderIsoRpow (1 / p) hp₀'
x : ℝ≥0
x✝¹ : x ∈ univ
y : ℝ≥0
x✝ : y ∈ univ
hxy : x ≠ y
a b : ℝ≥0
ha : 0 < a
hb : 0 < b
hab : a + b = 1
⊢ (fun a => ↑a) x ≠ (fun a => ↑a) y
[PROOFSTEP]
simp [hxy]
[GOAL]
p : ℝ
hp₀ : 0 < p
hp₁ : p < 1
hp₀' : 0 < 1 / p
hp₁' : 1 < 1 / p
f : ℝ≥0 ≃o ℝ≥0 := orderIsoRpow (1 / p) hp₀'
x : ℝ≥0
x✝¹ : x ∈ univ
y : ℝ≥0
x✝ : y ∈ univ
hxy : x ≠ y
a b : ℝ≥0
ha : 0 < a
hb : 0 < b
hab : a + b = 1
⊢ ↑(↑(RingHom.id ℝ≥0) a) + ↑(↑(RingHom.id ℝ≥0) b) = 1
[PROOFSTEP]
simp
[GOAL]
p : ℝ
hp₀ : 0 < p
hp₁ : p < 1
hp₀' : 0 < 1 / p
hp₁' : 1 < 1 / p
f : ℝ≥0 ≃o ℝ≥0 := orderIsoRpow (1 / p) hp₀'
x : ℝ≥0
x✝¹ : x ∈ univ
y : ℝ≥0
x✝ : y ∈ univ
hxy : x ≠ y
a b : ℝ≥0
ha : 0 < a
hb : 0 < b
hab : a + b = 1
⊢ ↑a + ↑b = 1
[PROOFSTEP]
norm_cast
[GOAL]
p : ℝ
hp₀ : 0 < p
hp₁ : p < 1
hp₀' : 0 < 1 / p
hp₁' : 1 < 1 / p
f : ℝ≥0 ≃o ℝ≥0 := orderIsoRpow (1 / p) hp₀'
h₁ : StrictConvexOn ℝ≥0 univ ↑f
⊢ StrictConcaveOn ℝ≥0 univ fun x => x ^ p
[PROOFSTEP]
have h₂ : ∀ x, f.symm x = x ^ p := by simp [NNReal.orderIsoRpow_symm_eq]
[GOAL]
p : ℝ
hp₀ : 0 < p
hp₁ : p < 1
hp₀' : 0 < 1 / p
hp₁' : 1 < 1 / p
f : ℝ≥0 ≃o ℝ≥0 := orderIsoRpow (1 / p) hp₀'
h₁ : StrictConvexOn ℝ≥0 univ ↑f
⊢ ∀ (x : ℝ≥0), ↑(OrderIso.symm f) x = x ^ p
[PROOFSTEP]
simp [NNReal.orderIsoRpow_symm_eq]
[GOAL]
p : ℝ
hp₀ : 0 < p
hp₁ : p < 1
hp₀' : 0 < 1 / p
hp₁' : 1 < 1 / p
f : ℝ≥0 ≃o ℝ≥0 := orderIsoRpow (1 / p) hp₀'
h₁ : StrictConvexOn ℝ≥0 univ ↑f
h₂ : ∀ (x : ℝ≥0), ↑(OrderIso.symm f) x = x ^ p
⊢ StrictConcaveOn ℝ≥0 univ fun x => x ^ p
[PROOFSTEP]
refine ⟨convex_univ, fun x _ y _ hxy a b ha hb hab => ?_⟩
[GOAL]
p : ℝ
hp₀ : 0 < p
hp₁ : p < 1
hp₀' : 0 < 1 / p
hp₁' : 1 < 1 / p
f : ℝ≥0 ≃o ℝ≥0 := orderIsoRpow (1 / p) hp₀'
h₁ : StrictConvexOn ℝ≥0 univ ↑f
h₂ : ∀ (x : ℝ≥0), ↑(OrderIso.symm f) x = x ^ p
x : ℝ≥0
x✝¹ : x ∈ univ
y : ℝ≥0
x✝ : y ∈ univ
hxy : x ≠ y
a b : ℝ≥0
ha : 0 < a
hb : 0 < b
hab : a + b = 1
⊢ a • (fun x => x ^ p) x + b • (fun x => x ^ p) y < (fun x => x ^ p) (a • x + b • y)
[PROOFSTEP]
simp only [← h₂]
[GOAL]
p : ℝ
hp₀ : 0 < p
hp₁ : p < 1
hp₀' : 0 < 1 / p
hp₁' : 1 < 1 / p
f : ℝ≥0 ≃o ℝ≥0 := orderIsoRpow (1 / p) hp₀'
h₁ : StrictConvexOn ℝ≥0 univ ↑f
h₂ : ∀ (x : ℝ≥0), ↑(OrderIso.symm f) x = x ^ p
x : ℝ≥0
x✝¹ : x ∈ univ
y : ℝ≥0
x✝ : y ∈ univ
hxy : x ≠ y
a b : ℝ≥0
ha : 0 < a
hb : 0 < b
hab : a + b = 1
⊢ a • ↑(OrderIso.symm (orderIsoRpow (1 / p) hp₀')) x + b • ↑(OrderIso.symm (orderIsoRpow (1 / p) hp₀')) y <
    ↑(OrderIso.symm (orderIsoRpow (1 / p) hp₀')) (a • x + b • y)
[PROOFSTEP]
exact (f.strictConcaveOn_symm h₁).2 (Set.mem_univ x) (Set.mem_univ y) hxy ha hb hab
[GOAL]
p : ℝ
hp₀ : 0 ≤ p
hp₁ : p ≤ 1
⊢ ConcaveOn ℝ≥0 univ fun x => x ^ p
[PROOFSTEP]
by_cases hp : p = 0
[GOAL]
case pos
p : ℝ
hp₀ : 0 ≤ p
hp₁ : p ≤ 1
hp : p = 0
⊢ ConcaveOn ℝ≥0 univ fun x => x ^ p
case neg p : ℝ hp₀ : 0 ≤ p hp₁ : p ≤ 1 hp : ¬p = 0 ⊢ ConcaveOn ℝ≥0 univ fun x => x ^ p
[PROOFSTEP]
case pos => exact ⟨convex_univ, fun _ _ _ _ _ _ _ _ hab => by simp [hp, hab]⟩
[GOAL]
p : ℝ
hp₀ : 0 ≤ p
hp₁ : p ≤ 1
hp : p = 0
⊢ ConcaveOn ℝ≥0 univ fun x => x ^ p
[PROOFSTEP]
case pos => exact ⟨convex_univ, fun _ _ _ _ _ _ _ _ hab => by simp [hp, hab]⟩
[GOAL]
p : ℝ
hp₀ : 0 ≤ p
hp₁ : p ≤ 1
hp : p = 0
⊢ ConcaveOn ℝ≥0 univ fun x => x ^ p
[PROOFSTEP]
exact ⟨convex_univ, fun _ _ _ _ _ _ _ _ hab => by simp [hp, hab]⟩
[GOAL]
p : ℝ
hp₀ : 0 ≤ p
hp₁ : p ≤ 1
hp : p = 0
x✝⁷ : ℝ≥0
x✝⁶ : x✝⁷ ∈ univ
x✝⁵ : ℝ≥0
x✝⁴ : x✝⁵ ∈ univ
x✝³ x✝² : ℝ≥0
x✝¹ : 0 ≤ x✝³
x✝ : 0 ≤ x✝²
hab : x✝³ + x✝² = 1
⊢ x✝³ • (fun x => x ^ p) x✝⁷ + x✝² • (fun x => x ^ p) x✝⁵ ≤ (fun x => x ^ p) (x✝³ • x✝⁷ + x✝² • x✝⁵)
[PROOFSTEP]
simp [hp, hab]
[GOAL]
case neg
p : ℝ
hp₀ : 0 ≤ p
hp₁ : p ≤ 1
hp : ¬p = 0
⊢ ConcaveOn ℝ≥0 univ fun x => x ^ p
[PROOFSTEP]
case neg =>
  push_neg at hp 
  by_cases hp' : p = 1
  case pos => exact ⟨convex_univ, by simp [hp']⟩
  case neg =>
    push_neg at hp' 
    exact (strictConcaveOn_rpow (by positivity) (lt_of_le_of_ne hp₁ hp')).concaveOn
[GOAL]
p : ℝ
hp₀ : 0 ≤ p
hp₁ : p ≤ 1
hp : ¬p = 0
⊢ ConcaveOn ℝ≥0 univ fun x => x ^ p
[PROOFSTEP]
case neg =>
  push_neg at hp 
  by_cases hp' : p = 1
  case pos => exact ⟨convex_univ, by simp [hp']⟩
  case neg =>
    push_neg at hp' 
    exact (strictConcaveOn_rpow (by positivity) (lt_of_le_of_ne hp₁ hp')).concaveOn
[GOAL]
p : ℝ
hp₀ : 0 ≤ p
hp₁ : p ≤ 1
hp : ¬p = 0
⊢ ConcaveOn ℝ≥0 univ fun x => x ^ p
[PROOFSTEP]
push_neg at hp 
[GOAL]
p : ℝ
hp₀ : 0 ≤ p
hp₁ : p ≤ 1
hp : p ≠ 0
⊢ ConcaveOn ℝ≥0 univ fun x => x ^ p
[PROOFSTEP]
by_cases hp' : p = 1
[GOAL]
case pos
p : ℝ
hp₀ : 0 ≤ p
hp₁ : p ≤ 1
hp : p ≠ 0
hp' : p = 1
⊢ ConcaveOn ℝ≥0 univ fun x => x ^ p
case neg p : ℝ hp₀ : 0 ≤ p hp₁ : p ≤ 1 hp : p ≠ 0 hp' : ¬p = 1 ⊢ ConcaveOn ℝ≥0 univ fun x => x ^ p
[PROOFSTEP]
case pos => exact ⟨convex_univ, by simp [hp']⟩
[GOAL]
p : ℝ
hp₀ : 0 ≤ p
hp₁ : p ≤ 1
hp : p ≠ 0
hp' : p = 1
⊢ ConcaveOn ℝ≥0 univ fun x => x ^ p
[PROOFSTEP]
case pos => exact ⟨convex_univ, by simp [hp']⟩
[GOAL]
p : ℝ
hp₀ : 0 ≤ p
hp₁ : p ≤ 1
hp : p ≠ 0
hp' : p = 1
⊢ ConcaveOn ℝ≥0 univ fun x => x ^ p
[PROOFSTEP]
exact ⟨convex_univ, by simp [hp']⟩
[GOAL]
p : ℝ
hp₀ : 0 ≤ p
hp₁ : p ≤ 1
hp : p ≠ 0
hp' : p = 1
⊢ ∀ ⦃x : ℝ≥0⦄,
    x ∈ univ →
      ∀ ⦃y : ℝ≥0⦄,
        y ∈ univ →
          ∀ ⦃a b : ℝ≥0⦄,
            0 ≤ a →
              0 ≤ b → a + b = 1 → a • (fun x => x ^ p) x + b • (fun x => x ^ p) y ≤ (fun x => x ^ p) (a • x + b • y)
[PROOFSTEP]
simp [hp']
[GOAL]
case neg
p : ℝ
hp₀ : 0 ≤ p
hp₁ : p ≤ 1
hp : p ≠ 0
hp' : ¬p = 1
⊢ ConcaveOn ℝ≥0 univ fun x => x ^ p
[PROOFSTEP]
case neg =>
  push_neg at hp' 
  exact (strictConcaveOn_rpow (by positivity) (lt_of_le_of_ne hp₁ hp')).concaveOn
[GOAL]
p : ℝ
hp₀ : 0 ≤ p
hp₁ : p ≤ 1
hp : p ≠ 0
hp' : ¬p = 1
⊢ ConcaveOn ℝ≥0 univ fun x => x ^ p
[PROOFSTEP]
case neg =>
  push_neg at hp' 
  exact (strictConcaveOn_rpow (by positivity) (lt_of_le_of_ne hp₁ hp')).concaveOn
[GOAL]
p : ℝ
hp₀ : 0 ≤ p
hp₁ : p ≤ 1
hp : p ≠ 0
hp' : ¬p = 1
⊢ ConcaveOn ℝ≥0 univ fun x => x ^ p
[PROOFSTEP]
push_neg at hp' 
[GOAL]
p : ℝ
hp₀ : 0 ≤ p
hp₁ : p ≤ 1
hp : p ≠ 0
hp' : p ≠ 1
⊢ ConcaveOn ℝ≥0 univ fun x => x ^ p
[PROOFSTEP]
exact (strictConcaveOn_rpow (by positivity) (lt_of_le_of_ne hp₁ hp')).concaveOn
[GOAL]
p : ℝ
hp₀ : 0 ≤ p
hp₁ : p ≤ 1
hp : p ≠ 0
hp' : p ≠ 1
⊢ 0 < p
[PROOFSTEP]
positivity
[GOAL]
⊢ StrictConcaveOn ℝ≥0 univ ↑sqrt
[PROOFSTEP]
have : NNReal.sqrt = fun (x : ℝ≥0) ↦ x ^ (1 / (2 : ℝ)) := by ext x; exact_mod_cast NNReal.sqrt_eq_rpow x
[GOAL]
⊢ ↑sqrt = fun x => x ^ (1 / 2)
[PROOFSTEP]
ext x
[GOAL]
case h.a
x : ℝ≥0
⊢ ↑(↑sqrt x) = ↑(x ^ (1 / 2))
[PROOFSTEP]
exact_mod_cast NNReal.sqrt_eq_rpow x
[GOAL]
this : ↑sqrt = fun x => x ^ (1 / 2)
⊢ StrictConcaveOn ℝ≥0 univ ↑sqrt
[PROOFSTEP]
rw [this]
[GOAL]
this : ↑sqrt = fun x => x ^ (1 / 2)
⊢ StrictConcaveOn ℝ≥0 univ fun x => x ^ (1 / 2)
[PROOFSTEP]
exact strictConcaveOn_rpow (by positivity) (by linarith)
[GOAL]
this : ↑sqrt = fun x => x ^ (1 / 2)
⊢ 0 < 1 / 2
[PROOFSTEP]
positivity
[GOAL]
this : ↑sqrt = fun x => x ^ (1 / 2)
⊢ 1 / 2 < 1
[PROOFSTEP]
linarith
[GOAL]
p : ℝ
hp₀ : 0 < p
hp₁ : p < 1
⊢ StrictConcaveOn ℝ (Ici 0) fun x => x ^ p
[PROOFSTEP]
refine ⟨convex_Ici _, fun x hx y hy hxy a b ha hb hab => ?_⟩
[GOAL]
p : ℝ
hp₀ : 0 < p
hp₁ : p < 1
x : ℝ
hx : x ∈ Ici 0
y : ℝ
hy : y ∈ Ici 0
hxy : x ≠ y
a b : ℝ
ha : 0 < a
hb : 0 < b
hab : a + b = 1
⊢ a • (fun x => x ^ p) x + b • (fun x => x ^ p) y < (fun x => x ^ p) (a • x + b • y)
[PROOFSTEP]
let x' : ℝ≥0 := ⟨x, hx⟩
[GOAL]
p : ℝ
hp₀ : 0 < p
hp₁ : p < 1
x : ℝ
hx : x ∈ Ici 0
y : ℝ
hy : y ∈ Ici 0
hxy : x ≠ y
a b : ℝ
ha : 0 < a
hb : 0 < b
hab : a + b = 1
x' : ℝ≥0 := { val := x, property := hx }
⊢ a • (fun x => x ^ p) x + b • (fun x => x ^ p) y < (fun x => x ^ p) (a • x + b • y)
[PROOFSTEP]
let y' : ℝ≥0 := ⟨y, hy⟩
[GOAL]
p : ℝ
hp₀ : 0 < p
hp₁ : p < 1
x : ℝ
hx : x ∈ Ici 0
y : ℝ
hy : y ∈ Ici 0
hxy : x ≠ y
a b : ℝ
ha : 0 < a
hb : 0 < b
hab : a + b = 1
x' : ℝ≥0 := { val := x, property := hx }
y' : ℝ≥0 := { val := y, property := hy }
⊢ a • (fun x => x ^ p) x + b • (fun x => x ^ p) y < (fun x => x ^ p) (a • x + b • y)
[PROOFSTEP]
let a' : ℝ≥0 := ⟨a, by positivity⟩
[GOAL]
p : ℝ
hp₀ : 0 < p
hp₁ : p < 1
x : ℝ
hx : x ∈ Ici 0
y : ℝ
hy : y ∈ Ici 0
hxy : x ≠ y
a b : ℝ
ha : 0 < a
hb : 0 < b
hab : a + b = 1
x' : ℝ≥0 := { val := x, property := hx }
y' : ℝ≥0 := { val := y, property := hy }
⊢ 0 ≤ a
[PROOFSTEP]
positivity
[GOAL]
p : ℝ
hp₀ : 0 < p
hp₁ : p < 1
x : ℝ
hx : x ∈ Ici 0
y : ℝ
hy : y ∈ Ici 0
hxy : x ≠ y
a b : ℝ
ha : 0 < a
hb : 0 < b
hab : a + b = 1
x' : ℝ≥0 := { val := x, property := hx }
y' : ℝ≥0 := { val := y, property := hy }
a' : ℝ≥0 := { val := a, property := (_ : 0 ≤ a) }
⊢ a • (fun x => x ^ p) x + b • (fun x => x ^ p) y < (fun x => x ^ p) (a • x + b • y)
[PROOFSTEP]
let b' : ℝ≥0 := ⟨b, by positivity⟩
[GOAL]
p : ℝ
hp₀ : 0 < p
hp₁ : p < 1
x : ℝ
hx : x ∈ Ici 0
y : ℝ
hy : y ∈ Ici 0
hxy : x ≠ y
a b : ℝ
ha : 0 < a
hb : 0 < b
hab : a + b = 1
x' : ℝ≥0 := { val := x, property := hx }
y' : ℝ≥0 := { val := y, property := hy }
a' : ℝ≥0 := { val := a, property := (_ : 0 ≤ a) }
⊢ 0 ≤ b
[PROOFSTEP]
positivity
[GOAL]
p : ℝ
hp₀ : 0 < p
hp₁ : p < 1
x : ℝ
hx : x ∈ Ici 0
y : ℝ
hy : y ∈ Ici 0
hxy : x ≠ y
a b : ℝ
ha : 0 < a
hb : 0 < b
hab : a + b = 1
x' : ℝ≥0 := { val := x, property := hx }
y' : ℝ≥0 := { val := y, property := hy }
a' : ℝ≥0 := { val := a, property := (_ : 0 ≤ a) }
b' : ℝ≥0 := { val := b, property := (_ : 0 ≤ b) }
⊢ a • (fun x => x ^ p) x + b • (fun x => x ^ p) y < (fun x => x ^ p) (a • x + b • y)
[PROOFSTEP]
have hx' : (fun z => z ^ p) x = (fun z => z ^ p) x' := rfl
[GOAL]
p : ℝ
hp₀ : 0 < p
hp₁ : p < 1
x : ℝ
hx : x ∈ Ici 0
y : ℝ
hy : y ∈ Ici 0
hxy : x ≠ y
a b : ℝ
ha : 0 < a
hb : 0 < b
hab : a + b = 1
x' : ℝ≥0 := { val := x, property := hx }
y' : ℝ≥0 := { val := y, property := hy }
a' : ℝ≥0 := { val := a, property := (_ : 0 ≤ a) }
b' : ℝ≥0 := { val := b, property := (_ : 0 ≤ b) }
hx' : (fun z => z ^ p) x = ↑((fun z => z ^ p) x')
⊢ a • (fun x => x ^ p) x + b • (fun x => x ^ p) y < (fun x => x ^ p) (a • x + b • y)
[PROOFSTEP]
have hy' : (fun z => z ^ p) y = (fun z => z ^ p) y' := rfl
[GOAL]
p : ℝ
hp₀ : 0 < p
hp₁ : p < 1
x : ℝ
hx : x ∈ Ici 0
y : ℝ
hy : y ∈ Ici 0
hxy : x ≠ y
a b : ℝ
ha : 0 < a
hb : 0 < b
hab : a + b = 1
x' : ℝ≥0 := { val := x, property := hx }
y' : ℝ≥0 := { val := y, property := hy }
a' : ℝ≥0 := { val := a, property := (_ : 0 ≤ a) }
b' : ℝ≥0 := { val := b, property := (_ : 0 ≤ b) }
hx' : (fun z => z ^ p) x = ↑((fun z => z ^ p) x')
hy' : (fun z => z ^ p) y = ↑((fun z => z ^ p) y')
⊢ a • (fun x => x ^ p) x + b • (fun x => x ^ p) y < (fun x => x ^ p) (a • x + b • y)
[PROOFSTEP]
have hxy' : x' ≠ y' := Subtype.ne_of_val_ne hxy
[GOAL]
p : ℝ
hp₀ : 0 < p
hp₁ : p < 1
x : ℝ
hx : x ∈ Ici 0
y : ℝ
hy : y ∈ Ici 0
hxy : x ≠ y
a b : ℝ
ha : 0 < a
hb : 0 < b
hab : a + b = 1
x' : ℝ≥0 := { val := x, property := hx }
y' : ℝ≥0 := { val := y, property := hy }
a' : ℝ≥0 := { val := a, property := (_ : 0 ≤ a) }
b' : ℝ≥0 := { val := b, property := (_ : 0 ≤ b) }
hx' : (fun z => z ^ p) x = ↑((fun z => z ^ p) x')
hy' : (fun z => z ^ p) y = ↑((fun z => z ^ p) y')
hxy' : x' ≠ y'
⊢ a • (fun x => x ^ p) x + b • (fun x => x ^ p) y < (fun x => x ^ p) (a • x + b • y)
[PROOFSTEP]
have hab' : a' + b' = 1 := by ext; simp [hab]
[GOAL]
p : ℝ
hp₀ : 0 < p
hp₁ : p < 1
x : ℝ
hx : x ∈ Ici 0
y : ℝ
hy : y ∈ Ici 0
hxy : x ≠ y
a b : ℝ
ha : 0 < a
hb : 0 < b
hab : a + b = 1
x' : ℝ≥0 := { val := x, property := hx }
y' : ℝ≥0 := { val := y, property := hy }
a' : ℝ≥0 := { val := a, property := (_ : 0 ≤ a) }
b' : ℝ≥0 := { val := b, property := (_ : 0 ≤ b) }
hx' : (fun z => z ^ p) x = ↑((fun z => z ^ p) x')
hy' : (fun z => z ^ p) y = ↑((fun z => z ^ p) y')
hxy' : x' ≠ y'
⊢ a' + b' = 1
[PROOFSTEP]
ext
[GOAL]
case a
p : ℝ
hp₀ : 0 < p
hp₁ : p < 1
x : ℝ
hx : x ∈ Ici 0
y : ℝ
hy : y ∈ Ici 0
hxy : x ≠ y
a b : ℝ
ha : 0 < a
hb : 0 < b
hab : a + b = 1
x' : ℝ≥0 := { val := x, property := hx }
y' : ℝ≥0 := { val := y, property := hy }
a' : ℝ≥0 := { val := a, property := (_ : 0 ≤ a) }
b' : ℝ≥0 := { val := b, property := (_ : 0 ≤ b) }
hx' : (fun z => z ^ p) x = ↑((fun z => z ^ p) x')
hy' : (fun z => z ^ p) y = ↑((fun z => z ^ p) y')
hxy' : x' ≠ y'
⊢ ↑(a' + b') = ↑1
[PROOFSTEP]
simp [hab]
[GOAL]
p : ℝ
hp₀ : 0 < p
hp₁ : p < 1
x : ℝ
hx : x ∈ Ici 0
y : ℝ
hy : y ∈ Ici 0
hxy : x ≠ y
a b : ℝ
ha : 0 < a
hb : 0 < b
hab : a + b = 1
x' : ℝ≥0 := { val := x, property := hx }
y' : ℝ≥0 := { val := y, property := hy }
a' : ℝ≥0 := { val := a, property := (_ : 0 ≤ a) }
b' : ℝ≥0 := { val := b, property := (_ : 0 ≤ b) }
hx' : (fun z => z ^ p) x = ↑((fun z => z ^ p) x')
hy' : (fun z => z ^ p) y = ↑((fun z => z ^ p) y')
hxy' : x' ≠ y'
hab' : a' + b' = 1
⊢ a • (fun x => x ^ p) x + b • (fun x => x ^ p) y < (fun x => x ^ p) (a • x + b • y)
[PROOFSTEP]
rw [hx', hy']
[GOAL]
p : ℝ
hp₀ : 0 < p
hp₁ : p < 1
x : ℝ
hx : x ∈ Ici 0
y : ℝ
hy : y ∈ Ici 0
hxy : x ≠ y
a b : ℝ
ha : 0 < a
hb : 0 < b
hab : a + b = 1
x' : ℝ≥0 := { val := x, property := hx }
y' : ℝ≥0 := { val := y, property := hy }
a' : ℝ≥0 := { val := a, property := (_ : 0 ≤ a) }
b' : ℝ≥0 := { val := b, property := (_ : 0 ≤ b) }
hx' : (fun z => z ^ p) x = ↑((fun z => z ^ p) x')
hy' : (fun z => z ^ p) y = ↑((fun z => z ^ p) y')
hxy' : x' ≠ y'
hab' : a' + b' = 1
⊢ a • ↑((fun z => z ^ p) x') + b • ↑((fun z => z ^ p) y') < (fun x => x ^ p) (a • x + b • y)
[PROOFSTEP]
exact
  (NNReal.strictConcaveOn_rpow hp₀ hp₁).2 (Set.mem_univ x') (Set.mem_univ y') hxy' (by exact_mod_cast ha)
    (by exact_mod_cast hb) hab'
[GOAL]
p : ℝ
hp₀ : 0 < p
hp₁ : p < 1
x : ℝ
hx : x ∈ Ici 0
y : ℝ
hy : y ∈ Ici 0
hxy : x ≠ y
a b : ℝ
ha : 0 < a
hb : 0 < b
hab : a + b = 1
x' : ℝ≥0 := { val := x, property := hx }
y' : ℝ≥0 := { val := y, property := hy }
a' : ℝ≥0 := { val := a, property := (_ : 0 ≤ a) }
b' : ℝ≥0 := { val := b, property := (_ : 0 ≤ b) }
hx' : (fun z => z ^ p) x = ↑((fun z => z ^ p) x')
hy' : (fun z => z ^ p) y = ↑((fun z => z ^ p) y')
hxy' : x' ≠ y'
hab' : a' + b' = 1
⊢ 0 < a'
[PROOFSTEP]
exact_mod_cast ha
[GOAL]
p : ℝ
hp₀ : 0 < p
hp₁ : p < 1
x : ℝ
hx : x ∈ Ici 0
y : ℝ
hy : y ∈ Ici 0
hxy : x ≠ y
a b : ℝ
ha : 0 < a
hb : 0 < b
hab : a + b = 1
x' : ℝ≥0 := { val := x, property := hx }
y' : ℝ≥0 := { val := y, property := hy }
a' : ℝ≥0 := { val := a, property := (_ : 0 ≤ a) }
b' : ℝ≥0 := { val := b, property := (_ : 0 ≤ b) }
hx' : (fun z => z ^ p) x = ↑((fun z => z ^ p) x')
hy' : (fun z => z ^ p) y = ↑((fun z => z ^ p) y')
hxy' : x' ≠ y'
hab' : a' + b' = 1
⊢ 0 < b'
[PROOFSTEP]
exact_mod_cast hb
[GOAL]
p : ℝ
hp₀ : 0 ≤ p
hp₁ : p ≤ 1
⊢ ConcaveOn ℝ (Ici 0) fun x => x ^ p
[PROOFSTEP]
by_cases hp : p = 0
[GOAL]
case pos
p : ℝ
hp₀ : 0 ≤ p
hp₁ : p ≤ 1
hp : p = 0
⊢ ConcaveOn ℝ (Ici 0) fun x => x ^ p
case neg p : ℝ hp₀ : 0 ≤ p hp₁ : p ≤ 1 hp : ¬p = 0 ⊢ ConcaveOn ℝ (Ici 0) fun x => x ^ p
[PROOFSTEP]
case pos => exact ⟨convex_Ici 0, fun _ _ _ _ _ _ _ _ hab => by simp [hp, hab]⟩
[GOAL]
p : ℝ
hp₀ : 0 ≤ p
hp₁ : p ≤ 1
hp : p = 0
⊢ ConcaveOn ℝ (Ici 0) fun x => x ^ p
[PROOFSTEP]
case pos => exact ⟨convex_Ici 0, fun _ _ _ _ _ _ _ _ hab => by simp [hp, hab]⟩
[GOAL]
p : ℝ
hp₀ : 0 ≤ p
hp₁ : p ≤ 1
hp : p = 0
⊢ ConcaveOn ℝ (Ici 0) fun x => x ^ p
[PROOFSTEP]
exact ⟨convex_Ici 0, fun _ _ _ _ _ _ _ _ hab => by simp [hp, hab]⟩
[GOAL]
p : ℝ
hp₀ : 0 ≤ p
hp₁ : p ≤ 1
hp : p = 0
x✝⁷ : ℝ
x✝⁶ : x✝⁷ ∈ Ici 0
x✝⁵ : ℝ
x✝⁴ : x✝⁵ ∈ Ici 0
x✝³ x✝² : ℝ
x✝¹ : 0 ≤ x✝³
x✝ : 0 ≤ x✝²
hab : x✝³ + x✝² = 1
⊢ x✝³ • (fun x => x ^ p) x✝⁷ + x✝² • (fun x => x ^ p) x✝⁵ ≤ (fun x => x ^ p) (x✝³ • x✝⁷ + x✝² • x✝⁵)
[PROOFSTEP]
simp [hp, hab]
[GOAL]
case neg
p : ℝ
hp₀ : 0 ≤ p
hp₁ : p ≤ 1
hp : ¬p = 0
⊢ ConcaveOn ℝ (Ici 0) fun x => x ^ p
[PROOFSTEP]
case neg =>
  push_neg at hp 
  by_cases hp' : p = 1
  case pos => exact ⟨convex_Ici 0, by simp [hp']⟩
  case neg =>
    push_neg at hp' 
    exact (strictConcaveOn_rpow (by positivity) (lt_of_le_of_ne hp₁ hp')).concaveOn
[GOAL]
p : ℝ
hp₀ : 0 ≤ p
hp₁ : p ≤ 1
hp : ¬p = 0
⊢ ConcaveOn ℝ (Ici 0) fun x => x ^ p
[PROOFSTEP]
case neg =>
  push_neg at hp 
  by_cases hp' : p = 1
  case pos => exact ⟨convex_Ici 0, by simp [hp']⟩
  case neg =>
    push_neg at hp' 
    exact (strictConcaveOn_rpow (by positivity) (lt_of_le_of_ne hp₁ hp')).concaveOn
[GOAL]
p : ℝ
hp₀ : 0 ≤ p
hp₁ : p ≤ 1
hp : ¬p = 0
⊢ ConcaveOn ℝ (Ici 0) fun x => x ^ p
[PROOFSTEP]
push_neg at hp 
[GOAL]
p : ℝ
hp₀ : 0 ≤ p
hp₁ : p ≤ 1
hp : p ≠ 0
⊢ ConcaveOn ℝ (Ici 0) fun x => x ^ p
[PROOFSTEP]
by_cases hp' : p = 1
[GOAL]
case pos
p : ℝ
hp₀ : 0 ≤ p
hp₁ : p ≤ 1
hp : p ≠ 0
hp' : p = 1
⊢ ConcaveOn ℝ (Ici 0) fun x => x ^ p
case neg p : ℝ hp₀ : 0 ≤ p hp₁ : p ≤ 1 hp : p ≠ 0 hp' : ¬p = 1 ⊢ ConcaveOn ℝ (Ici 0) fun x => x ^ p
[PROOFSTEP]
case pos => exact ⟨convex_Ici 0, by simp [hp']⟩
[GOAL]
p : ℝ
hp₀ : 0 ≤ p
hp₁ : p ≤ 1
hp : p ≠ 0
hp' : p = 1
⊢ ConcaveOn ℝ (Ici 0) fun x => x ^ p
[PROOFSTEP]
case pos => exact ⟨convex_Ici 0, by simp [hp']⟩
[GOAL]
p : ℝ
hp₀ : 0 ≤ p
hp₁ : p ≤ 1
hp : p ≠ 0
hp' : p = 1
⊢ ConcaveOn ℝ (Ici 0) fun x => x ^ p
[PROOFSTEP]
exact ⟨convex_Ici 0, by simp [hp']⟩
[GOAL]
p : ℝ
hp₀ : 0 ≤ p
hp₁ : p ≤ 1
hp : p ≠ 0
hp' : p = 1
⊢ ∀ ⦃x : ℝ⦄,
    x ∈ Ici 0 →
      ∀ ⦃y : ℝ⦄,
        y ∈ Ici 0 →
          ∀ ⦃a b : ℝ⦄,
            0 ≤ a →
              0 ≤ b → a + b = 1 → a • (fun x => x ^ p) x + b • (fun x => x ^ p) y ≤ (fun x => x ^ p) (a • x + b • y)
[PROOFSTEP]
simp [hp']
[GOAL]
case neg
p : ℝ
hp₀ : 0 ≤ p
hp₁ : p ≤ 1
hp : p ≠ 0
hp' : ¬p = 1
⊢ ConcaveOn ℝ (Ici 0) fun x => x ^ p
[PROOFSTEP]
case neg =>
  push_neg at hp' 
  exact (strictConcaveOn_rpow (by positivity) (lt_of_le_of_ne hp₁ hp')).concaveOn
[GOAL]
p : ℝ
hp₀ : 0 ≤ p
hp₁ : p ≤ 1
hp : p ≠ 0
hp' : ¬p = 1
⊢ ConcaveOn ℝ (Ici 0) fun x => x ^ p
[PROOFSTEP]
case neg =>
  push_neg at hp' 
  exact (strictConcaveOn_rpow (by positivity) (lt_of_le_of_ne hp₁ hp')).concaveOn
[GOAL]
p : ℝ
hp₀ : 0 ≤ p
hp₁ : p ≤ 1
hp : p ≠ 0
hp' : ¬p = 1
⊢ ConcaveOn ℝ (Ici 0) fun x => x ^ p
[PROOFSTEP]
push_neg at hp' 
[GOAL]
p : ℝ
hp₀ : 0 ≤ p
hp₁ : p ≤ 1
hp : p ≠ 0
hp' : p ≠ 1
⊢ ConcaveOn ℝ (Ici 0) fun x => x ^ p
[PROOFSTEP]
exact (strictConcaveOn_rpow (by positivity) (lt_of_le_of_ne hp₁ hp')).concaveOn
[GOAL]
p : ℝ
hp₀ : 0 ≤ p
hp₁ : p ≤ 1
hp : p ≠ 0
hp' : p ≠ 1
⊢ 0 < p
[PROOFSTEP]
positivity
[GOAL]
⊢ StrictConcaveOn ℝ (Ici 0) sqrt
[PROOFSTEP]
have : Real.sqrt = fun (x : ℝ) ↦ x ^ (1 / (2 : ℝ)) := by ext x; exact Real.sqrt_eq_rpow x
[GOAL]
⊢ sqrt = fun x => x ^ (1 / 2)
[PROOFSTEP]
ext x
[GOAL]
case h
x : ℝ
⊢ sqrt x = x ^ (1 / 2)
[PROOFSTEP]
exact Real.sqrt_eq_rpow x
[GOAL]
this : sqrt = fun x => x ^ (1 / 2)
⊢ StrictConcaveOn ℝ (Ici 0) sqrt
[PROOFSTEP]
rw [this]
[GOAL]
this : sqrt = fun x => x ^ (1 / 2)
⊢ StrictConcaveOn ℝ (Ici 0) fun x => x ^ (1 / 2)
[PROOFSTEP]
exact strictConcaveOn_rpow (by positivity) (by linarith)
[GOAL]
this : sqrt = fun x => x ^ (1 / 2)
⊢ 0 < 1 / 2
[PROOFSTEP]
positivity
[GOAL]
this : sqrt = fun x => x ^ (1 / 2)
⊢ 1 / 2 < 1
[PROOFSTEP]
linarith
