awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Analysis.Convex.SpecificFunctions.Deriv
Goal:
x : ℝ
hx : 0 < x
h₀ : √x ≠ 0
h :
  -log x / (4 * HPow.hPow (β := ℕ) (√x) 3) =
    ((√x * √x)⁻¹ * (2 * √x) - (2 + log x) * (2 * (1 / (2 * √x)))) / HPow.hPow (β := ℕ) (2 * √x) 2
⊢ -log x / (4 * HPow.hPow (β := ℕ) (√x) 3) =
    (x⁻¹ * (2 * √x) - (2 + log x) * (2 * (1 / (2 * √x)))) / HPow.hPow (β := ℕ) (2 * √x) 2

Tactic:
nth_rw 3 [← mul_self_sqrt hx.le]

Premises used: Real.mul_self_sqrt, LT.lt.le
-- Module: Mathlib.Analysis.Convex.SpecificFunctions.Deriv
Goal:
x : ℝ
hx : 0 < x
h₀ : √x ≠ 0
⊢ -log x / (4 * HPow.hPow (β := ℕ) (√x) 3) =
    ((√x * √x)⁻¹ * (2 * √x) - (2 + log x) * (2 * (1 / (2 * √x)))) / HPow.hPow (β := ℕ) (2 * √x) 2

Tactic:
field
-- Module: Mathlib.Analysis.Convex.SpecificFunctions.Deriv
Goal:
apply : ContinuousOn (Y := ℝ) (fun (x : ℝ) ↦ √x * log x) (Ioi 1)
apply₁ :
  ∀ (x : ℝ) (hx : Membership.mem (γ := Set ℝ) (Ioi 1) x),
    LT.lt (α := ℝ) (deriv^[2] (fun (x : ℝ) ↦ √x * log x) x : ℝ) (0 : ℝ)
⊢ StrictConcaveOn ℝ (β := ℝ) (Ioi 1) fun (x : ℝ) ↦ √x * log x

Tactic:
apply strictConcaveOn_of_deriv2_neg' (convex_Ioi 1) _ fun x hx => ?_

Premises used: strictConcaveOn_of_deriv2_neg', OfNat.ofNat, convex_Ioi
-- Module: Mathlib.Analysis.Convex.SpecificFunctions.Deriv
Goal:
⊢ ContinuousOn (Y := ℝ) (fun (x : ℝ) ↦ √x * log x) (Ioi 1)

Tactic:
continuous_sqrt.continuousOn.mul
      (continuousOn_log.mono fun x hx => ne_of_gt (zero_lt_one.trans hx))

Premises used: Continuous.continuousOn, Real.continuousOn_log, Real.continuous_sqrt, ne_of_gt, zero_lt_one, LT.lt.trans, ContinuousOn.mono, ContinuousOn.mul
-- Module: Mathlib.Analysis.Convex.SpecificFunctions.Deriv
Goal:
⊢ ContinuousOn (Y := ℝ) (fun (x : ℝ) ↦ √x * log x) (Ioi 1)

Tactic:
exact continuous_sqrt.continuousOn.mul
      (continuousOn_log.mono fun x hx => ne_of_gt (zero_lt_one.trans hx))

Premises used: Continuous.continuousOn, Real.continuousOn_log, Real.continuous_sqrt, ne_of_gt, zero_lt_one, LT.lt.trans, ContinuousOn.mono, ContinuousOn.mul
-- Module: Mathlib.Analysis.Convex.SpecificFunctions.Deriv
Goal:
x : ℝ
hx : Membership.mem (γ := Set ℝ) (Ioi 1) x
rw : -log x / (4 * HPow.hPow (β := ℕ) (√x) 3) < 0
⊢ LT.lt (α := ℝ) (deriv^[2] (fun (x : ℝ) ↦ √x * log x) x : ℝ) (0 : ℝ)

Tactic:
rw [deriv2_sqrt_mul_log x]

Premises used: deriv2_sqrt_mul_log
-- Module: Mathlib.Analysis.Convex.SpecificFunctions.Deriv
Goal:
x : ℝ
hx : Membership.mem (γ := Set ℝ) (Ioi 1) x
⊢ -log x / (4 * HPow.hPow (β := ℕ) (√x) 3) < 0

Tactic:
div_neg_of_neg_of_pos (neg_neg_of_pos (log_pos hx))
      (mul_pos four_pos (pow_pos (sqrt_pos.mpr (zero_lt_one.trans hx)) 3))

Premises used: Iff.mpr, pow_pos, four_pos, Real.log_pos, zero_lt_one, mul_pos, Real.sqrt_pos, LT.lt.trans, neg_neg_of_pos, div_neg_of_neg_of_pos, OfNat.ofNat
-- Module: Mathlib.Analysis.Convex.SpecificFunctions.Deriv
Goal:
x : ℝ
hx : Membership.mem (γ := Set ℝ) (Ioi 1) x
⊢ -log x / (4 * HPow.hPow (β := ℕ) (√x) 3) < 0

Tactic:
exact div_neg_of_neg_of_pos (neg_neg_of_pos (log_pos hx))
      (mul_pos four_pos (pow_pos (sqrt_pos.mpr (zero_lt_one.trans hx)) 3))

