Documentation
Carleson
.
ToMathlib
.
Analysis
.
Convex
.
SpecificFunctions
.
Basic
Search
return to top
source
Imports
Init
Mathlib.Analysis.Convex.SpecificFunctions.Basic
Imported by
ConvexOn_rpow_left
source
theorem
ConvexOn_rpow_left
(
b
:
ℝ
)
(
hb
:
0
<
b
)
:
ConvexOn
ℝ
Set.univ
fun (
x
:
ℝ
) =>
b
^
x