Product of convex spaces

This file defines the cartesian product of convex spaces.

@[implicit_reducible]

noncomputable instance Prod.instConvexSpace {R : Type u_2} [Semiring R] [PartialOrder R] [IsStrictOrderedRing R] {X : Type u_3} {Y : Type u_4} [Convexity.ConvexSpace R X] [Convexity.ConvexSpace R Y] : Convexity.ConvexSpace R (X × Y)

Equations

• Prod.instConvexSpace = Convexity.ConvexSpace.mk (fun (w : Convexity.StdSimplex R (X × Y)) => (Convexity.iConvexComb w Prod.fst, Convexity.iConvexComb w Prod.snd)) ⋯ ⋯

@[simp]

theorem Prod.fst_sConvexComb {R : Type u_2} [Semiring R] [PartialOrder R] [IsStrictOrderedRing R] {X : Type u_3} {Y : Type u_4} [Convexity.ConvexSpace R X] [Convexity.ConvexSpace R Y] (w : Convexity.StdSimplex R (X × Y)) : (Convexity.sConvexComb w).1 = Convexity.iConvexComb w fst

@[simp]

theorem Prod.snd_sConvexComb {R : Type u_2} [Semiring R] [PartialOrder R] [IsStrictOrderedRing R] {X : Type u_3} {Y : Type u_4} [Convexity.ConvexSpace R X] [Convexity.ConvexSpace R Y] (w : Convexity.StdSimplex R (X × Y)) : (Convexity.sConvexComb w).2 = Convexity.iConvexComb w snd

theorem Prod.isAffineMap_fst {R : Type u_2} [Semiring R] [PartialOrder R] [IsStrictOrderedRing R] {X : Type u_3} {Y : Type u_4} [Convexity.ConvexSpace R X] [Convexity.ConvexSpace R Y] : Convexity.IsAffineMap R fst

theorem Prod.isAffineMap_snd {R : Type u_2} [Semiring R] [PartialOrder R] [IsStrictOrderedRing R] {X : Type u_3} {Y : Type u_4} [Convexity.ConvexSpace R X] [Convexity.ConvexSpace R Y] : Convexity.IsAffineMap R snd

@[simp]

theorem Prod.fst_iConvexComb {I : Type u_1} {R : Type u_2} [Semiring R] [PartialOrder R] [IsStrictOrderedRing R] {X : Type u_3} {Y : Type u_4} [Convexity.ConvexSpace R X] [Convexity.ConvexSpace R Y] (w : Convexity.StdSimplex R I) (f : I → X × Y) : (Convexity.iConvexComb w f).1 = Convexity.iConvexComb w fun (i : I) => (f i).1

@[simp]

theorem Prod.snd_iConvexComb {I : Type u_1} {R : Type u_2} [Semiring R] [PartialOrder R] [IsStrictOrderedRing R] {X : Type u_3} {Y : Type u_4} [Convexity.ConvexSpace R X] [Convexity.ConvexSpace R Y] (w : Convexity.StdSimplex R I) (f : I → X × Y) : (Convexity.iConvexComb w f).2 = Convexity.iConvexComb w fun (i : I) => (f i).2

@[simp]

theorem Prod.fst_convexCombPair {R : Type u_2} [Semiring R] [PartialOrder R] [IsStrictOrderedRing R] {X : Type u_3} {Y : Type u_4} [Convexity.ConvexSpace R X] [Convexity.ConvexSpace R Y] (a b : R) (ha : 0 ≤ a) (hb : 0 ≤ b) (hab : a + b = 1) (x y : X × Y) : (Convexity.convexCombPair a b ha hb hab x y).1 = Convexity.convexCombPair a b ha hb hab x.1 y.1

@[simp]

theorem Prod.snd_convexCombPair {R : Type u_2} [Semiring R] [PartialOrder R] [IsStrictOrderedRing R] {X : Type u_3} {Y : Type u_4} [Convexity.ConvexSpace R X] [Convexity.ConvexSpace R Y] (a b : R) (ha : 0 ≤ a) (hb : 0 ≤ b) (hab : a + b = 1) (x y : X × Y) : (Convexity.convexCombPair a b ha hb hab x y).2 = Convexity.convexCombPair a b ha hb hab x.2 y.2

@[implicit_reducible]

noncomputable instance Pi.instConvexSpaceForall {R : Type u_2} [Semiring R] [PartialOrder R] [IsStrictOrderedRing R] {ι : Type u_3} {X : ι → Type u_4} [(i : ι) → Convexity.ConvexSpace R (X i)] : Convexity.ConvexSpace R ((i : ι) → X i)

