The ambient affine-hyperplane coordinate measure

theorem MeasureTheory.Measure.measurable_stdSimplexCoordMap {ι : Type u_1} [Fintype ι] (i : ι) : Measurable (stdSimplexCoordMap i)

The coordinate map is measurable.

noncomputable def MeasureTheory.Measure.stdSimplexMeasureAt {ι : Type u_1} [Fintype ι] (i : ι) : Measure (ι → ℝ)

Lebesgue measure pushed forward from the free coordinates omitting i.

Equations

• MeasureTheory.Measure.stdSimplexMeasureAt i = MeasureTheory.Measure.map (stdSimplexCoordMap i) MeasureTheory.volume

theorem MeasureTheory.Measure.volume_map_smul_free_coords {ι : Type u_1} [Fintype ι] (i : ι) (c : ℝ) (hc : 0 < c) : map (fun (x : { j : ι // j ≠ i } → ℝ) => c • x) volume = ENNReal.ofReal (c ^ (Fintype.card ι - 1))⁻¹ • volume

The Lebesgue measure is homogeneous of degree (Fintype.card ι - 1) in the free coordinates.

theorem MeasureTheory.Measure.stdSimplexMeasureAt_eq_map_piSplitAt_symm {ι : Type u_1} [Fintype ι] (i : ι) : stdSimplexMeasureAt i = map (⇑(Homeomorph.piSplitAt i fun (x : ι) => ℝ).symm) (map (fun (x : { j : ι // j ≠ i } → ℝ) => (1 - ∑ q : { j : ι // j ≠ i }, x q, x)) volume)

Coordinate explicit form of stdSimplexMeasureAt.

theorem MeasureTheory.Measure.stdSimplexMeasureAt_map_perm {ι : Type u_1} [Fintype ι] (i : ι) (σ : Equiv.Perm ι) : map (fun (u : ι → ℝ) => u ∘ ⇑σ) (stdSimplexMeasureAt (σ i)) = stdSimplexMeasureAt i

Pushing stdSimplexMeasureAt (σ i) forward along σ gives stdSimplexMeasureAt i.

theorem MeasureTheory.Measure.stdSimplexMeasureAt_swap {ι : Type u_1} [Fintype ι] (i j : ι) : map (fun (x : ι → ℝ) => x ∘ ⇑(Equiv.swap i j)) (stdSimplexMeasureAt i) = stdSimplexMeasureAt j

Pushing stdSimplexMeasureAt i forward along the transposition swap i j gives stdSimplexMeasureAt j.

theorem MeasureTheory.Measure.stdSimplexMeasureAt_eq {ι : Type u_1} [Fintype ι] (i j : ι) : stdSimplexMeasureAt i = stdSimplexMeasureAt j

The coordinate measure is independent of the chosen special coordinate.

noncomputable def MeasureTheory.Measure.stdSimplexMeasure {ι : Type u_1} [Fintype ι] : Measure (ι → ℝ)

The coordinate Lebesgue measure on stdSimplexAffineSet. When ι is empty the measure is zero; otherwise it is the push-forward of Lebesgue measure from any set of free coordinates.

Equations

• MeasureTheory.Measure.stdSimplexMeasure = if h : Nonempty ι then MeasureTheory.Measure.stdSimplexMeasureAt (Classical.choice h) else 0

theorem MeasureTheory.Measure.stdSimplexMeasure_eq_at {ι : Type u_1} [Fintype ι] [Nonempty ι] (i : ι) : stdSimplexMeasure = stdSimplexMeasureAt i

stdSimplexMeasure equals stdSimplexMeasureAt i, for any i.

theorem MeasureTheory.Measure.stdSimplexMeasure_restrict_stdSimplex {ι : Type u_1} [Fintype ι] [Nonempty ι] (i : ι) : stdSimplexMeasure.restrict (Convexity.StdSimplex.coordinateSet ℝ ι) = map (stdSimplexCoordMap i) (volume.restrict (stdSimplexFreeCoords i))

The coordinate map pushes the restricted volume on the free coordinates to the restricted simplex measure.

@[simp]

theorem MeasureTheory.Measure.stdSimplexMeasure_empty {ι : Type u_1} [Fintype ι] [IsEmpty ι] : stdSimplexMeasure = 0

stdSimplexMeasure is zero when ι is empty.

instance MeasureTheory.Measure.sigmaFinite_stdSimplexMeasure {ι : Type u_1} [Fintype ι] : SigmaFinite stdSimplexMeasure

stdSimplexMeasure is a SigmaFinite measure.

@[simp]

theorem MeasureTheory.Measure.stdSimplexMeasureAt_of_unique {ι : Type u_1} [Fintype ι] [Unique ι] (i : ι) : stdSimplexMeasureAt i = dirac fun (x : ι) => 1

For a type with a unique element, the pushforward measure at that element is a Dirac mass at the all-ones point.

theorem MeasureTheory.Measure.stdSimplexMeasure_unique {ι : Type u_1} [Fintype ι] [Unique ι] : stdSimplexMeasure = dirac fun (x : ι) => 1

Restating stdSimplexMeasureAt_of_unique in terms of stdSimplexMeasure.

theorem MeasureTheory.Measure.stdSimplexMeasure_restrict_stdSimplexAffineSet {ι : Type u_1} [Fintype ι] : stdSimplexMeasure = stdSimplexMeasure.restrict stdSimplexAffineSet

The coordinate Lebesgue measure is supported on stdSimplexAffineSet.

instance MeasureTheory.Measure.instIsFiniteMeasureForallRealRestrictStdSimplexMeasureCoordinateSet {ι : Type u_1} [Fintype ι] : IsFiniteMeasure (stdSimplexMeasure.restrict (Convexity.StdSimplex.coordinateSet ℝ ι))

The coordinate Lebesgue measure is finite on the standard simplex.

theorem MeasureTheory.Measure.measurePreserving_stdSimplexMeasure_perm {ι : Type u_1} [Fintype ι] (σ : Equiv.Perm ι) : MeasurePreserving (fun (x : ι → ℝ) => x ∘ ⇑σ) stdSimplexMeasure stdSimplexMeasure

Permuting coordinates is a measure-preserving transformation of stdSimplexMeasure: the map x ↦ x ∘ σ is measurable, and it pushes stdSimplexMeasure forward to itself.

theorem MeasureTheory.Measure.stdSimplexMeasure_map_perm {ι : Type u_1} [Fintype ι] (σ : Equiv.Perm ι) : map (fun (x : ι → ℝ) => x ∘ ⇑σ) stdSimplexMeasure = stdSimplexMeasure

The pushforward of stdSimplexMeasure under a coordinate permutation is stdSimplexMeasure itself — the Measure.map equation extracted from measurePreserving_stdSimplexMeasure_perm.

@[simp]

theorem MeasureTheory.Measure.stdSimplexMeasure_stdSimplex {ι : Type u_1} [Fintype ι] [Nonempty ι] : stdSimplexMeasure (Convexity.StdSimplex.coordinateSet ℝ ι) = 1 / ↑(Fintype.card ι - 1).factorial

Extended real evaluation of the measure of the standard simplex. The value is $1/(k-1)!$ where k = Fintype.card ι.

theorem MeasureTheory.Measure.stdSimplexMeasure_stdSimplex_toReal {ι : Type u_1} [Fintype ι] [Nonempty ι] : (stdSimplexMeasure (Convexity.StdSimplex.coordinateSet ℝ ι)).toReal = 1 / ↑(Fintype.card ι - 1).factorial

Real-valued form of the coordinate-volume formula for the standard simplex.

theorem MeasureTheory.Measure.stdSimplexMeasure_stdSimplex_ne_top {ι : Type u_1} [Fintype ι] [Nonempty ι] : stdSimplexMeasure (Convexity.StdSimplex.coordinateSet ℝ ι) ≠ ⊤

The measure of the standard simplex is finite.

theorem MeasureTheory.Measure.stdSimplexMeasureAt_apply {ι : Type u_1} [Fintype ι] (i : ι) {s : Set (ι → ℝ)} (hs : MeasurableSet s) : (stdSimplexMeasureAt i) s = volume (stdSimplexCoordMap i ⁻¹' s)

The projected measure of a measurable set: stdSimplexMeasureAt i s equals the volume of the preimage of s under stdSimplexCoordMap i.

theorem MeasureTheory.Measure.stdSimplexMeasure_coord_eq_zero {ι : Type u_1} [Fintype ι] [Nonempty ι] (i : ι) : stdSimplexMeasure {u : ι → ℝ | u i = 0} = 0

The coordinate faces have measure 0.

theorem MeasureTheory.Measure.ae_zero_lt_of_mem_stdSimplex {ι : Type u_1} [Fintype ι] [Nonempty ι] : ∀ᵐ (u : ι → ℝ) ∂stdSimplexMeasure.restrict (Convexity.StdSimplex.coordinateSet ℝ ι), ∀ (i : ι), 0 < u i

Almost every point of the simplex has every coordinate strictly positive, with respect to stdSimplexMeasure restricted to the simplex.

theorem MeasureTheory.Measure.memLp_coordinate_of_restrict_stdSimplex {ι : Type u_1} [Fintype ι] {μ : Measure (ι → ℝ)} [IsFiniteMeasure μ] (hμ : μ.restrict (Convexity.StdSimplex.coordinateSet ℝ ι) = μ) (i : ι) (p : ENNReal) : MemLp (fun (u : ι → ℝ) => u i) p μ

Coordinates belong to every Lᵖ space for a finite measure supported on the simplex.