Documentation

TauCeti.Topology.PL.FiniteInf

Finite minima of affine functionals #

A finite minimum of continuous affine functionals is piecewise affine. The cells are the polyhedra on which a fixed functional is no larger than every member of the finite family. This is the chart calculation used by the inverse of a barycentric stellar identification: the amount transferred from a starred face is its least barycentric coordinate.

The construction is the standard polyhedral decomposition from Rourke--Sanderson, Introduction to Piecewise-Linear Topology, Chapter 1. It supplies the affine charts needed for PL compatibility of barycentric stellar identifications.

source
def Finset.infCell {E : Type u_1} [AddCommGroup E] [Module ℝ E] [TopologicalSpace E] {ι : Type u_2} (s : Finset ι) (f : ι → E →ᴬ[ℝ] ℝ) (i : ↥s) :
Set E

The cell on which the affine functional indexed by i is a minimum on s.

Instances For
    source
    @[simp]
    theorem Finset.mem_infCell_iff {E : Type u_1} [AddCommGroup E] [Module ℝ E] [TopologicalSpace E] {ι : Type u_2} (s : Finset ι) (f : ι → E →ᴬ[ℝ] ℝ) (i : ↥s) (x : E) :
    x ∈ s.infCell f i ↔ ∀ j ∈ s, (f ↑i) x ≤ (f j) x
    source
    theorem Finset.isConvexPolyhedron_infCell {E : Type u_1} [AddCommGroup E] [Module ℝ E] [TopologicalSpace E] {ι : Type u_2} (s : Finset ι) (f : ι → E →ᴬ[ℝ] ℝ) (i : ↥s) :
    TauCeti.IsConvexPolyhedron (s.infCell f i)

    A finite-minimum cell is an intersection of affine half-spaces.

    source
    theorem Finset.subset_iUnion_infCell {E : Type u_1} [AddCommGroup E] [Module ℝ E] [TopologicalSpace E] {ι : Type u_2} (s : Finset ι) (hs : s.Nonempty) (f : ι → E →ᴬ[ℝ] ℝ) :
    Set.univ ⊆ ⋃ (i : ↥s), s.infCell f i

    The cells of a finite family cover the whole source space.

    source
    theorem Finset.infAffine_eq_of_mem_infCell {E : Type u_1} [AddCommGroup E] [Module ℝ E] [TopologicalSpace E] {ι : Type u_2} (s : Finset ι) (hs : s.Nonempty) (f : ι → E →ᴬ[ℝ] ℝ) (i : ↥s) {x : E} (hx : x ∈ s.infCell f i) :
    (s.inf' hs fun (j : ι) => (f j) x) = (f ↑i) x

    The finite affine infimum agrees with the active functional on its cell.

    source
    theorem Finset.isPLOn_infAffine {E : Type u_1} [AddCommGroup E] [Module ℝ E] [TopologicalSpace E] {ι : Type u_2} (s : Finset ι) (hs : s.Nonempty) (f : ι → E →ᴬ[ℝ] ℝ) :
    TauCeti.IsPLOn (fun (x : E) => s.inf' hs fun (i : ι) => (f i) x) Set.univ

    A finite minimum of continuous affine functionals is piecewise affine on the whole source.