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

• Even.convexOn_pow: for even n : ℕ.
• convexOn_pow: over $[0, +∞)$ for n : ℕ.
• convexOn_zpow: over $(0, +∞)$ For n : ℤ.

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 ∈ s → 0 ≤ f x) (hg₀ : ∀ ⦃x : 𝕜⦄, x ∈ s → 0 ≤ 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 ∈ s → 0 ≤ f x) (hg₀ : ∀ ⦃x : 𝕜⦄, x ∈ s → 0 ≤ 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 ∈ s → f x ≤ 0) (hg₀ : ∀ ⦃x : 𝕜⦄, x ∈ s → g 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 ∈ s → f x ≤ 0) (hg₀ : ∀ ⦃x : 𝕜⦄, x ∈ s → g 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 ∈ s → 0 ≤ f x) (hg₀ : ∀ ⦃x : 𝕜⦄, x ∈ s → g 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 ∈ s → 0 ≤ f x) (hg₀ : ∀ ⦃x : 𝕜⦄, x ∈ s → g 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 ∈ s → f x ≤ 0) (hg₀ : ∀ ⦃x : 𝕜⦄, x ∈ s → 0 ≤ 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 ∈ s → f x ≤ 0) (hg₀ : ∀ ⦃x : 𝕜⦄, x ∈ s → 0 ≤ 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 g : 𝕜 → E} (hf : ConvexOn 𝕜 s f) (hg : ConvexOn 𝕜 s g) (hf₀ : ∀ ⦃x : 𝕜⦄, x ∈ s → 0 ≤ f x) (hg₀ : ∀ ⦃x : 𝕜⦄, x ∈ s → 0 ≤ 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 g : 𝕜 → E} (hf : ConcaveOn 𝕜 s f) (hg : ConcaveOn 𝕜 s g) (hf₀ : ∀ ⦃x : 𝕜⦄, x ∈ s → 0 ≤ f x) (hg₀ : ∀ ⦃x : 𝕜⦄, x ∈ s → 0 ≤ 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 g : 𝕜 → E} (hf : ConvexOn 𝕜 s f) (hg : ConvexOn 𝕜 s g) (hf₀ : ∀ ⦃x : 𝕜⦄, x ∈ s → f x ≤ 0) (hg₀ : ∀ ⦃x : 𝕜⦄, x ∈ s → g 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 g : 𝕜 → E} (hf : ConcaveOn 𝕜 s f) (hg : ConcaveOn 𝕜 s g) (hf₀ : ∀ ⦃x : 𝕜⦄, x ∈ s → f x ≤ 0) (hg₀ : ∀ ⦃x : 𝕜⦄, x ∈ s → g 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 g : 𝕜 → E} (hf : ConvexOn 𝕜 s f) (hg : ConcaveOn 𝕜 s g) (hf₀ : ∀ ⦃x : 𝕜⦄, x ∈ s → 0 ≤ f x) (hg₀ : ∀ ⦃x : 𝕜⦄, x ∈ s → g 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 g : 𝕜 → E} (hf : ConcaveOn 𝕜 s f) (hg : ConvexOn 𝕜 s g) (hf₀ : ∀ ⦃x : 𝕜⦄, x ∈ s → 0 ≤ f x) (hg₀ : ∀ ⦃x : 𝕜⦄, x ∈ s → g 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 g : 𝕜 → E} (hf : ConvexOn 𝕜 s f) (hg : ConcaveOn 𝕜 s g) (hf₀ : ∀ ⦃x : 𝕜⦄, x ∈ s → f x ≤ 0) (hg₀ : ∀ ⦃x : 𝕜⦄, x ∈ s → 0 ≤ 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 g : 𝕜 → E} (hf : ConcaveOn 𝕜 s f) (hg : ConvexOn 𝕜 s g) (hf₀ : ∀ ⦃x : 𝕜⦄, x ∈ s → f x ≤ 0) (hg₀ : ∀ ⦃x : 𝕜⦄, x ∈ s → 0 ≤ 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 ∈ s → 0 ≤ 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.