@[simp]

theorem StieltjesFunction.measure_zero : StieltjesFunction.measure 0 = 0

theorem StieltjesFunction.measure_Iio (f : StieltjesFunction) {l : ℝ} (hf : Filter.Tendsto (↑f) Filter.atBot (nhds l)) (x : ℝ) : f.measure (Set.Iio x) = ENNReal.ofReal (Function.leftLim (↑f) x - l)

theorem StieltjesFunction.measure_Ioi (f : StieltjesFunction) {l : ℝ} (hf : Filter.Tendsto (↑f) Filter.atTop (nhds l)) (x : ℝ) : f.measure (Set.Ioi x) = ENNReal.ofReal (l - ↑f x)

theorem StieltjesFunction.measure_Ioi_of_tendsto_atTop_atTop (f : StieltjesFunction) (hf : Filter.Tendsto (↑f) Filter.atTop Filter.atTop) (x : ℝ) : f.measure (Set.Ioi x) = ⊤

theorem StieltjesFunction.measure_Ici_of_tendsto_atTop_atTop (f : StieltjesFunction) (hf : Filter.Tendsto (↑f) Filter.atTop Filter.atTop) (x : ℝ) : f.measure (Set.Ici x) = ⊤

theorem StieltjesFunction.measure_Iic_of_tendsto_atBot_atBot (f : StieltjesFunction) (hf : Filter.Tendsto (↑f) Filter.atBot Filter.atBot) (x : ℝ) : f.measure (Set.Iic x) = ⊤

theorem StieltjesFunction.measure_Iio_of_tendsto_atBot_atBot (f : StieltjesFunction) (hf : Filter.Tendsto (↑f) Filter.atBot Filter.atBot) (x : ℝ) : f.measure (Set.Iio x) = ⊤

theorem StieltjesFunction.measure_univ_of_tendsto_atTop_atTop (f : StieltjesFunction) (hf : Filter.Tendsto (↑f) Filter.atTop Filter.atTop) : f.measure Set.univ = ⊤

theorem StieltjesFunction.measure_univ_of_tendsto_atBot_atBot (f : StieltjesFunction) (hf : Filter.Tendsto (↑f) Filter.atBot Filter.atBot) : f.measure Set.univ = ⊤

@[irreducible]

noncomputable def ConvexOn.curvatureMeasure (f : ℝ → ℝ) : MeasureTheory.Measure ℝ

The curvature measure induced by a convex function. It is defined as the only measure that has the right derivative of the function as a CDF. For nonconvex functions it is defined as the zero measure.

Equations

• ConvexOn.curvatureMeasure = ConvexOn.wrapped✝.1

theorem ConvexOn.curvatureMeasure_def (f : ℝ → ℝ) : ConvexOn.curvatureMeasure f = if hf : ConvexOn ℝ Set.univ f then hf.rightDerivStieltjes.measure else 0

theorem ConvexOn.curvatureMeasure_of_convexOn {f : ℝ → ℝ} (hf : ConvexOn ℝ Set.univ f) : ConvexOn.curvatureMeasure f = hf.rightDerivStieltjes.measure

theorem ConvexOn.curvatureMeasure_of_not_convexOn {f : ℝ → ℝ} (hf : ¬ConvexOn ℝ Set.univ f) : ConvexOn.curvatureMeasure f = 0

instance ConvexOn.instIsLocallyFiniteMeasureRealCurvatureMeasure {f : ℝ → ℝ} : MeasureTheory.IsLocallyFiniteMeasure (ConvexOn.curvatureMeasure f)

Equations

• ⋯ = ⋯

@[simp]

theorem ConvexOn.curvatureMeasure_const (c : ℝ) : (ConvexOn.curvatureMeasure fun (x : ℝ) => c) = 0

@[simp]

theorem ConvexOn.curvatureMeasure_linear (a : ℝ) : (ConvexOn.curvatureMeasure fun (x : ℝ) => a * x) = 0

theorem ConvexOn.curvatureMeasure_add {f : ℝ → ℝ} {g : ℝ → ℝ} (hf : ConvexOn ℝ Set.univ f) (hg : ConvexOn ℝ Set.univ g) : ConvexOn.curvatureMeasure (f + g) = ConvexOn.curvatureMeasure f + ConvexOn.curvatureMeasure g

@[simp]

theorem ConvexOn.curvatureMeasure_add_const {f : ℝ → ℝ} (c : ℝ) : (ConvexOn.curvatureMeasure fun (x : ℝ) => f x + c) = ConvexOn.curvatureMeasure f

@[simp]

theorem ConvexOn.curvatureMeasure_add_linear {f : ℝ → ℝ} (a : ℝ) : (ConvexOn.curvatureMeasure fun (x : ℝ) => f x + a * x) = ConvexOn.curvatureMeasure f

theorem ConvexOn.convex_taylor {f : ℝ → ℝ} (hf : ConvexOn ℝ Set.univ f) (hf_cont : Continuous f) {a : ℝ} {b : ℝ} : f b - f a - rightDeriv f a * (b - a) = ∫ (x : ℝ) in a..b, b - x ∂ConvexOn.curvatureMeasure f

A Taylor formula for convex functions in terms of the right derivative and the curvature measure.