Premises used: Iff.mpr, pow_pos, four_pos, Real.log_pos, zero_lt_one, mul_pos, Real.sqrt_pos, LT.lt.trans, neg_neg_of_pos, div_neg_of_neg_of_pos, OfNat.ofNat
-- Module: Mathlib.Analysis.Convex.SpecificFunctions.Deriv
Goal:
apply : ∀ (x : ℝ) (hx : x ∈ interior (Icc 0 π)), deriv^[2] sin x < 0
⊢ StrictConcaveOn ℝ (Icc 0 π) sin

Tactic:
apply strictConcaveOn_of_deriv2_neg (convex_Icc _ _) continuousOn_sin fun x hx => ?_

Premises used: Real.continuousOn_sin, convex_Icc, strictConcaveOn_of_deriv2_neg
-- Module: Mathlib.Analysis.Convex.SpecificFunctions.Deriv
Goal:
x : ℝ
hx : x ∈ interior (Icc 0 π)
⊢ x ∈ Ioo 0 π

Tactic:
rw [interior_Icc] at hx

Premises used: interior_Icc
-- Module: Mathlib.Analysis.Convex.SpecificFunctions.Deriv
Goal:
x : ℝ
hx : x ∈ Ioo 0 π
⊢ deriv^[2] sin x < 0

Tactic:
simp [sin_pos_of_mem_Ioo hx]

Premises used: Real.sin_pos_of_mem_Ioo
-- Module: Mathlib.Analysis.Convex.SpecificFunctions.Deriv
Goal:
apply : ∀ (x : ℝ) (hx : x ∈ interior (Icc (-(π / 2)) (π / 2))), deriv^[2] cos x < 0
⊢ StrictConcaveOn ℝ (Icc (-(π / 2)) (π / 2)) cos

Tactic:
apply strictConcaveOn_of_deriv2_neg (convex_Icc _ _) continuousOn_cos fun x hx => ?_

Premises used: Real.continuousOn_cos, convex_Icc, strictConcaveOn_of_deriv2_neg
-- Module: Mathlib.Analysis.Convex.SpecificFunctions.Deriv
Goal:
x : ℝ
hx : x ∈ interior (Icc (-(π / 2)) (π / 2))
⊢ x ∈ Ioo (-(π / 2)) (π / 2)

Tactic:
rw [interior_Icc] at hx

Premises used: interior_Icc
-- Module: Mathlib.Analysis.Convex.SpecificFunctions.Deriv
Goal:
x : ℝ
hx : x ∈ Ioo (-(π / 2)) (π / 2)
⊢ deriv^[2] cos x < 0

Tactic:
simp [cos_pos_of_mem_Ioo hx]

Premises used: Real.cos_pos_of_mem_Ioo
-- Module: Mathlib.Analysis.Convex.SpecificFunctions.Pow
Goal:
p : ℝ
hp₀ : 0 < p
hp₁ : p < 1
⊢ 0 < 1 / p

Tactic:
have hp₀' : 0 < 1 / p := div_pos zero_lt_one hp₀
-- Module: Mathlib.Analysis.Convex.SpecificFunctions.Pow
Goal:
p : ℝ
hp₀ : 0 < p
hp₁ : p < 1
hp₀' : 0 < 1 / p
rw : p < 1
⊢ 1 < 1 / p

Tactic:
rw [one_lt_div hp₀]

Premises used: one_lt_div
-- Module: Mathlib.Analysis.Convex.SpecificFunctions.Pow
Goal:
p : ℝ
hp₀ : 0 < p
hp₁ : p < 1
hp₀' : 0 < 1 / p
⊢ p < 1

Tactic:
hp₁
-- Module: Mathlib.Analysis.Convex.SpecificFunctions.Pow
Goal:
p : ℝ
hp₀ : 0 < p
hp₁ : p < 1
hp₀' : 0 < 1 / p
⊢ p < 1

Tactic:
exact hp₁
-- Module: Mathlib.Analysis.Convex.SpecificFunctions.Pow
Goal:
p : ℝ
hp₀ : 0 < p
hp₁ : p < 1
hp₀' : 0 < 1 / p
⊢ 1 < 1 / p

Tactic:
have hp₁' : 1 < 1 / p := by rw [one_lt_div hp₀]; exact hp₁
-- Module: Mathlib.Analysis.Convex.SpecificFunctions.Pow
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 (E := ℝ≥0) (β := ℝ≥0) univ (⇑f : (a : ℝ≥0) → ℝ≥0)

Tactic:
⟨convex_univ, fun x _ y _ hxy a b ha hb hab => ?_⟩

Premises used: StrictConvexOn, convex_univ, And.intro
-- Module: Mathlib.Analysis.Convex.SpecificFunctions.Pow
Goal:
p : ℝ
hp₀ : 0 < p
hp₁ : p < 1
hp₀' : 0 < 1 / p
hp₁' : 1 < 1 / p
f : ℝ≥0 ≃o ℝ≥0 := orderIsoRpow (1 / p) hp₀'
refine :
  ∀ (x : ℝ≥0),
    Membership.mem (γ := Set ℝ≥0) univ x →
      ∀ (y : ℝ≥0),
        Membership.mem (γ := Set ℝ≥0) univ y →
          ∀ (hxy : x ≠ y) (a b : ℝ≥0) (ha : 0 < a) (hb : 0 < b) (hab : a + b = 1),
            (f : (a : ℝ≥0) → ℝ≥0) (a • x + b • y) <
              HSMul.hSMul (β := ℝ≥0) a ((f : (a : ℝ≥0) → ℝ≥0) x : ℝ≥0) +
                HSMul.hSMul (β := ℝ≥0) b ((f : (a : ℝ≥0) → ℝ≥0) y : ℝ≥0)
