Fibers of convex subsets of products

For a convex set s ⊆ V × W, each fiber Prod.mk v ⁻¹' s is convex, and a convex combination of two fibers, formed by pointwise Minkowski operations, lies in the fiber over the corresponding convex combination of base points. The second inclusion is the set-level input for Brunn's concavity principle, which compares fiber volumes by the Brunn–Minkowski inequality.

A strip |u.1| < a of a product 𝕜 × W is convex (TauCeti.convex_setOf_abs_fst_lt). Convexity transfers between subsets of V × ℝ that correspond under a nonzero rescaling of the height coordinate (TauCeti.convex_of_height_scale).

theorem Convex.preimage_prodMk {𝕜 : Type u_1} {V : Type u_2} {W : Type u_3} [Semiring 𝕜] [PartialOrder 𝕜] [AddCommMonoid V] [Module 𝕜 V] [AddCommMonoid W] [Module 𝕜 W] {s : Set (V × W)} (hs : Convex 𝕜 s) (v : V) : Convex 𝕜 (Prod.mk v ⁻¹' s)

The fibers of a convex subset of a product are convex.

theorem Convex.smul_preimage_prodMk_add_smul_preimage_prodMk_subset {𝕜 : Type u_1} {V : Type u_2} {W : Type u_3} [Semiring 𝕜] [PartialOrder 𝕜] [AddCommMonoid V] [Module 𝕜 V] [AddCommMonoid W] [Module 𝕜 W] {s : Set (V × W)} (hs : Convex 𝕜 s) (p q : V) {a b : 𝕜} (ha : 0 ≤ a) (hb : 0 ≤ b) (hab : a + b = 1) : a • Prod.mk p ⁻¹' s + b • Prod.mk q ⁻¹' s ⊆ Prod.mk (a • p + b • q) ⁻¹' s

A convex combination of two fibers of a convex set lies in the fiber over the convex combination of the base points.

theorem TauCeti.convex_setOf_abs_fst_lt {𝕜 : Type u_4} {W : Type u_5} [Field 𝕜] [LinearOrder 𝕜] [IsStrictOrderedRing 𝕜] [AddCommGroup W] [Module 𝕜 W] (a : 𝕜) : Convex 𝕜 {u : 𝕜 × W | |u.1| < a}

A strip |u.1| < a of a product 𝕜 × W is convex.

theorem TauCeti.convex_of_height_scale {V : Type u_4} [AddCommMonoid V] [SMul ℝ V] {s t : Set (V × ℝ)} {r : ℝ} (hr : r ≠ 0) (hst : ∀ (x : V) (τ : ℝ), (x, τ) ∈ s ↔ (x, r * τ) ∈ t) (h : Convex ℝ s) : Convex ℝ t

Rescaling the height coordinate by a nonzero real r transfers convexity from a subset of V × ℝ to any subset that corresponds to it under that rescaling.