Equations

• Pi.instConvexSpaceForall = Convexity.ConvexSpace.mk (fun (w : Convexity.StdSimplex R ((i : ι) → X i)) (i : ι) => Convexity.iConvexComb w fun (x : (i : ι) → X i) => x i) ⋯ ⋯

@[simp]

theorem Pi.sConvexComb_apply {R : Type u_2} [Semiring R] [PartialOrder R] [IsStrictOrderedRing R] {ι : Type u_3} {X : ι → Type u_4} [(i : ι) → Convexity.ConvexSpace R (X i)] (w : Convexity.StdSimplex R ((i : ι) → X i)) (i : ι) : Convexity.sConvexComb w i = Convexity.iConvexComb w fun (x : (i : ι) → X i) => x i

theorem Pi.isAffineMap_eval {R : Type u_2} [Semiring R] [PartialOrder R] [IsStrictOrderedRing R] {ι : Type u_3} {X : ι → Type u_4} [(i : ι) → Convexity.ConvexSpace R (X i)] {i : ι} : Convexity.IsAffineMap R fun (x : (i : ι) → X i) => x i

@[simp]

theorem Pi.iConvexComb_apply {I : Type u_1} {R : Type u_2} [Semiring R] [PartialOrder R] [IsStrictOrderedRing R] {ι : Type u_3} {X : ι → Type u_4} [(i : ι) → Convexity.ConvexSpace R (X i)] (w : Convexity.StdSimplex R I) (f : I → (i : ι) → X i) (i : ι) : Convexity.iConvexComb w f i = Convexity.iConvexComb w fun (j : I) => f j i

@[simp]

theorem Pi.convexCombPair_apply {R : Type u_2} [Semiring R] [PartialOrder R] [IsStrictOrderedRing R] {ι : Type u_3} {X : ι → Type u_4} [(i : ι) → Convexity.ConvexSpace R (X i)] (a b : R) (ha : 0 ≤ a) (hb : 0 ≤ b) (hab : a + b = 1) (f g : (i : ι) → X i) (i : ι) : Convexity.convexCombPair a b ha hb hab f g i = Convexity.convexCombPair a b ha hb hab (f i) (g i)

@[implicit_reducible]

noncomputable instance Finsupp.instConvexSpace {R : Type u_2} [Semiring R] [PartialOrder R] [IsStrictOrderedRing R] {ι : Type u_3} {X : Type u_4} [Zero X] [Convexity.ConvexSpace R X] : Convexity.ConvexSpace R (ι →₀ X)

Equations

• One or more equations did not get rendered due to their size.

@[simp]

theorem Finsupp.sConvexComb_apply {R : Type u_2} [Semiring R] [PartialOrder R] [IsStrictOrderedRing R] {ι : Type u_3} {X : Type u_4} [Zero X] [Convexity.ConvexSpace R X] (w : Convexity.StdSimplex R (ι →₀ X)) (i : ι) : (Convexity.sConvexComb w) i = Convexity.iConvexComb w fun (x : ι →₀ X) => x i

theorem Finsupp.isAffineMap_eval {R : Type u_2} [Semiring R] [PartialOrder R] [IsStrictOrderedRing R] {ι : Type u_3} {X : Type u_4} [Zero X] [Convexity.ConvexSpace R X] {i : ι} : Convexity.IsAffineMap R fun (x : ι →₀ X) => x i

@[simp]

theorem Finsupp.iConvexComb_apply {I : Type u_1} {R : Type u_2} [Semiring R] [PartialOrder R] [IsStrictOrderedRing R] {ι : Type u_3} {X : Type u_4} [Zero X] [Convexity.ConvexSpace R X] (w : Convexity.StdSimplex R I) (f : I → ι →₀ X) (i : ι) : (Convexity.iConvexComb w f) i = Convexity.iConvexComb w fun (j : I) => (f j) i

@[simp]

theorem Finsupp.convexCombPair_apply {R : Type u_2} [Semiring R] [PartialOrder R] [IsStrictOrderedRing R] {ι : Type u_3} {X : Type u_4} [Zero X] [Convexity.ConvexSpace R X] (a b : R) (ha : 0 ≤ a) (hb : 0 ≤ b) (hab : a + b = 1) (f g : ι →₀ X) (i : ι) : (Convexity.convexCombPair a b ha hb hab f g) i = Convexity.convexCombPair a b ha hb hab (f i) (g i)