Aggregation of solid-simplex volume

Aggregation of a solid simplex

theorem lintegral_posSimplex_split_pred {α : Type u_1} [Fintype α] (p : α → Prop) [DecidablePred p] (r : ℝ) (G : ({ a : α // p a } → ℝ) × ({ a : α // ¬p a } → ℝ) → ENNReal) (hG : Measurable G) : ∫⁻ (x : α → ℝ) in posSimplex α r, G ((MeasurableEquiv.piEquivPiSubtypeProd (fun (x : α) => ℝ) p) x) = ∫⁻ (u : { a : α // p a } → ℝ) in posSimplex { a : α // p a } r, ∫⁻ (v : { a : α // ¬p a } → ℝ) in posSimplex { a : α // ¬p a } (r - ∑ i : { a : α // p a }, u i), G (u, v)

Tonelli disintegration of a positive simplex after splitting along a decidable predicate.

noncomputable def posSimplexAggregateDensity {α : Type u_1} {β : Type u_2} [Fintype α] [Fintype β] (f : α → β) (z : β → ℝ) : ENNReal

Fibrewise density for the push-forward of Lebesgue measure on a solid simplex under coordinate aggregation. For a vector z this is the product of the solid-simplex volumes of the fibres of f.

Equations

• posSimplexAggregateDensity f z = ∏ k : β, ENNReal.ofReal (z k) ^ (Fintype.card { i : α // f i = k } - 1) / ↑(Fintype.card { i : α // f i = k } - 1).factorial

theorem lintegral_posSimplex_comp_aggregate_of_isEmpty {α : Type u_1} {β : Type u_2} [Fintype α] [Fintype β] [IsEmpty β] (f : α → β) (_hf : Function.Surjective f) (r : ℝ) (hr : 0 ≤ r) (g : (β → ℝ) → ENNReal) (_hg : Measurable g) : ∫⁻ (x : α → ℝ) in posSimplex α r, g ((FunOnFinite.linearMap ℝ ℝ f) x) = ∫⁻ (z : β → ℝ) in posSimplex β r, g z * posSimplexAggregateDensity f z

The solid-simplex aggregation formula when the target index type is empty.

theorem lintegral_posSimplex_comp_aggregate_of_unique {α : Type u_1} {β : Type u_2} [Fintype α] [Fintype β] [Unique β] (f : α → β) (hf : Function.Surjective f) (r : ℝ) (hr : 0 ≤ r) (g : (β → ℝ) → ENNReal) (hg : Measurable g) : ∫⁻ (x : α → ℝ) in posSimplex α r, g ((FunOnFinite.linearMap ℝ ℝ f) x) = ∫⁻ (z : β → ℝ) in posSimplex β r, g z * posSimplexAggregateDensity f z

The solid-simplex aggregation formula when the target has a unique coordinate.

theorem lintegral_posSimplex_comp_aggregate {α : Type u_1} {β : Type u_2} [Fintype α] [Fintype β] (f : α → β) (hf : Function.Surjective f) (r : ℝ) (hr : 0 ≤ r) (g : (β → ℝ) → ENNReal) (hg : Measurable g) : ∫⁻ (x : α → ℝ) in posSimplex α r, g ((FunOnFinite.linearMap ℝ ℝ f) x) = ∫⁻ (z : β → ℝ) in posSimplex β r, g z * posSimplexAggregateDensity f z

Pushing Lebesgue measure on a solid simplex forward under coordinate aggregation (FunOnFinite.linearMap) weights the target solid simplex by the product of fibre volumes.

This is the solid-simplex form of the aggregation identity used for stdSimplexMeasure. The unique-target case is lintegral_posSimplex_comp_sum.