⊢ StrictConvexOn ℝ≥0 (E := ℝ≥0) (β := ℝ≥0) univ (⇑f : (a : ℝ≥0) → ℝ≥0)

Tactic:
refine ⟨convex_univ, fun x _ y _ hxy a b ha hb hab => ?_⟩
-- Module: Mathlib.Analysis.Convex.SpecificFunctions.Pow
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
h : Membership.mem (γ := Set ℝ≥0) univ x
y : ℝ≥0
h_1 : Membership.mem (γ := Set ℝ≥0) univ y
hxy : x ≠ y
a b : ℝ≥0
ha : 0 < a
hb : 0 < b
hab : a + b = 1
⊢ (↑x : ℝ) ≠ (↑y : ℝ)

Tactic:
simp [hxy]
-- Module: Mathlib.Analysis.Convex.SpecificFunctions.Pow
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
h : Membership.mem (γ := Set ℝ≥0) univ x
y : ℝ≥0
h_1 : Membership.mem (γ := Set ℝ≥0) univ y
hxy : x ≠ y
a b : ℝ≥0
ha : 0 < a
hb : 0 < b
hab norm_cast norm_cast₁ norm_cast₂ norm_cast₃ : a + b = 1
⊢ (↑a : ℝ) + (↑b : ℝ) = 1

Tactic:
norm_cast
-- Module: Mathlib.Analysis.Convex.SpecificFunctions.Pow
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
h : Membership.mem (γ := Set ℝ≥0) univ x
y : ℝ≥0
h_1 : Membership.mem (γ := Set ℝ≥0) univ y
hxy : x ≠ y
a b : ℝ≥0
ha : 0 < a
hb : 0 < b
hab : a + b = 1
⊢ (f : (a : ℝ≥0) → ℝ≥0) (a • x + b • y) <
    HSMul.hSMul (β := ℝ≥0) a ((f : (a : ℝ≥0) → ℝ≥0) x : ℝ≥0) + HSMul.hSMul (β := ℝ≥0) b ((f : (a : ℝ≥0) → ℝ≥0) y : ℝ≥0)

