Probability lemmas for Grünbaum's inequality

theorem Grunbaum.volume_preimage_singleton_eq_zero {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] [FiniteDimensional ℝ E] [MeasureTheory.MeasureSpace E] [BorelSpace E] [MeasureTheory.volume.IsAddHaarMeasure] (L : E →L[ℝ] ℝ) (hL : L ≠ 0) (t : ℝ) : MeasureTheory.volume (⇑L ⁻¹' {t}) = 0

theorem Grunbaum.nullSingletonClass_map_uniform {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] [FiniteDimensional ℝ E] [MeasureTheory.MeasureSpace E] [BorelSpace E] [MeasureTheory.volume.IsAddHaarMeasure] (K : Set E) (L : E →L[ℝ] ℝ) (hL : L ≠ 0) : MeasureTheory.NullSingletonClass (MeasureTheory.Measure.map (⇑L) ((MeasureTheory.volume K)⁻¹ • MeasureTheory.volume.restrict K))

theorem Grunbaum.continuous_cdf_of_noAtoms (μ : MeasureTheory.Measure ℝ) [MeasureTheory.IsProbabilityMeasure μ] [MeasureTheory.NullSingletonClass μ] : Continuous ↑(ProbabilityTheory.cdf μ)

theorem Grunbaum.measure_cdf_preimage_Iic (μ : MeasureTheory.Measure ℝ) [MeasureTheory.IsProbabilityMeasure μ] [MeasureTheory.NullSingletonClass μ] (u : ℝ) (hu0 : 0 ≤ u) (hu1 : u < 1) : μ (↑(ProbabilityTheory.cdf μ) ⁻¹' Set.Iic u) = ENNReal.ofReal u

noncomputable def Grunbaum.cdfToUnitInterval (μ : MeasureTheory.Measure ℝ) (x : ℝ) : ↑unitInterval

The cumulative distribution function regarded as a map into [0,1].

Equations

• Grunbaum.cdfToUnitInterval μ x = ⟨↑(ProbabilityTheory.cdf μ) x, ⋯⟩

theorem Grunbaum.measurable_cdfToUnitInterval (μ : MeasureTheory.Measure ℝ) [MeasureTheory.IsProbabilityMeasure μ] [MeasureTheory.NullSingletonClass μ] : Measurable (cdfToUnitInterval μ)

theorem Grunbaum.map_cdfToUnitInterval_apply_Iic (μ : MeasureTheory.Measure ℝ) [MeasureTheory.IsProbabilityMeasure μ] [MeasureTheory.NullSingletonClass μ] (u : ↑unitInterval) : (MeasureTheory.Measure.map (cdfToUnitInterval μ) μ) (Set.Iic u) = ENNReal.ofReal ↑u

theorem Grunbaum.Integrable.integral_eq_integral_Ioc_meas_lt' {α : Type u_1} [MeasurableSpace α] {μ : MeasureTheory.Measure α} {f : α → ℝ} {M : ℝ} (f_intble : MeasureTheory.Integrable f μ) (f_nn : 0 ≤ᵐ[μ] f) (f_bdd : f ≤ᵐ[μ] fun (x : α) => M) : ∫ (ω : α), f ω ∂μ = ∫ (t : ℝ) in Set.Ioc 0 M, μ.real {a : α | t < f a}

theorem Grunbaum.integral_cdf_rpow_inv_natCast (μ : MeasureTheory.Measure ℝ) [MeasureTheory.IsProbabilityMeasure μ] [MeasureTheory.NullSingletonClass μ] {n : ℕ} (hn : n ≠ 0) : ∫ (x : ℝ), ↑(ProbabilityTheory.cdf μ) x ^ (↑n)⁻¹ ∂μ = ↑n / (↑n + 1)

theorem Grunbaum.cdf_rpow_inv_natCast_le_at_mean (μ : MeasureTheory.Measure ℝ) [MeasureTheory.IsProbabilityMeasure μ] [MeasureTheory.NullSingletonClass μ] {n : ℕ} (hn : n ≠ 0) (m : ℝ) (hconc : ConcaveOn ℝ (Set.Ici m) fun (x : ℝ) => ↑(ProbabilityTheory.cdf μ) x ^ (↑n)⁻¹) (hsupport : ∀ᵐ (x : ℝ) ∂μ, x ∈ Set.Ici m) (hid : MeasureTheory.Integrable (fun (x : ℝ) => x) μ) : ↑n / (↑n + 1) ≤ ↑(ProbabilityTheory.cdf μ) (∫ (x : ℝ), x ∂μ) ^ (↑n)⁻¹

noncomputable def Grunbaum.uniformVolume {E : Type u_1} [MeasureTheory.MeasureSpace E] (K : Set E) : MeasureTheory.Measure E

Lebesgue volume restricted to K and normalized to total mass one.

Equations

• Grunbaum.uniformVolume K = (MeasureTheory.volume K)⁻¹ • MeasureTheory.volume.restrict K

noncomputable def Grunbaum.volumeCentroid {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] [MeasureTheory.MeasureSpace E] (K : Set E) : E

The centroid of K defined by its set average.

Equations

• Grunbaum.volumeCentroid K = ⨍ (x : E) in K, x

theorem Grunbaum.isProbabilityMeasure_uniformVolume {E : Type u_1} [MeasureTheory.MeasureSpace E] (K : Set E) (hK0 : MeasureTheory.volume K ≠ 0) (hKtop : MeasureTheory.volume K ≠ ⊤) : MeasureTheory.IsProbabilityMeasure (uniformVolume K)

theorem Grunbaum.volumeCentroid_eq_integral_uniformVolume {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] [MeasureTheory.MeasureSpace E] (K : Set E) : volumeCentroid K = ∫ (x : E), x ∂uniformVolume K

theorem Grunbaum.integral_id_map_uniformVolume_eq_centroid_projection {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] [FiniteDimensional ℝ E] [MeasureTheory.MeasureSpace E] [BorelSpace E] [MeasureTheory.volume.IsAddHaarMeasure] (K : Set E) (hK : IsCompact K) (L : E →L[ℝ] ℝ) : ∫ (t : ℝ), t ∂MeasureTheory.Measure.map (⇑L) (uniformVolume K) = L (volumeCentroid K)

theorem Grunbaum.ContinuousLinearMap.map_setAverage {α : Type u_1} {E : Type u_2} {F : Type u_3} [MeasurableSpace α] [NormedAddCommGroup E] [NormedSpace ℝ E] [CompleteSpace E] [NormedAddCommGroup F] [NormedSpace ℝ F] [CompleteSpace F] (L : E →L[ℝ] F) (μ : MeasureTheory.Measure α) (s : Set α) (f : α → E) (hf : MeasureTheory.IntegrableOn f s μ) : L (⨍ (x : α) in s, f x ∂μ) = ⨍ (x : α) in s, L (f x) ∂μ