Documentation

Mathlib.Analysis.Convex.Mul

Product of convex functions #

This file proves that the product of convex functions is convex, provided they monovary.

As corollaries, we also prove that x ↦ x ^ n is convex

theorem ConvexOn.smul' {𝕜 : Type u_1} {E : Type u_2} {F : Type u_3} [LinearOrderedCommRing 𝕜] [LinearOrderedCommRing E] [LinearOrderedAddCommGroup F] [Module 𝕜 E] [Module 𝕜 F] [Module E F] [IsScalarTower 𝕜 E F] [SMulCommClass 𝕜 E F] [OrderedSMul 𝕜 F] [OrderedSMul E F] {s : Set 𝕜} {f : 𝕜E} {g : 𝕜F} (hf : ConvexOn 𝕜 s f) (hg : ConvexOn 𝕜 s g) (hf₀ : ∀ ⦃x : 𝕜⦄, x s0 f x) (hg₀ : ∀ ⦃x : 𝕜⦄, x s0 g x) (hfg : MonovaryOn f g s) :
ConvexOn 𝕜 s (f g)
theorem ConcaveOn.smul' {𝕜 : Type u_1} {E : Type u_2} {F : Type u_3} [LinearOrderedCommRing 𝕜] [LinearOrderedCommRing E] [LinearOrderedAddCommGroup F] [Module 𝕜 E] [Module 𝕜 F] [Module E F] [IsScalarTower 𝕜 E F] [SMulCommClass 𝕜 E F] [OrderedSMul 𝕜 F] [OrderedSMul E F] {s : Set 𝕜} {f : 𝕜E} {g : 𝕜F} [OrderedSMul 𝕜 E] (hf : ConcaveOn 𝕜 s f) (hg : ConcaveOn 𝕜 s g) (hf₀ : ∀ ⦃x : 𝕜⦄, x s0 f x) (hg₀ : ∀ ⦃x : 𝕜⦄, x s0 g x) (hfg : AntivaryOn f g s) :
ConcaveOn 𝕜 s (f g)
theorem ConvexOn.smul'' {𝕜 : Type u_1} {E : Type u_2} {F : Type u_3} [LinearOrderedCommRing 𝕜] [LinearOrderedCommRing E] [LinearOrderedAddCommGroup F] [Module 𝕜 E] [Module 𝕜 F] [Module E F] [IsScalarTower 𝕜 E F] [SMulCommClass 𝕜 E F] [OrderedSMul 𝕜 F] [OrderedSMul E F] {s : Set 𝕜} {f : 𝕜E} {g : 𝕜F} [OrderedSMul 𝕜 E] (hf : ConvexOn 𝕜 s f) (hg : ConvexOn 𝕜 s g) (hf₀ : ∀ ⦃x : 𝕜⦄, x sf x 0) (hg₀ : ∀ ⦃x : 𝕜⦄, x sg x 0) (hfg : AntivaryOn f g s) :
ConcaveOn 𝕜 s (f g)
theorem ConcaveOn.smul'' {𝕜 : Type u_1} {E : Type u_2} {F : Type u_3} [LinearOrderedCommRing 𝕜] [LinearOrderedCommRing E] [LinearOrderedAddCommGroup F] [Module 𝕜 E] [Module 𝕜 F] [Module E F] [IsScalarTower 𝕜 E F] [SMulCommClass 𝕜 E F] [OrderedSMul 𝕜 F] [OrderedSMul E F] {s : Set 𝕜} {f : 𝕜E} {g : 𝕜F} (hf : ConcaveOn 𝕜 s f) (hg : ConcaveOn 𝕜 s g) (hf₀ : ∀ ⦃x : 𝕜⦄, x sf x 0) (hg₀ : ∀ ⦃x : 𝕜⦄, x sg x 0) (hfg : MonovaryOn f g s) :
ConvexOn 𝕜 s (f g)
theorem ConvexOn.smul_concaveOn {𝕜 : Type u_1} {E : Type u_2} {F : Type u_3} [LinearOrderedCommRing 𝕜] [LinearOrderedCommRing E] [LinearOrderedAddCommGroup F] [Module 𝕜 E] [Module 𝕜 F] [Module E F] [IsScalarTower 𝕜 E F] [SMulCommClass 𝕜 E F] [OrderedSMul 𝕜 F] [OrderedSMul E F] {s : Set 𝕜} {f : 𝕜E} {g : 𝕜F} (hf : ConvexOn 𝕜 s f) (hg : ConcaveOn 𝕜 s g) (hf₀ : ∀ ⦃x : 𝕜⦄, x s0 f x) (hg₀ : ∀ ⦃x : 𝕜⦄, x sg x 0) (hfg : AntivaryOn f g s) :
ConcaveOn 𝕜 s (f g)
theorem ConcaveOn.smul_convexOn {𝕜 : Type u_1} {E : Type u_2} {F : Type u_3} [LinearOrderedCommRing 𝕜] [LinearOrderedCommRing E] [LinearOrderedAddCommGroup F] [Module 𝕜 E] [Module 𝕜 F] [Module E F] [IsScalarTower 𝕜 E F] [SMulCommClass 𝕜 E F] [OrderedSMul 𝕜 F] [OrderedSMul E F] {s : Set 𝕜} {f : 𝕜E} {g : 𝕜F} [OrderedSMul 𝕜 E] (hf : ConcaveOn 𝕜 s f) (hg : ConvexOn 𝕜 s g) (hf₀ : ∀ ⦃x : 𝕜⦄, x s0 f x) (hg₀ : ∀ ⦃x : 𝕜⦄, x sg x 0) (hfg : MonovaryOn f g s) :
ConvexOn 𝕜 s (f g)
theorem ConvexOn.smul_concaveOn' {𝕜 : Type u_1} {E : Type u_2} {F : Type u_3} [LinearOrderedCommRing 𝕜] [LinearOrderedCommRing E] [LinearOrderedAddCommGroup F] [Module 𝕜 E] [Module 𝕜 F] [Module E F] [IsScalarTower 𝕜 E F] [SMulCommClass 𝕜 E F] [OrderedSMul 𝕜 F] [OrderedSMul E F] {s : Set 𝕜} {f : 𝕜E} {g : 𝕜F} [OrderedSMul 𝕜 E] (hf : ConvexOn 𝕜 s f) (hg : ConcaveOn 𝕜 s g) (hf₀ : ∀ ⦃x : 𝕜⦄, x sf x 0) (hg₀ : ∀ ⦃x : 𝕜⦄, x s0 g x) (hfg : MonovaryOn f g s) :
ConvexOn 𝕜 s (f g)
theorem ConcaveOn.smul_convexOn' {𝕜 : Type u_1} {E : Type u_2} {F : Type u_3} [LinearOrderedCommRing 𝕜] [LinearOrderedCommRing E] [LinearOrderedAddCommGroup F] [Module 𝕜 E] [Module 𝕜 F] [Module E F] [IsScalarTower 𝕜 E F] [SMulCommClass 𝕜 E F] [OrderedSMul 𝕜 F] [OrderedSMul E F] {s : Set 𝕜} {f : 𝕜E} {g : 𝕜F} (hf : ConcaveOn 𝕜 s f) (hg : ConvexOn 𝕜 s g) (hf₀ : ∀ ⦃x : 𝕜⦄, x sf x 0) (hg₀ : ∀ ⦃x : 𝕜⦄, x s0 g x) (hfg : AntivaryOn f g s) :
ConcaveOn 𝕜 s (f g)
theorem ConvexOn.mul {𝕜 : Type u_1} {E : Type u_2} [LinearOrderedCommRing 𝕜] [LinearOrderedCommRing E] [Module 𝕜 E] {s : Set 𝕜} [OrderedSMul 𝕜 E] [IsScalarTower 𝕜 E E] [SMulCommClass 𝕜 E E] {f : 𝕜E} {g : 𝕜E} (hf : ConvexOn 𝕜 s f) (hg : ConvexOn 𝕜 s g) (hf₀ : ∀ ⦃x : 𝕜⦄, x s0 f x) (hg₀ : ∀ ⦃x : 𝕜⦄, x s0 g x) (hfg : MonovaryOn f g s) :
ConvexOn 𝕜 s (f * g)
theorem ConcaveOn.mul {𝕜 : Type u_1} {E : Type u_2} [LinearOrderedCommRing 𝕜] [LinearOrderedCommRing E] [Module 𝕜 E] {s : Set 𝕜} [OrderedSMul 𝕜 E] [IsScalarTower 𝕜 E E] [SMulCommClass 𝕜 E E] {f : 𝕜E} {g : 𝕜E} (hf : ConcaveOn 𝕜 s f) (hg : ConcaveOn 𝕜 s g) (hf₀ : ∀ ⦃x : 𝕜⦄, x s0 f x) (hg₀ : ∀ ⦃x : 𝕜⦄, x s0 g x) (hfg : AntivaryOn f g s) :
ConcaveOn 𝕜 s (f * g)
theorem ConvexOn.mul' {𝕜 : Type u_1} {E : Type u_2} [LinearOrderedCommRing 𝕜] [LinearOrderedCommRing E] [Module 𝕜 E] {s : Set 𝕜} [OrderedSMul 𝕜 E] [IsScalarTower 𝕜 E E] [SMulCommClass 𝕜 E E] {f : 𝕜E} {g : 𝕜E} (hf : ConvexOn 𝕜 s f) (hg : ConvexOn 𝕜 s g) (hf₀ : ∀ ⦃x : 𝕜⦄, x sf x 0) (hg₀ : ∀ ⦃x : 𝕜⦄, x sg x 0) (hfg : AntivaryOn f g s) :
ConcaveOn 𝕜 s (f * g)
theorem ConcaveOn.mul' {𝕜 : Type u_1} {E : Type u_2} [LinearOrderedCommRing 𝕜] [LinearOrderedCommRing E] [Module 𝕜 E] {s : Set 𝕜} [OrderedSMul 𝕜 E] [IsScalarTower 𝕜 E E] [SMulCommClass 𝕜 E E] {f : 𝕜E} {g : 𝕜E} (hf : ConcaveOn 𝕜 s f) (hg : ConcaveOn 𝕜 s g) (hf₀ : ∀ ⦃x : 𝕜⦄, x sf x 0) (hg₀ : ∀ ⦃x : 𝕜⦄, x sg x 0) (hfg : MonovaryOn f g s) :
ConvexOn 𝕜 s (f * g)
theorem ConvexOn.mul_concaveOn {𝕜 : Type u_1} {E : Type u_2} [LinearOrderedCommRing 𝕜] [LinearOrderedCommRing E] [Module 𝕜 E] {s : Set 𝕜} [OrderedSMul 𝕜 E] [IsScalarTower 𝕜 E E] [SMulCommClass 𝕜 E E] {f : 𝕜E} {g : 𝕜E} (hf : ConvexOn 𝕜 s f) (hg : ConcaveOn 𝕜 s g) (hf₀ : ∀ ⦃x : 𝕜⦄, x s0 f x) (hg₀ : ∀ ⦃x : 𝕜⦄, x sg x 0) (hfg : AntivaryOn f g s) :
ConcaveOn 𝕜 s (f * g)
theorem ConcaveOn.mul_convexOn {𝕜 : Type u_1} {E : Type u_2} [LinearOrderedCommRing 𝕜] [LinearOrderedCommRing E] [Module 𝕜 E] {s : Set 𝕜} [OrderedSMul 𝕜 E] [IsScalarTower 𝕜 E E] [SMulCommClass 𝕜 E E] {f : 𝕜E} {g : 𝕜E} (hf : ConcaveOn 𝕜 s f) (hg : ConvexOn 𝕜 s g) (hf₀ : ∀ ⦃x : 𝕜⦄, x s0 f x) (hg₀ : ∀ ⦃x : 𝕜⦄, x sg x 0) (hfg : MonovaryOn f g s) :
ConvexOn 𝕜 s (f * g)
theorem ConvexOn.mul_concaveOn' {𝕜 : Type u_1} {E : Type u_2} [LinearOrderedCommRing 𝕜] [LinearOrderedCommRing E] [Module 𝕜 E] {s : Set 𝕜} [OrderedSMul 𝕜 E] [IsScalarTower 𝕜 E E] [SMulCommClass 𝕜 E E] {f : 𝕜E} {g : 𝕜E} (hf : ConvexOn 𝕜 s f) (hg : ConcaveOn 𝕜 s g) (hf₀ : ∀ ⦃x : 𝕜⦄, x sf x 0) (hg₀ : ∀ ⦃x : 𝕜⦄, x s0 g x) (hfg : MonovaryOn f g s) :
ConvexOn 𝕜 s (f * g)
theorem ConcaveOn.mul_convexOn' {𝕜 : Type u_1} {E : Type u_2} [LinearOrderedCommRing 𝕜] [LinearOrderedCommRing E] [Module 𝕜 E] {s : Set 𝕜} [OrderedSMul 𝕜 E] [IsScalarTower 𝕜 E E] [SMulCommClass 𝕜 E E] {f : 𝕜E} {g : 𝕜E} (hf : ConcaveOn 𝕜 s f) (hg : ConvexOn 𝕜 s g) (hf₀ : ∀ ⦃x : 𝕜⦄, x sf x 0) (hg₀ : ∀ ⦃x : 𝕜⦄, x s0 g x) (hfg : AntivaryOn f g s) :
ConcaveOn 𝕜 s (f g)
theorem ConvexOn.pow {𝕜 : Type u_1} {E : Type u_2} [LinearOrderedCommRing 𝕜] [LinearOrderedCommRing E] [Module 𝕜 E] {s : Set 𝕜} [OrderedSMul 𝕜 E] [IsScalarTower 𝕜 E E] [SMulCommClass 𝕜 E E] {f : 𝕜E} (hf : ConvexOn 𝕜 s f) (hf₀ : ∀ ⦃x : 𝕜⦄, x s0 f x) (n : ) :
ConvexOn 𝕜 s (f ^ n)
theorem convexOn_pow {𝕜 : Type u_1} [LinearOrderedCommRing 𝕜] (n : ) :
ConvexOn 𝕜 (Set.Ici 0) fun (x : 𝕜) => x ^ n

x^n, n : ℕ is convex on [0, +∞) for all n.

theorem Even.convexOn_pow {𝕜 : Type u_1} [LinearOrderedCommRing 𝕜] {n : } (hn : Even n) :
ConvexOn 𝕜 Set.univ fun (x : 𝕜) => x ^ n

x^n, n : ℕ is convex on the whole real line whenever n is even.

theorem convexOn_zpow {𝕜 : Type u_1} [LinearOrderedField 𝕜] (n : ) :
ConvexOn 𝕜 (Set.Ioi 0) fun (x : 𝕜) => x ^ n

x^m, m : ℤ is convex on (0, +∞) for all m.