Tactic:
exact (strictConvexOn_rpow hp₁').2 x.2 y.2 (by simp [hxy]) ha hb (by simp; norm_cast)

Premises used: strictConvexOn_rpow, And.right, Subtype.property
-- Module: Mathlib.Analysis.Convex.SpecificFunctions.Pow
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 (E := ℝ≥0) (β := ℝ≥0) univ (⇑f : (a : ℝ≥0) → ℝ≥0)

Tactic:
have h₁ : StrictConvexOn ℝ≥0 univ f := by
    refine ⟨convex_univ, fun x _ y _ hxy a b ha hb hab => ?_⟩
    exact (strictConvexOn_rpow hp₁').2 x.2 y.2 (by simp [hxy]) ha hb (by simp; norm_cast)
-- Module: Mathlib.Analysis.Convex.SpecificFunctions.Pow
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 (E := ℝ≥0) (β := ℝ≥0) univ (⇑f : (a : ℝ≥0) → ℝ≥0)
⊢ ∀ (x : ℝ≥0), (f.symm : (a : ℝ≥0) → ℝ≥0) x = x ^ p

Tactic:
simp [f, NNReal.orderIsoRpow_symm_eq]

Premises used: NNReal.orderIsoRpow_symm_eq
-- Module: Mathlib.Analysis.Convex.SpecificFunctions.Pow
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 (E := ℝ≥0) (β := ℝ≥0) univ (⇑f : (a : ℝ≥0) → ℝ≥0)
⊢ ∀ (x : ℝ≥0), (f.symm : (a : ℝ≥0) → ℝ≥0) x = x ^ p

Tactic:
have h₂ : ∀ x, f.symm x = x ^ p := by simp [f, NNReal.orderIsoRpow_symm_eq]
-- Module: Mathlib.Analysis.Convex.SpecificFunctions.Pow
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 (E := ℝ≥0) (β := ℝ≥0) univ (⇑f : (a : ℝ≥0) → ℝ≥0)
h₂ : ∀ (x : ℝ≥0), (f.symm : (a : ℝ≥0) → ℝ≥0) x = x ^ p
⊢ StrictConcaveOn ℝ≥0 (β := ℝ≥0) univ fun (x : ℝ≥0) ↦ x ^ p

Tactic:
⟨convex_univ, fun x mx y my hxy a b ha hb hab => ?_⟩

Premises used: StrictConcaveOn, convex_univ, And.intro
-- Module: Mathlib.Analysis.Convex.SpecificFunctions.Pow
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 (E := ℝ≥0) (β := ℝ≥0) univ (⇑f : (a : ℝ≥0) → ℝ≥0)
h₂ : ∀ (x : ℝ≥0), (f.symm : (a : ℝ≥0) → ℝ≥0) x = x ^ p
refine :
  ∀ (x : ℝ≥0) (mx : Membership.mem (γ := Set ℝ≥0) univ x) (y : ℝ≥0) (my : Membership.mem (γ := Set ℝ≥0) univ y)
    (hxy : x ≠ y) (a b : ℝ≥0) (ha : 0 < a) (hb : 0 < b) (hab : a + b = 1),
    HSMul.hSMul (β := ℝ≥0) a ((fun (x : ℝ≥0) ↦ x ^ p) x) + HSMul.hSMul (β := ℝ≥0) b ((fun (x : ℝ≥0) ↦ x ^ p) y) <
      (fun (x : ℝ≥0) ↦ x ^ p) (a • x + b • y)
⊢ StrictConcaveOn ℝ≥0 (β := ℝ≥0) univ fun (x : ℝ≥0) ↦ x ^ p

Tactic:
refine ⟨convex_univ, fun x mx y my hxy a b ha hb hab => ?_⟩
-- Module: Mathlib.Analysis.Convex.SpecificFunctions.Pow
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 (E := ℝ≥0) (β := ℝ≥0) univ (⇑f : (a : ℝ≥0) → ℝ≥0)
h₂ : ∀ (x : ℝ≥0), (f.symm : (a : ℝ≥0) → ℝ≥0) x = x ^ p
x : ℝ≥0
mx : Membership.mem (γ := Set ℝ≥0) univ x
y : ℝ≥0
my : Membership.mem (γ := Set ℝ≥0) univ y
hxy : x ≠ y
a b : ℝ≥0
ha : 0 < a
hb : 0 < b
hab : a + b = 1
simp :
  HSMul.hSMul (β := ℝ≥0) a ((f.symm : (a : ℝ≥0) → ℝ≥0) x : ℝ≥0) +
      HSMul.hSMul (β := ℝ≥0) b ((f.symm : (a : ℝ≥0) → ℝ≥0) y : ℝ≥0) <
    (f.symm : (a : ℝ≥0) → ℝ≥0) (a • x + b • y)
⊢ HSMul.hSMul (β := ℝ≥0) a ((fun (x : ℝ≥0) ↦ x ^ p) x) + HSMul.hSMul (β := ℝ≥0) b ((fun (x : ℝ≥0) ↦ x ^ p) y) <
    (fun (x : ℝ≥0) ↦ x ^ p) (a • x + b • y)

Tactic:
simp only [← h₂]
-- Module: Mathlib.Analysis.Convex.SpecificFunctions.Pow
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 (E := ℝ≥0) (β := ℝ≥0) univ (⇑f : (a : ℝ≥0) → ℝ≥0)
h₂ : ∀ (x : ℝ≥0), (f.symm : (a : ℝ≥0) → ℝ≥0) x = x ^ p
x : ℝ≥0
mx : Membership.mem (γ := Set ℝ≥0) univ x
y : ℝ≥0
my : Membership.mem (γ := Set ℝ≥0) univ y
hxy : x ≠ y
a b : ℝ≥0
ha : 0 < a
hb : 0 < b
hab : a + b = 1
⊢ HSMul.hSMul (β := ℝ≥0) a ((f.symm : (a : ℝ≥0) → ℝ≥0) x : ℝ≥0) +
      HSMul.hSMul (β := ℝ≥0) b ((f.symm : (a : ℝ≥0) → ℝ≥0) y : ℝ≥0) <
    (f.symm : (a : ℝ≥0) → ℝ≥0) (a • x + b • y)

Tactic:
(f.strictConcaveOn_symm h₁).2 mx my hxy ha hb hab

Premises used: And.right, OrderIso.strictConcaveOn_symm
-- Module: Mathlib.Analysis.Convex.SpecificFunctions.Pow
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 (E := ℝ≥0) (β := ℝ≥0) univ (⇑f : (a : ℝ≥0) → ℝ≥0)
h₂ : ∀ (x : ℝ≥0), (f.symm : (a : ℝ≥0) → ℝ≥0) x = x ^ p
x : ℝ≥0
mx : Membership.mem (γ := Set ℝ≥0) univ x
y : ℝ≥0
my : Membership.mem (γ := Set ℝ≥0) univ y
hxy : x ≠ y
a b : ℝ≥0
ha : 0 < a
hb : 0 < b
hab : a + b = 1
⊢ HSMul.hSMul (β := ℝ≥0) a ((f.symm : (a : ℝ≥0) → ℝ≥0) x : ℝ≥0) +
      HSMul.hSMul (β := ℝ≥0) b ((f.symm : (a : ℝ≥0) → ℝ≥0) y : ℝ≥0) <
    (f.symm : (a : ℝ≥0) → ℝ≥0) (a • x + b • y)

Tactic:
exact (f.strictConcaveOn_symm h₁).2 mx my hxy ha hb hab

Premises used: And.right, OrderIso.strictConcaveOn_symm
-- Module: Mathlib.Analysis.Convex.SpecificFunctions.Pow
Goal:
p : ℝ
hp₀ : 0 ≤ p
hp₁ : p ≤ 1
inl :
  ∀ (hp₀ : LE.le (α := ℝ) 0 0) (hp₁ : LE.le (α := ℝ) 0 1),
    ConcaveOn ℝ≥0 (β := ℝ≥0) univ fun (x : ℝ≥0) ↦ HPow.hPow (β := ℝ) x 0
inr : ∀ (hp₀ : 0 < p), ConcaveOn ℝ≥0 (β := ℝ≥0) univ fun (x : ℝ≥0) ↦ x ^ p
⊢ ConcaveOn ℝ≥0 (β := ℝ≥0) univ fun (x : ℝ≥0) ↦ x ^ p

Tactic:
rcases eq_or_lt_of_le hp₀ with (rfl | hp₀)

Premises used: eq_or_lt_of_le, rfl
-- Module: Mathlib.Analysis.Convex.SpecificFunctions.Pow
Goal:
hp₀ : LE.le (α := ℝ) 0 0
hp₁ : LE.le (α := ℝ) 0 1
⊢ ConcaveOn ℝ≥0 (β := ℝ≥0) univ fun (x : ℝ≥0) ↦ HPow.hPow (β := ℝ) x 0

Tactic:
simpa only [rpow_zero] using concaveOn_const (c := 1) convex_univ

Premises used: convex_univ, NNReal.rpow_zero, OfNat.ofNat, concaveOn_const
-- Module: Mathlib.Analysis.Convex.SpecificFunctions.Pow
Goal:
p : ℝ
hp₀_1 : 0 ≤ p
hp₁ : p ≤ 1
hp₀ : 0 < p
inr :
  ∀ (hp₀ : LE.le (α := ℝ) 0 1) (hp₁ : LE.le (α := ℝ) 1 1) (hp₀ : LT.lt (α := ℝ) 0 1),
    ConcaveOn ℝ≥0 (β := ℝ≥0) univ fun (x : ℝ≥0) ↦ HPow.hPow (β := ℝ) x 1
inr₁ : ∀ (hp₁ : p < 1), ConcaveOn ℝ≥0 (β := ℝ≥0) univ fun (x : ℝ≥0) ↦ x ^ p
⊢ ConcaveOn ℝ≥0 (β := ℝ≥0) univ fun (x : ℝ≥0) ↦ x ^ p

Tactic:
rcases eq_or_lt_of_le hp₁ with (rfl | hp₁)

Premises used: eq_or_lt_of_le, rfl
-- Module: Mathlib.Analysis.Convex.SpecificFunctions.Pow
Goal:
hp₀_1 : LE.le (α := ℝ) 0 1
hp₁ : LE.le (α := ℝ) 1 1
hp₀ : LT.lt (α := ℝ) 0 1
⊢ ConcaveOn ℝ≥0 (β := ℝ≥0) univ fun (x : ℝ≥0) ↦ HPow.hPow (β := ℝ) x 1

Tactic:
simpa only [rpow_one] using concaveOn_id convex_univ

Premises used: concaveOn_id, convex_univ, NNReal.rpow_one
-- Module: Mathlib.Analysis.Convex.SpecificFunctions.Pow
Goal:
p : ℝ
hp₀_1 : 0 ≤ p
hp₁_1 : p ≤ 1
hp₀ : 0 < p
hp₁ : p < 1
⊢ ConcaveOn ℝ≥0 (β := ℝ≥0) univ fun (x : ℝ≥0) ↦ x ^ p

Tactic:
(strictConcaveOn_rpow hp₀ hp₁).concaveOn

Premises used: StrictConcaveOn.concaveOn, NNReal.strictConcaveOn_rpow
-- Module: Mathlib.Analysis.Convex.SpecificFunctions.Pow
Goal:
p : ℝ
hp₀_1 : 0 ≤ p
hp₁_1 : p ≤ 1
hp₀ : 0 < p
hp₁ : p < 1
⊢ ConcaveOn ℝ≥0 (β := ℝ≥0) univ fun (x : ℝ≥0) ↦ x ^ p

Tactic:
exact (strictConcaveOn_rpow hp₀ hp₁).concaveOn

Premises used: StrictConcaveOn.concaveOn, NNReal.strictConcaveOn_rpow
-- Module: Mathlib.Analysis.Convex.SpecificFunctions.Pow
Goal:
h : ∀ (x : ℝ≥0), (↑((sqrt : (a : ℝ≥0) → ℝ≥0) x) : ℝ) = (↑(x ^ (1 / 2)) : ℝ)
⊢ Eq (α := (a : ℝ≥0) → ℝ≥0) (⇑sqrt : (a : ℝ≥0) → ℝ≥0) fun (x : ℝ≥0) ↦ x ^ (1 / 2)

Tactic:
ext x
-- Module: Mathlib.Analysis.Convex.SpecificFunctions.Pow
Goal:
x : ℝ≥0
⊢ (↑((sqrt : (a : ℝ≥0) → ℝ≥0) x) : ℝ) = (↑(x ^ (1 / 2)) : ℝ)

Tactic:
mod_cast NNReal.sqrt_eq_rpow x

Premises used: NNReal.sqrt_eq_rpow, congrArg, cast, HDiv.hDiv, Nat.cast, NNReal.sqrt, HPow.hPow, congrFun', NNReal.coe_inj._simp_1, OfNat.ofNat, Eq.symm, Eq, Nat.cast_one, DFunLike.coe, NNReal.toReal, Eq.trans
-- Module: Mathlib.Analysis.Convex.SpecificFunctions.Pow
Goal:
x : ℝ≥0
⊢ (↑((sqrt : (a : ℝ≥0) → ℝ≥0) x) : ℝ) = (↑(x ^ (1 / 2)) : ℝ)

Tactic:
exact mod_cast NNReal.sqrt_eq_rpow x

Premises used: NNReal.sqrt_eq_rpow
-- Module: Mathlib.Analysis.Convex.SpecificFunctions.Pow
Goal:
⊢ Eq (α := (a : ℝ≥0) → ℝ≥0) (⇑sqrt : (a : ℝ≥0) → ℝ≥0) fun (x : ℝ≥0) ↦ x ^ (1 / 2)

Tactic:
have : NNReal.sqrt = fun x : ℝ≥0 ↦ x ^ (1 / (2 : ℝ)) := by
    ext x; exact mod_cast NNReal.sqrt_eq_rpow x
-- Module: Mathlib.Analysis.Convex.SpecificFunctions.Pow
Goal:
this : Eq (α := (a : ℝ≥0) → ℝ≥0) (⇑sqrt : (a : ℝ≥0) → ℝ≥0) fun (x : ℝ≥0) ↦ x ^ (1 / 2)
rw : StrictConcaveOn ℝ≥0 (β := ℝ≥0) univ fun (x : ℝ≥0) ↦ x ^ (1 / 2)
⊢ StrictConcaveOn ℝ≥0 (E := ℝ≥0) (β := ℝ≥0) univ (⇑sqrt : (a : ℝ≥0) → ℝ≥0)

Tactic:
rw [this]
-- Module: Mathlib.Analysis.Convex.SpecificFunctions.Pow
Goal:
this : Eq (α := (a : ℝ≥0) → ℝ≥0) (⇑sqrt : (a : ℝ≥0) → ℝ≥0) fun (x : ℝ≥0) ↦ x ^ (1 / 2)
⊢ 0 < 1 / 2

Tactic:
positivity
-- Module: Mathlib.Analysis.Convex.SpecificFunctions.Pow
Goal:
this : Eq (α := (a : ℝ≥0) → ℝ≥0) (⇑sqrt : (a : ℝ≥0) → ℝ≥0) fun (x : ℝ≥0) ↦ x ^ (1 / 2)
linarith : 1 ≤ 1 / 2 → 2 / 2 = 1
linarith₁ : 1 ≤ 1 / 2 → HMul.hMul (α := ℝ) 1 2 = 2
linarith₂ : 1 ≤ 1 / 2 → GT.gt (α := ℝ) 2 0
linarith₃ : 1 ≤ 1 / 2 → -1 + HMul.hMul (α := ℝ) 1 1 = 0
⊢ 1 / 2 < 1

Tactic:
linarith
-- Module: Mathlib.Analysis.Convex.SpecificFunctions.Pow
Goal:
this : Eq (α := (a : ℝ≥0) → ℝ≥0) (⇑sqrt : (a : ℝ≥0) → ℝ≥0) fun (x : ℝ≥0) ↦ x ^ (1 / 2)
⊢ StrictConcaveOn ℝ≥0 (β := ℝ≥0) univ fun (x : ℝ≥0) ↦ x ^ (1 / 2)

Tactic:
exact strictConcaveOn_rpow (by positivity) (by linarith)

Premises used: NNReal.strictConcaveOn_rpow
-- Module: Mathlib.Analysis.Convex.SpecificFunctions.Pow
Goal:
p : ℝ
hp₀ : 0 < p
hp₁ : p < 1
⊢ StrictConcaveOn ℝ (β := ℝ) (Ici 0) fun (x : ℝ) ↦ x ^ p

Tactic:
⟨convex_Ici _, fun x hx y hy hxy a b ha hb hab => ?_⟩

Premises used: StrictConcaveOn, And.intro, convex_Ici
-- Module: Mathlib.Analysis.Convex.SpecificFunctions.Pow
Goal:
p : ℝ
hp₀ : 0 < p
hp₁ : p < 1
refine :
  ∀ (x : ℝ) (hx : Membership.mem (γ := Set ℝ) (Ici 0) x) (y : ℝ) (hy : Membership.mem (γ := Set ℝ) (Ici 0) y)
    (hxy : x ≠ y) (a b : ℝ) (ha : 0 < a) (hb : 0 < b) (hab : a + b = 1),
    HSMul.hSMul (β := ℝ) a ((fun (x : ℝ) ↦ x ^ p) x) + HSMul.hSMul (β := ℝ) b ((fun (x : ℝ) ↦ x ^ p) y) <
      (fun (x : ℝ) ↦ x ^ p) (a • x + b • y)
⊢ StrictConcaveOn ℝ (β := ℝ) (Ici 0) fun (x : ℝ) ↦ x ^ p

Tactic:
refine ⟨convex_Ici _, fun x hx y hy hxy a b ha hb hab => ?_⟩
-- Module: Mathlib.Analysis.Convex.SpecificFunctions.Pow
Goal:
p : ℝ
hp₀ : 0 < p
hp₁ : p < 1
x : ℝ
hx : Membership.mem (γ := Set ℝ) (Ici 0) x
y : ℝ
hy : Membership.mem (γ := Set ℝ) (Ici 0) y
hxy : x ≠ y
a b : ℝ
ha : 0 < a
hb : 0 < b
hab : a + b = 1
x' : ℝ≥0 := NNReal.mk x hx
y' : ℝ≥0 := NNReal.mk y hy
a' : ℝ≥0 := NNReal.mk a ⋯
b' : ℝ≥0 := NNReal.mk b ⋯
⊢ x' ≠ y'

Tactic:
have hxy' : x' ≠ y' := Subtype.coe_ne_coe.1 hxy
-- Module: Mathlib.Analysis.Convex.SpecificFunctions.Pow
Goal:
p : ℝ
hp₀ : 0 < p
hp₁ : p < 1
x : ℝ
hx : Membership.mem (γ := Set ℝ) (Ici 0) x
y : ℝ
hy : Membership.mem (γ := Set ℝ) (Ici 0) y
hxy : x ≠ y
a b : ℝ
ha : 0 < a
hb : 0 < b
hab : a + b = 1
x' : ℝ≥0 := NNReal.mk x hx
y' : ℝ≥0 := NNReal.mk y hy
a' : ℝ≥0 := NNReal.mk a ⋯
b' : ℝ≥0 := NNReal.mk b ⋯
hxy' : x' ≠ y'
a₁ : (↑(a' + b') : ℝ) = (↑1 : ℝ)
⊢ a' + b' = 1

Tactic:
ext
-- Module: Mathlib.Analysis.Convex.SpecificFunctions.Pow
Goal:
p : ℝ
hp₀ : 0 < p
hp₁ : p < 1
x : ℝ
hx : Membership.mem (γ := Set ℝ) (Ici 0) x
y : ℝ
hy : Membership.mem (γ := Set ℝ) (Ici 0) y
hxy : x ≠ y
a b : ℝ
ha : 0 < a
hb : 0 < b
hab : a + b = 1
x' : ℝ≥0 := NNReal.mk x hx
y' : ℝ≥0 := NNReal.mk y hy
a' : ℝ≥0 := NNReal.mk a ⋯
b' : ℝ≥0 := NNReal.mk b ⋯
hxy' : x' ≠ y'
⊢ (↑(a' + b') : ℝ) = (↑1 : ℝ)

Tactic:
simp [a', b', hab]
-- Module: Mathlib.Analysis.Convex.SpecificFunctions.Pow
Goal:
p : ℝ
hp₀ : 0 < p
hp₁ : p < 1
x : ℝ
hx : Membership.mem (γ := Set ℝ) (Ici 0) x
y : ℝ
hy : Membership.mem (γ := Set ℝ) (Ici 0) y
hxy : x ≠ y
a b : ℝ
ha : 0 < a
hb : 0 < b
hab : a + b = 1
x' : ℝ≥0 := NNReal.mk x hx
y' : ℝ≥0 := NNReal.mk y hy
a' : ℝ≥0 := NNReal.mk a ⋯
b' : ℝ≥0 := NNReal.mk b ⋯
hxy' : x' ≠ y'
⊢ a' + b' = 1

Tactic:
have hab' : a' + b' = 1 := by ext; simp [a', b', hab]
-- Module: Mathlib.Analysis.Convex.SpecificFunctions.Pow
Goal:
p : ℝ
hp₀ : 0 < p
hp₁ : p < 1
x : ℝ
hx : Membership.mem (γ := Set ℝ) (Ici 0) x
y : ℝ
hy : Membership.mem (γ := Set ℝ) (Ici 0) y
hxy : x ≠ y
a b : ℝ
ha : 0 < a
hb : 0 < b
hab : a + b = 1
x' : ℝ≥0 := NNReal.mk x hx
y' : ℝ≥0 := NNReal.mk y hy
a' : ℝ≥0 := NNReal.mk a ⋯
b' : ℝ≥0 := NNReal.mk b ⋯
hxy' : x' ≠ y'
hab' : a' + b' = 1
⊢ HSMul.hSMul (β := ℝ) a ((fun (x : ℝ) ↦ x ^ p) x) + HSMul.hSMul (β := ℝ) b ((fun (x : ℝ) ↦ x ^ p) y) <
    (fun (x : ℝ) ↦ x ^ p) (a • x + b • y)

Tactic:
exact_mod_cast (NNReal.strictConcaveOn_rpow hp₀ hp₁).2 (Set.mem_univ x') (Set.mem_univ y')
    hxy' (mod_cast ha) (mod_cast hb) hab'

Premises used: And.right, Set.mem_univ, NNReal.strictConcaveOn_rpow
-- Module: Mathlib.Analysis.Convex.SpecificFunctions.Pow
Goal:
p : ℝ
hp₀ : 0 ≤ p
hp₁ : p ≤ 1
inl :
  ∀ (hp₀ : LE.le (α := ℝ) 0 0) (hp₁ : LE.le (α := ℝ) 0 1),
    ConcaveOn ℝ (β := ℝ) (Ici 0) fun (x : ℝ) ↦ HPow.hPow (β := ℝ) x 0
inr : ∀ (hp₀ : 0 < p), ConcaveOn ℝ (β := ℝ) (Ici 0) fun (x : ℝ) ↦ x ^ p
⊢ ConcaveOn ℝ (β := ℝ) (Ici 0) fun (x : ℝ) ↦ x ^ p

Tactic:
rcases eq_or_lt_of_le hp₀ with (rfl | hp₀)

Premises used: eq_or_lt_of_le, rfl
-- Module: Mathlib.Analysis.Convex.SpecificFunctions.Pow
Goal:
hp₀ : LE.le (α := ℝ) 0 0
hp₁ : LE.le (α := ℝ) 0 1
⊢ ConcaveOn ℝ (β := ℝ) (Ici 0) fun (x : ℝ) ↦ HPow.hPow (β := ℝ) x 0

Tactic:
simpa only [rpow_zero] using concaveOn_const (c := 1) (convex_Ici _)

Premises used: Real.rpow_zero, convex_Ici, OfNat.ofNat, concaveOn_const
-- Module: Mathlib.Analysis.Convex.SpecificFunctions.Pow
Goal:
p : ℝ
hp₀_1 : 0 ≤ p
hp₁ : p ≤ 1
hp₀ : 0 < p
inr :
  ∀ (hp₀ : LE.le (α := ℝ) 0 1) (hp₁ : LE.le (α := ℝ) 1 1) (hp₀ : LT.lt (α := ℝ) 0 1),
    ConcaveOn ℝ (β := ℝ) (Ici 0) fun (x : ℝ) ↦ HPow.hPow (β := ℝ) x 1
inr₁ : ∀ (hp₁ : p < 1), ConcaveOn ℝ (β := ℝ) (Ici 0) fun (x : ℝ) ↦ x ^ p
⊢ ConcaveOn ℝ (β := ℝ) (Ici 0) fun (x : ℝ) ↦ x ^ p

Tactic:
rcases eq_or_lt_of_le hp₁ with (rfl | hp₁)

Premises used: eq_or_lt_of_le, rfl
-- Module: Mathlib.Analysis.Convex.SpecificFunctions.Pow
Goal:
hp₀_1 : LE.le (α := ℝ) 0 1
hp₁ : LE.le (α := ℝ) 1 1
hp₀ : LT.lt (α := ℝ) 0 1
⊢ ConcaveOn ℝ (β := ℝ) (Ici 0) fun (x : ℝ) ↦ HPow.hPow (β := ℝ) x 1

Tactic:
simpa only [rpow_one] using concaveOn_id (convex_Ici _)

Premises used: concaveOn_id, Real.rpow_one, convex_Ici
-- Module: Mathlib.Analysis.Convex.SpecificFunctions.Pow
Goal:
p : ℝ
hp₀_1 : 0 ≤ p
hp₁_1 : p ≤ 1
hp₀ : 0 < p
hp₁ : p < 1
⊢ ConcaveOn ℝ (β := ℝ) (Ici 0) fun (x : ℝ) ↦ x ^ p

Tactic:
(strictConcaveOn_rpow hp₀ hp₁).concaveOn

Premises used: Real.strictConcaveOn_rpow, StrictConcaveOn.concaveOn
-- Module: Mathlib.Analysis.Convex.SpecificFunctions.Pow
Goal:
p : ℝ
hp₀_1 : 0 ≤ p
hp₁_1 : p ≤ 1
hp₀ : 0 < p
hp₁ : p < 1
⊢ ConcaveOn ℝ (β := ℝ) (Ici 0) fun (x : ℝ) ↦ x ^ p

Tactic:
exact (strictConcaveOn_rpow hp₀ hp₁).concaveOn

Premises used: Real.strictConcaveOn_rpow, StrictConcaveOn.concaveOn
-- Module: Mathlib.Analysis.Convex.SpecificFunctions.Pow
Goal:
rw : StrictConcaveOn ℝ (β := ℝ) (Ici 0) fun (x : ℝ) ↦ (fun (x : ℝ) ↦ x ^ (1 / 2)) x
⊢ StrictConcaveOn ℝ (β := ℝ) (Ici 0) fun (x : ℝ) ↦ √x

Tactic:
rw [funext Real.sqrt_eq_rpow]

Premises used: funext, Real.sqrt_eq_rpow
-- Module: Mathlib.Analysis.Convex.SpecificFunctions.Pow
Goal:
⊢ 0 < 1 / 2

Tactic:
positivity
-- Module: Mathlib.Analysis.Convex.SpecificFunctions.Pow
Goal:
linarith : 1 ≤ 1 / 2 → 2 / 2 = 1
linarith₁ : 1 ≤ 1 / 2 → HMul.hMul (α := ℝ) 1 2 = 2
linarith₂ : 1 ≤ 1 / 2 → GT.gt (α := ℝ) 2 0
linarith₃ : 1 ≤ 1 / 2 → -1 + HMul.hMul (α := ℝ) 1 1 = 0
⊢ 1 / 2 < 1

Tactic:
linarith
-- Module: Mathlib.Analysis.Convex.SpecificFunctions.Pow
Goal:
⊢ StrictConcaveOn ℝ (β := ℝ) (Ici 0) fun (x : ℝ) ↦ (fun (x : ℝ) ↦ x ^ (1 / 2)) x

Tactic:
exact strictConcaveOn_rpow (by positivity) (by linarith)

Premises used: Real.strictConcaveOn_rpow
-- Module: Mathlib.Analysis.Convex.Star
Goal:
𝕜 : Type u_1
E : Type u_2
inst : Semiring 𝕜
inst_1 : PartialOrder 𝕜
inst_2 : AddCommMonoid E
inst_3 : SMul 𝕜 E
x : E
s : Set E
mp : StarConvex 𝕜 x s → ∀ ⦃y : E⦄, y ∈ s → [x -[𝕜] y] ⊆ s
mpr : (∀ ⦃y : E⦄, y ∈ s → [x -[𝕜] y] ⊆ s) → StarConvex 𝕜 x s
⊢ StarConvex 𝕜 x s ↔ ∀ ⦃y : E⦄, y ∈ s → [x -[𝕜] y] ⊆ s

Tactic:
constructor
-- Module: Mathlib.Analysis.Convex.Star
Goal:
𝕜 : Type u_1
E : Type u_2
inst : Semiring 𝕜
inst_1 : PartialOrder 𝕜
inst_2 : AddCommMonoid E
inst_3 : SMul 𝕜 E
x : E
s : Set E
h : StarConvex 𝕜 x s
y : E
hy : y ∈ s
a b : 𝕜
ha : 0 ≤ a
hb : 0 ≤ b
hab : a + b = 1
⊢ a • x + b • y ∈ s

Tactic:
h hy ha hb hab