Fibrewise sums of Euclidean coordinates

A map f : ι → κ of finite index types coarsens a Euclidean coordinate system: the coordinates of a vector indexed by ι are merged into the groups cut out by the fibres of f, one group summed into each coordinate of a vector indexed by κ. This is Mathlib's FunOnFinite.map, here read through EuclideanSpace.equiv so that it acts on Euclidean space, where it is again continuous and measurable. The coordinates may be real or complex; measurability uses the Borel measurable structure on the scalar field.

Main definitions

• TauCeti.euclideanFiberSum sums the coordinates of a Euclidean vector over each fibre of a map of index types.

noncomputable def TauCeti.euclideanFiberSum {𝕜 : Type u_1} [RCLike 𝕜] {ι : Type u_2} {κ : Type u_3} [Fintype ι] [Fintype κ] (f : ι → κ) (x : EuclideanSpace 𝕜 ι) : EuclideanSpace 𝕜 κ

Sum the coordinates of a Euclidean vector over each fibre of f.

This is Mathlib's FunOnFinite.map read in Euclidean coordinates.

Equations

• TauCeti.euclideanFiberSum f x = (EuclideanSpace.equiv κ 𝕜).symm (FunOnFinite.map f ((EuclideanSpace.equiv ι 𝕜) x))

@[simp]

theorem TauCeti.euclideanFiberSum_apply {𝕜 : Type u_1} [RCLike 𝕜] {ι : Type u_2} {κ : Type u_3} [Fintype ι] [Fintype κ] [DecidableEq κ] (f : ι → κ) (x : EuclideanSpace 𝕜 ι) (j : κ) : (euclideanFiberSum f x).ofLp j = ∑ i : ι with f i = j, x.ofLp i

theorem TauCeti.continuous_euclideanFiberSum {𝕜 : Type u_1} [RCLike 𝕜] {ι : Type u_2} {κ : Type u_3} [Fintype ι] [Fintype κ] (f : ι → κ) : Continuous (euclideanFiberSum f)

Fibrewise summation is continuous.

theorem TauCeti.measurable_euclideanFiberSum {𝕜 : Type u_1} [RCLike 𝕜] {ι : Type u_2} {κ : Type u_3} [Fintype ι] [Fintype κ] [MeasurableSpace 𝕜] [BorelSpace 𝕜] (f : ι → κ) : Measurable (euclideanFiberSum f)

Fibrewise summation is measurable.