Radial integration over the positive orthant

The radial coordinate is the sum of the coordinates. Its angular measure is the coordinate-normalized standard-simplex measure, so the radial factor is t^(card ι - 1).

theorem MeasureTheory.radial_slice_smul {ι : Type u_1} [Fintype ι] (i : ι) (t : ℝ) (v : { j : ι // j ≠ i } → ℝ) : (Homeomorph.funSplitAt ℝ i).symm (t - ∑ j : { j : ι // j ≠ i }, t * v j, t • v) = t • stdSimplexCoordMap i v

Scaling free coordinates in a slice of fixed coordinate sum scales its simplex chart.

theorem MeasureTheory.lintegral_eq_lintegral_sum_slice {ι : Type u_1} [Fintype ι] (i : ι) (f : (ι → ℝ) → ENNReal) (hf : Measurable f) : ∫⁻ (x : ι → ℝ), f x = ∫⁻ (t : ℝ) (v : { j : ι // j ≠ i } → ℝ), f ((Homeomorph.funSplitAt ℝ i).symm (t - ∑ j : { j : ι // j ≠ i }, v j, v))

Lebesgue integration with the sum of the coordinates as the first coordinate.

theorem MeasureTheory.sum_radial_slice {ι : Type u_1} [Fintype ι] (i : ι) (t : ℝ) (v : { j : ι // j ≠ i } → ℝ) : ∑ j : ι, (Homeomorph.funSplitAt ℝ i).symm (t - ∑ k : { j : ι // j ≠ i }, v k, v) j = t

The affine slice with total t has coordinate sum t.

theorem MeasureTheory.nonneg_radial_slice_iff {ι : Type u_1} [Fintype ι] (i : ι) (t : ℝ) (v : { j : ι // j ≠ i } → ℝ) : (∀ (j : ι), 0 ≤ (Homeomorph.funSplitAt ℝ i).symm (t - ∑ k : { j : ι // j ≠ i }, v k, v) j) ↔ v ∈ posSimplex { j : ι // j ≠ i } t

Nonnegative points on the slice of total t are parametrized by the positive simplex of radius t in the free coordinates.

theorem MeasureTheory.lintegral_eq_radial_stdSimplex {ι : Type u_1} [Fintype ι] [Nonempty ι] (f : (ι → ℝ) → ENNReal) (hf : Measurable f) (hsupp : ∀ (x : ι → ℝ), (¬∀ (i : ι), 0 ≤ x i) → f x = 0) : ∫⁻ (x : ι → ℝ), f x = ∫⁻ (t : ℝ) in Set.Ioi 0, ENNReal.ofReal (t ^ (Fintype.card ι - 1)) * ∫⁻ (u : ι → ℝ) in Convexity.StdSimplex.coordinateSet ℝ ι, f (t • u) ∂Measure.stdSimplexMeasure

Radial integration for a measurable nonnegative function supported on the positive orthant. The simplex measure is the coordinate-normalized one, with no Euclidean area factor.