Theorems · Theorem · real analysis

ConvexOn.smul_concaveOn

∀ {𝕜 : Type u_1} {E : Type u_2} {F : Type u_3} {G : Type u_4} [inst : CommRing 𝕜] [inst_1 : LinearOrder 𝕜]
  [IsStrictOrderedRing 𝕜] [inst_3 : CommRing E] [inst_4 : LinearOrder E] [IsStrictOrderedRing E]
  [inst_6 : AddCommGroup F] [inst_7 : LinearOrder F] [IsOrderedAddMonoid F] [inst_9 : AddCommGroup G]
  [inst_10 : Module 𝕜 G] [inst_11 : Module 𝕜 E] [inst_12 : Module 𝕜 F] [inst_13 : Module E F] [IsScalarTower 𝕜 E F]
  [SMulCommClass 𝕜 E F] [IsOrderedModule 𝕜 F] [IsStrictOrderedModule E F] {s : Set G} {f : G → E} {g : G → F},
  ConvexOn 𝕜 s f →
    ConcaveOn 𝕜 s g →
      (∀ ⦃x : G⦄, x ∈ s → 0 ≤ f x) → (∀ ⦃x : G⦄, x ∈ s → g x ≤ 0) → AntivaryOn f g s → ConcaveOn 𝕜 s (f • g)

Defined in

Mathlib.Analysis.Convex.Mul

Cited by

1 results in Mathlib

Foundations

Depth 73 from the axioms · uses propext, Classical.choice, Quot.sound

Assumes

CommRingLinearOrderIsStrictOrderedRingCommRingLinearOrderIsStrictOrderedRingAddCommGroupLinearOrderIsOrderedAddMonoidAddCommGroupModuleModuleModuleModuleIsScalarTowerSMulCommClassIsOrderedModuleIsStrictOrderedModule