Product of convex spaces

This file defines the cartesian product of convex spaces.

@[instance_reducible]

noncomputable instance Prod.instConvexSpace {R : Type u_2} [Semiring R] [PartialOrder R] [IsStrictOrderedRing R] {X : Type u_4} {Y : Type u_5} [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_4} {Y : Type u_5} [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_4} {Y : Type u_5} [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_4} {Y : Type u_5} [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_4} {Y : Type u_5} [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_4} {Y : Type u_5} [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_4} {Y : Type u_5} [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_4} {Y : Type u_5} [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_4} {Y : Type u_5} [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

instance Prod.instIsConvexCombComm {R : Type u_2} {S : Type u_3} [Semiring R] [PartialOrder R] [IsStrictOrderedRing R] [Semiring S] [PartialOrder S] [IsStrictOrderedRing S] {X : Type u_4} {Y : Type u_5} [Convexity.ConvexSpace R X] [Convexity.ConvexSpace R Y] [Convexity.ConvexSpace S X] [Convexity.ConvexSpace S Y] [Convexity.IsConvexCombComm R S X] [Convexity.IsConvexCombComm R S Y] : Convexity.IsConvexCombComm R S (X × Y)

@[instance_reducible]

noncomputable instance Pi.instConvexSpaceForall {R : Type u_2} [Semiring R] [PartialOrder R] [IsStrictOrderedRing R] {ι : Type u_4} {X : ι → Type u_5} [(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_4} {X : ι → Type u_5} [(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_4} {X : ι → Type u_5} [(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_4} {X : ι → Type u_5} [(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_4} {X : ι → Type u_5} [(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)

instance Pi.instIsConvexCombCommForall {R : Type u_2} {S : Type u_3} [Semiring R] [PartialOrder R] [IsStrictOrderedRing R] [Semiring S] [PartialOrder S] [IsStrictOrderedRing S] {ι : Type u_4} {X : ι → Type u_5} [(i : ι) → Convexity.ConvexSpace R (X i)] [(i : ι) → Convexity.ConvexSpace S (X i)] [∀ (i : ι), Convexity.IsConvexCombComm R S (X i)] : Convexity.IsConvexCombComm R S ((i : ι) → X i)

@[instance_reducible]

noncomputable instance Finsupp.instConvexSpace {R : Type u_2} [Semiring R] [PartialOrder R] [IsStrictOrderedRing R] {ι : Type u_4} {X : Type u_5} [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_4} {X : Type u_5} [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_4} {X : Type u_5} [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_4} {X : Type u_5} [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_4} {X : Type u_5} [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)

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

theorem Convexity.IsAffineMap.prodMk {R : Type u_2} [Semiring R] [PartialOrder R] [IsStrictOrderedRing R] {X : Type u_5} {Y : Type u_6} [ConvexSpace R X] [ConvexSpace R Y] {Z : Type u_7} [ConvexSpace R Z] {f : X → Y} {g : X → Z} (hf : IsAffineMap R f) (hg : IsAffineMap R g) : IsAffineMap R fun (x : X) => (f x, g x)

theorem Convexity.IsAffineMap.fst {R : Type u_2} [Semiring R] [PartialOrder R] [IsStrictOrderedRing R] {X : Type u_5} {Y : Type u_6} [ConvexSpace R X] [ConvexSpace R Y] {Z : Type u_7} [ConvexSpace R Z] {f : X → Y × Z} (hf : IsAffineMap R f) : IsAffineMap R fun (x : X) => (f x).1

theorem Convexity.IsAffineMap.snd {R : Type u_2} [Semiring R] [PartialOrder R] [IsStrictOrderedRing R] {X : Type u_5} {Y : Type u_6} [ConvexSpace R X] [ConvexSpace R Y] {Z : Type u_7} [ConvexSpace R Z] {f : X → Y × Z} (hf : IsAffineMap R f) : IsAffineMap R fun (x : X) => (f x).2

theorem Convexity.isAffineMap_prod_iff {R : Type u_2} [Semiring R] [PartialOrder R] [IsStrictOrderedRing R] {X : Type u_5} {Y : Type u_6} [ConvexSpace R X] [ConvexSpace R Y] {Z : Type u_7} [ConvexSpace R Z] {f : X → Y × Z} : IsAffineMap R f ↔ (IsAffineMap R fun (x : X) => (f x).1) ∧ IsAffineMap R fun (x : X) => (f x).2

@[simp]

theorem Convexity.isAffineMap_prodMk_iff {R : Type u_2} [Semiring R] [PartialOrder R] [IsStrictOrderedRing R] {X : Type u_5} {Y : Type u_6} [ConvexSpace R X] [ConvexSpace R Y] {Z : Type u_7} [ConvexSpace R Z] {f : X → Y} {g : X → Z} : (IsAffineMap R fun (x : X) => (f x, g x)) ↔ IsAffineMap R f ∧ IsAffineMap R g

theorem Convexity.IsAffineMap.pi {R : Type u_2} [Semiring R] [PartialOrder R] [IsStrictOrderedRing R] {ι : Type u_4} {X : Type u_5} [ConvexSpace R X] {Y : ι → Type u_7} [(i : ι) → ConvexSpace R (Y i)] {f : X → (i : ι) → Y i} (hf : ∀ (i : ι), IsAffineMap R fun (x : X) => f x i) : IsAffineMap R f

theorem Convexity.IsAffineMap.eval {R : Type u_2} [Semiring R] [PartialOrder R] [IsStrictOrderedRing R] {ι : Type u_4} {X : Type u_5} [ConvexSpace R X] {Y : ι → Type u_7} [(i : ι) → ConvexSpace R (Y i)] {f : X → (i : ι) → Y i} (hf : IsAffineMap R f) (i : ι) : IsAffineMap R fun (x : X) => f x i

theorem Convexity.isAffineMap_pi_iff {R : Type u_2} [Semiring R] [PartialOrder R] [IsStrictOrderedRing R] {ι : Type u_4} {X : Type u_5} [ConvexSpace R X] {Y : ι → Type u_7} [(i : ι) → ConvexSpace R (Y i)] {f : X → (i : ι) → Y i} : IsAffineMap R f ↔ ∀ (i : ι), IsAffineMap R fun (x : X) => f x i

theorem Convexity.IsAffineMap.finsupp {R : Type u_2} [Semiring R] [PartialOrder R] [IsStrictOrderedRing R] {ι : Type u_4} {X : Type u_5} {Y : Type u_6} [ConvexSpace R X] [ConvexSpace R Y] [Zero Y] {f : X → ι →₀ Y} (hf : ∀ (i : ι), IsAffineMap R fun (x : X) => (f x) i) : IsAffineMap R f

theorem Convexity.IsAffineMap.finsuppEval {R : Type u_2} [Semiring R] [PartialOrder R] [IsStrictOrderedRing R] {ι : Type u_4} {X : Type u_5} {Y : Type u_6} [ConvexSpace R X] [ConvexSpace R Y] [Zero Y] {f : X → ι →₀ Y} (hf : IsAffineMap R f) (i : ι) : IsAffineMap R fun (x : X) => (f x) i

theorem Convexity.isAffineMap_finsupp_iff {R : Type u_2} [Semiring R] [PartialOrder R] [IsStrictOrderedRing R] {ι : Type u_4} {X : Type u_5} {Y : Type u_6} [ConvexSpace R X] [ConvexSpace R Y] [Zero Y] {f : X → ι →₀ Y} : IsAffineMap R f ↔ ∀ (i : ι), IsAffineMap R fun (x : X) => (f x) i