Aggregation of finite coordinates

This file develops aggregation of a function along the fibers of a map between finite types. For Mathlib's intrinsic Convexity.StdSimplex, this operation is the finite-coordinate realization of Convexity.StdSimplex.map.

The fiber-cardinality results are included because they describe the exponents and normalization constants that occur when coordinate measures on standard simplices are pushed forward.

Main definitions and results

• stdSimplexAggregate: aggregation of coordinates along a finite map.
• Convexity.StdSimplex.weights_map_eq_stdSimplexAggregate: compatibility with the intrinsic standard-simplex map.
• stdSimplexAggregateFiberCard: cardinality of a fiber of the aggregation map.

@[reducible, inline]

noncomputable abbrev stdSimplexAggregate {ι : Type u_1} [Fintype ι] {κ : Type u_2} {R : Type u_3} [Finite κ] [Semiring R] (f : ι → κ) : (ι → R) → κ → R

Coordinate aggregation sends u : ι → R to its block sums under a map f : ι → κ. This is an application-oriented functional name for FunOnFinite.linearMap.

Equations

• stdSimplexAggregate f = ⇑(FunOnFinite.linearMap R R f)

theorem continuous_stdSimplexAggregate {ι : Type u_1} [Fintype ι] {κ : Type u_2} {R : Type u_3} [Finite κ] [Semiring R] [TopologicalSpace R] [ContinuousAdd R] (f : ι → κ) : Continuous (stdSimplexAggregate f)

Aggregation is continuous whenever addition in the coefficient semiring is continuous.

theorem Convexity.StdSimplex.weights_map_eq_stdSimplexAggregate {ι : Type u_1} [Fintype ι] {κ : Type u_2} {R : Type u_3} [Semiring R] [PartialOrder R] [IsStrictOrderedRing R] [Finite κ] (f : ι → κ) (s : StdSimplex R ι) : (fun (k : κ) => (map f s).weights k) = stdSimplexAggregate f fun (i : ι) => s.weights i

Mapping an intrinsic standard-simplex point and then reading its weights agrees with aggregation of its finite coordinate function.

theorem stdSimplexAggregate_pos {ι : Type u_1} [Fintype ι] {κ : Type u_2} {R : Type u_3} [Finite κ] [Semiring R] [PartialOrder R] [AddLeftStrictMono R] [IsOrderedCancelAddMonoid R] {f : ι → κ} (hf : Function.Surjective f) {u : ι → R} (hu : ∀ (i : ι), 0 < u i) (k : κ) : 0 < stdSimplexAggregate f u k

Aggregating positive parameters along a surjective partition gives positive parameters.

noncomputable def stdSimplexAggregateFiberCard {ι : Type u_1} [Fintype ι] {κ : Type u_2} (f : ι → κ) (k : κ) : ℕ

Cardinality of a fiber of an aggregation map. The codomain need not be finite because every fiber is a subtype of the finite domain ι.

Equations

• stdSimplexAggregateFiberCard f k = Fintype.card { i : ι // f i = k }

theorem stdSimplexAggregateFiberCard_pos {ι : Type u_1} [Fintype ι] {κ : Type u_2} {f : ι → κ} (hf : Function.Surjective f) (k : κ) : 0 < stdSimplexAggregateFiberCard f k

Every fiber of a surjective aggregation map has positive cardinality.

theorem sum_stdSimplexAggregateFiberCard {ι : Type u_1} [Fintype ι] {κ : Type u_2} [Fintype κ] (f : ι → κ) : ∑ k : κ, stdSimplexAggregateFiberCard f k = Fintype.card ι

The cardinalities of all fibers of a map from a finite type sum to the cardinality of its domain.

theorem stdSimplexAggregate_one {ι : Type u_1} [Fintype ι] {κ : Type u_2} {S : Type u_3} [Finite κ] [Semiring S] (f : ι → κ) (k : κ) : stdSimplexAggregate f (fun (x : ι) => 1) k = ↑(stdSimplexAggregateFiberCard f k)

Aggregating the constant-one vector records the cardinality of each fiber.