Connect the algebraic definition and measure theory for the volume of a simplex

This file proves that Affine.Simplex.volume agrees with the volume measure of its closed interior.

Main statements

• Affine.Simplex.euclideanHausdorffMeasure_real_closedInterior: the volume measure of the closed interior of a simplex satisfies the recurrence relation with base and height.
• Affine.Simplex.volume_eq_euclideanHausdorffMeasure_real_closedInterior: Affine.Simplex.volume is equal to the volume measure of the closed interior.

theorem Affine.Simplex.measurableSet_closedInterior {V : Type u_1} {P : Type u_2} [NormedAddCommGroup V] [InnerProductSpace ℝ V] [MetricSpace P] [NormedAddTorsor V P] [MeasurableSpace P] [BorelSpace P] {n : ℕ} (s : Simplex ℝ P n) : MeasurableSet s.closedInterior

theorem Affine.Simplex.euclideanHausdorffMeasure_closedInterior_inter_shift_aeEq {V : Type u_1} {P : Type u_2} [NormedAddCommGroup V] [InnerProductSpace ℝ V] [MetricSpace P] [NormedAddTorsor V P] [MeasurableSpace P] [BorelSpace P] {n : ℕ} (s : Simplex ℝ P (n + 1)) (i : Fin (n + 2)) : (fun (x : ℝ) => (MeasureTheory.Measure.euclideanHausdorffMeasure n) (s.closedInterior ∩ ↑((affineSpan ℝ (s.points '' {i}ᶜ)).shift (s.points i) x))) =ᵐ[MeasureTheory.volume.restrict (Set.Icc 0 1)] fun (x : ℝ) => ‖x‖₊ ^ n • (MeasureTheory.Measure.euclideanHausdorffMeasure n) (s.faceOpposite i).closedInterior

The volume of the cross section of a simplex is scaled from the base. This is an intermediate result for volume calculation and is expressed as a.e.-equal to take care of the exception at zero.

TODO: if the cross section object also shows up elsewhere, we should turn it to a proper definition.

theorem Affine.Simplex.support_euclideanHausdorffMeasure_closedInterior_inter_shift_subset {V : Type u_1} {P : Type u_2} [NormedAddCommGroup V] [InnerProductSpace ℝ V] [MetricSpace P] [NormedAddTorsor V P] [MeasurableSpace P] [BorelSpace P] {n : ℕ} (s : Simplex ℝ P (n + 1)) (i : Fin (n + 2)) : (Function.support fun (x : ℝ) => (MeasureTheory.Measure.euclideanHausdorffMeasure n) (s.closedInterior ∩ ↑((affineSpan ℝ (s.points '' {i}ᶜ)).shift (s.points i) x))) ⊆ Set.Icc 0 1

The cross section of a simplex vanishes outside of the simplex in terms of its volume.

theorem Affine.Simplex.euclideanHausdorffMeasure_closedInterior {V : Type u_1} {P : Type u_2} [NormedAddCommGroup V] [InnerProductSpace ℝ V] [MetricSpace P] [NormedAddTorsor V P] [MeasurableSpace P] [BorelSpace P] {n : ℕ} (s : Simplex ℝ P (n + 1)) (i : Fin (n + 2)) : (MeasureTheory.Measure.euclideanHausdorffMeasure (n + 1)) s.closedInterior = (↑(n + 1))⁻¹ * ENNReal.ofReal (s.height i) * (MeasureTheory.Measure.euclideanHausdorffMeasure n) (s.faceOpposite i).closedInterior

The $n$-volume of the closed interior of a $n$-simplex is equal to $h * b / n$, where $h$ is the height and $b$ is the $(n - 1)$-volume of the base. This version is expressed in ENNReal.

theorem Affine.Simplex.euclideanHausdorffMeasure_real_closedInterior {V : Type u_1} {P : Type u_2} [NormedAddCommGroup V] [InnerProductSpace ℝ V] [MetricSpace P] [NormedAddTorsor V P] [MeasurableSpace P] [BorelSpace P] {n : ℕ} (s : Simplex ℝ P (n + 1)) (i : Fin (n + 2)) : (MeasureTheory.Measure.euclideanHausdorffMeasure (n + 1)).real s.closedInterior = (↑(n + 1))⁻¹ * s.height i * (MeasureTheory.Measure.euclideanHausdorffMeasure n).real (s.faceOpposite i).closedInterior

The $n$-volume of the closed interior of a $n$-simplex is equal to $h * b / n$, where $h$ is the height and $b$ is the $(n - 1)$-volume of the base. This version is expressed in Real.

theorem Affine.Simplex.euclideanHausdorffMeasure_closedInterior_eq_one {V : Type u_1} {P : Type u_2} [NormedAddCommGroup V] [InnerProductSpace ℝ V] [MetricSpace P] [NormedAddTorsor V P] [MeasurableSpace P] [BorelSpace P] (s : Simplex ℝ P 0) : (MeasureTheory.Measure.euclideanHausdorffMeasure 0) s.closedInterior = 1

theorem Affine.Simplex.euclideanHausdorffMeasure_closedInterior_real_eq_one {V : Type u_1} {P : Type u_2} [NormedAddCommGroup V] [InnerProductSpace ℝ V] [MetricSpace P] [NormedAddTorsor V P] [MeasurableSpace P] [BorelSpace P] (s : Simplex ℝ P 0) : (MeasureTheory.Measure.euclideanHausdorffMeasure 0).real s.closedInterior = 1

theorem Affine.Simplex.volume_eq_euclideanHausdorffMeasure_real_closedInterior {V : Type u_1} {P : Type u_2} [NormedAddCommGroup V] [InnerProductSpace ℝ V] [MetricSpace P] [NormedAddTorsor V P] [MeasurableSpace P] [BorelSpace P] {n : ℕ} (s : Simplex ℝ P n) : s.volume = (MeasureTheory.Measure.euclideanHausdorffMeasure n).real s.closedInterior

Affine.Simplex.volume is equal to the Euclidean Hausdorff measure of the closed interior.

theorem Affine.Simplex.volume_eq_volume_real_closedInterior {V : Type u_1} [NormedAddCommGroup V] [InnerProductSpace ℝ V] {n : ℕ} [MeasurableSpace V] [BorelSpace V] [FiniteDimensional ℝ V] (hn : Module.finrank ℝ V = n) (s : Simplex ℝ V n) : s.volume = MeasureTheory.volume.real s.closedInterior

Affine.Simplex.volume is equal to the Lebesgue measure of the closed interior.