Stat.Order­Statistic

theorem iid_uniform_cube_law (n : ℕ) : iidSample uniform01 n = volume.restrict (unitCube n) := by change (Measure.pi fun _ : Fin n => volume.restrict (Icc (0 : ℝ) 1)) = _ rw [← Measure.restrict_pi_pi, ← volume_pi] congr 1 ext x simp [unitCube, Pi.le_def, Set.mem_Icc, forall_and]

theorem sorted_cube_law (n : ℕ) : (volume.restrict (unitCube n)).map (sortedSample n) = (n.factorial : ENNReal) • (volume.restrict (orderedUnitRegion n)) := by let s (σ : Perm (Fin n)) : Set (Fin n → ℝ) := {x | x ∈ unitCube n ∧ Monotone (x ∘ σ)} have hs (σ : Perm (Fin n)) : MeasurableSet (s σ) := by have hc : MeasurableSet (unitCube n) := by have heq : unitCube n = ⋂ i, (fun x : Fin n → ℝ => x i) ⁻¹' Icc (0 : ℝ) 1 := by ext x simp [unitCube] rw [heq] exact MeasurableSet.iInter (fun i => measurable_pi_apply i measurableSet_Icc) have hmono : MeasurableSet {x : Fin n → ℝ | Monotone (x ∘ σ)} := by have hcont : Continuous (fun x : Fin n → ℝ => x ∘ σ) := by fun_prop exact (isClosed_monotone.preimage hcont).measurableSet exact hc.inter hmono have hm (σ : Perm (Fin n)) : AEMeasurable (sortedSample n) (volume.restrict (s σ)) := by have hperm : Measurable (fun x : Fin n → ℝ => x ∘ σ) := by fun_prop exact hperm.aemeasurable.congr (ae_restrict_of_forall_mem (hs σ) (fun x hx => (sortedSample_eq_comp_of_monotone n σ x hx.2).symm)) have hsum : AEMeasurable (sortedSample n) (∑ σ : Perm (Fin n), volume.restrict (s σ)) := by rw [← Measure.sum_fintype] exact AEMeasurable.sum_measure hm calc (volume.restrict (unitCube n)).map (sortedSample n) = (∑ σ : Perm (Fin n), volume.restrict (s σ)).map (sortedSample n) := by rw [cube_chamber_decomposition] _ = ∑ σ : Perm (Fin n), (volume.restrict (s σ)).map (sortedSample n) := Measure.map_finset_sum' hsum _ = ∑ _σ : Perm (Fin n), volume.restrict (orderedUnitRegion n) := by simp only [s, permutation_chamber_map] _ = (n.factorial : ENNReal) • (volume.restrict (orderedUnitRegion n)) := by simp [Finset.sum_const, Fintype.card_perm, Nat.cast_smul_eq_nsmul]

theorem orderedSpacings_prefixCoordinates (n : ℕ) (z : Fin n → ℝ) : orderedSpacings n (prefixCoordinates n z) = z := by funext i by_cases hi : i.val = 0 · have hset : Iic i = {i} := by ext j simp only [Finset.mem_Iic, Finset.mem_singleton] constructor · intro hj exact Fin.ext (by omega) · intro h subst j exact le_refl _ simp [orderedSpacings, prefixCoordinates, hi, hset] · have hset : Iic (⟨i.val - 1, by omega⟩ : Fin n) = Finset.Iio i := by ext j simp only [Finset.mem_Iic, Finset.mem_Iio, Fin.le_def, Fin.lt_def] omega have hsum := Finset.sum_Iio_add_eq_sum_Iic (f := z) i rw [← hset] at hsum simp only [orderedSpacings, prefixCoordinates, hi, ↓reduceIte] linarith

theorem prefixCoordinates_orderedSpacings (n : ℕ) (y : Fin n → ℝ) : prefixCoordinates n (orderedSpacings n y) = y := by cases n with | zero => funext i exact elim0 i | succ n => funext i induction i using Fin.induction with | zero => have hset : Iic (0 : Fin (n + 1)) = {0} := by ext j simp only [Finset.mem_Iic, Finset.mem_singleton] exact ⟨fun h => le_antisymm h (bot_le), fun h => h ▸ le_refl _⟩ simp [prefixCoordinates, orderedSpacings, hset] | succ j ih => have hset : Finset.Iio j.succ = Iic j.castSucc := by ext k simp only [Finset.mem_Iio, Finset.mem_Iic, Fin.lt_def, Fin.le_def] simp only [Fin.val_succ, Fin.val_castSucc] omega have hpred : (⟨j.val, by omega⟩ : Fin (n + 1)) = j.castSucc := by ext rfl have hsum := Finset.sum_Iio_add_eq_sum_Iic (f := orderedSpacings (n + 1) y) j.succ rw [hset] at hsum change (∑ k ∈ Iic j.succ, orderedSpacings (n + 1) y k) = y j.succ rw [← hsum, ← prefixCoordinates, ih] simp [orderedSpacings, hpred]

theorem orderedSpacings_preimage_simplex (n : ℕ) : (orderedSpacings n) ⁻¹' spacingSimplex n = orderedUnitRegion n := by ext y simp only [Set.mem_preimage, spacingSimplex, orderedUnitRegion, Set.mem_ofPred_eq] constructor · rintro ⟨hpos, hsum⟩ have hy : prefixCoordinates n (orderedSpacings n y) = y := prefixCoordinates_orderedSpacings n y have hmono : Monotone (prefixCoordinates n (orderedSpacings n y)) := by intro i j hij exact Finset.sum_le_sum_of_subset_of_nonneg (Finset.Iic_subset_Iic.mpr hij) (by intros; exact hpos _) refine ⟨?_, hy ▸ hmono⟩ intro i rw [← hy] constructor · exact Finset.sum_nonneg (fun j _ => hpos j) · exact le_trans (Finset.sum_le_univ_sum_of_nonneg hpos) hsum · rintro ⟨hunit, hmono⟩ constructor · intro i by_cases hi : i.val = 0 · simpa [orderedSpacings, hi] using (hunit i).1 · have hp : (⟨i.val - 1, by omega⟩ : Fin n) ≤ i := by apply Fin.le_def.mpr change i.val - 1 ≤ i.val omega simpa [orderedSpacings, hi] using sub_nonneg.mpr (hmono hp) · cases n with | zero => simp | succ m => have hlast : (Iic (last m)) = univ := by ext i simp only [Finset.mem_Iic, Finset.mem_univ, iff_true] exact Fin.le_last i have h := congrFun (prefixCoordinates_orderedSpacings (m + 1) y) (last m) simp only [prefixCoordinates, hlast] at h rw [h] exact (hunit (last m)).2

theorem orderedSpacingsLinear_apply (n : ℕ) (y : Fin n → ℝ) : orderedSpacingsLinear n y = orderedSpacings n y := by funext i by_cases hi : i.val = 0 · simp [orderedSpacingsLinear, orderedSpacings, hi] · simp [orderedSpacingsLinear, orderedSpacings, hi]

theorem orderedSpacingsLinear_det (n : ℕ) : det (orderedSpacingsLinear n) = 1 := by classical let M := LinearMap.toMatrix' (orderedSpacingsLinear n) have htri : M.IsLowerTriangular := by intro i j hij have hij' : i < j := hij have hj0 : i.val ≠ 0 ∨ i.val = 0 := ne_or_eq _ _ rcases hj0 with hi | hi · simp [M, LinearMap.toMatrix'_apply, orderedSpacingsLinear_apply, orderedSpacings, hi, ne_of_lt hij', show (⟨i.val - 1, by omega⟩ : Fin n) ≠ j from by intro h have := congrArg val h simp at this omega] · simp [M, LinearMap.toMatrix'_apply, orderedSpacingsLinear_apply, orderedSpacings, hi, ne_of_lt hij'] have hdiag (i : Fin n) : M i i = 1 := by by_cases hi : i.val = 0 · simp [M, LinearMap.toMatrix'_apply, orderedSpacingsLinear_apply, orderedSpacings, hi] · have hp : (⟨i.val - 1, by omega⟩ : Fin n) ≠ i := by intro h have := congrArg val h simp at this omega simp [M, LinearMap.toMatrix'_apply, orderedSpacingsLinear_apply, orderedSpacings, hi, hp] rw [← LinearMap.det_toMatrix'] change M.det = 1 rw [Matrix.det_of_isLowerTriangular M htri] simp [hdiag]

theorem orderedSpacings_measurePreserving (n : ℕ) : MeasurePreserving (orderedSpacings n) volume volume := by have hfun : orderedSpacings n = orderedSpacingsLinear n := by funext y exact (orderedSpacingsLinear_apply n y).symm have hmeas : Measurable (orderedSpacings n) := by rw [hfun] exact (orderedSpacingsLinear n).continuous_of_finiteDimensional.measurable refine ⟨hmeas, ?_⟩ rw [hfun] simpa [orderedSpacingsLinear_det n] using (Real.map_linearMap_volume_pi_eq_smul_volume_pi (f := orderedSpacingsLinear n) (by simp [orderedSpacingsLinear_det n]))

theorem orderedSpacings_restrict_law (n : ℕ) : (volume.restrict (orderedUnitRegion n)).map (orderedSpacings n) = volume.restrict (spacingSimplex n) := by have hsimplex : MeasurableSet (spacingSimplex n) := by have hclosed : IsClosed (spacingSimplex n) := by change IsClosed {z : Fin n → ℝ | (∀ i, 0 ≤ z i) ∧ (∑ i, z i) ≤ 1} apply IsClosed.inter · have hp : IsClosed (⋂ i : Fin n, (fun z : Fin n → ℝ => z i) ⁻¹' Ici (0 : ℝ)) := isClosed_iInter (fun i => isClosed_Ici.preimage (continuous_apply i)) have heq : {z : Fin n → ℝ | ∀ i, 0 ≤ z i} = ⋂ i : Fin n, (fun z : Fin n → ℝ => z i) ⁻¹' Ici (0 : ℝ) := by ext z simp change IsClosed (ofPred (fun z : Fin n → ℝ => ∀ i, 0 ≤ z i)) rw [heq] exact hp · exact isClosed_Iic.preimage (continuous_finsetSum _ (fun i _ => (show Continuous (fun z : Fin n → ℝ => z i) from continuous_apply i))) exact hclosed.measurableSet have hmp := orderedSpacings_measurePreserving n rw [← orderedSpacings_preimage_simplex n, ← Measure.restrict_map hmp.measurable hsimplex, hmp.map_eq]

theorem scaledSpacingSimplex_volume (n : ℕ) (r : ℝ) (hr : 0 ≤ r) : volume (scaledSpacingSimplex n r) = ofReal (r ^ n / (n.factorial : ℝ)) := by classical have hsort : AEMeasurable (sortedSample n) (volume : Measure (Fin n → ℝ)) := by let s (σ : Perm (Fin n)) : Set (Fin n → ℝ) := {x | Monotone (x ∘ σ)} have hs (σ : Perm (Fin n)) : MeasurableSet (s σ) := by have hc : Continuous (fun x : Fin n → ℝ => x ∘ σ) := by fun_prop exact (isClosed_monotone.preimage hc).measurableSet have hcover : (⋃ σ, s σ) = univ := by ext x simp only [Set.mem_iUnion, Set.mem_univ, iff_true] exact ⟨Tuple.sort x, Tuple.monotone_sort x⟩ have hpiece (σ : Perm (Fin n)) : AEMeasurable (sortedSample n) (volume.restrict (s σ)) := by have hp : Measurable (fun x : Fin n → ℝ => x ∘ σ) := by fun_prop apply hp.aemeasurable.congr exact ae_restrict_of_forall_mem (hs σ) (fun x hx => (show (fun x => x ∘ σ) x = sortedSample n x from (Tuple.comp_sort_eq_comp_iff_monotone (f := x) (σ := σ)).2 hx)) simpa only [hcover, Measure.restrict_univ] using (AEMeasurable.iUnion hpiece) have hsort' : AEMeasurable (sortedSample n) (iidSample uniform01 n) := by rw [iid_uniform_cube_law] exact hsort.restrict have hspacing : Measurable (orderedSpacings n) := (orderedSpacings_measurePreserving n).measurable have hfirst : AEMeasurable (firstNSpacings n) (iidSample uniform01 n) := by convert hspacing.comp_aemeasurable hsort' using 1 funext x exact firstNSpacings_eq_orderedSpacings n x have hprob : (iidSample uniform01 n) univ = 1 := by haveI : IsProbabilityMeasure uniform01 := ⟨by simp [uniform01]⟩ simp [iidSample] have hunit : volume (spacingSimplex n) = (n.factorial : ENNReal)⁻¹ := by have h := congrArg (fun μ : Measure (Fin n → ℝ) => μ univ) (uniform_firstN_spacings_law n) rw [Measure.map_apply_of_aemeasurable hfirst MeasurableSet.univ] at h simp only [Set.preimage_univ, Measure.smul_apply, Measure.restrict_apply, Set.univ_inter, hprob] at h exact ENNReal.eq_inv_of_mul_eq_one_left (by simpa [mul_comm] using h.symm) have hscale : r • spacingSimplex n = scaledSpacingSimplex n r := by ext z simp only [Set.mem_smul_set, spacingSimplex, scaledSpacingSimplex, Set.mem_ofPred_eq] by_cases hr0 : r = 0 · subst r constructor · rintro ⟨y, _, rfl⟩ simp · rintro ⟨hp, hs⟩ have hz : z = 0 := by funext i have hi : z i ≤ ∑ j, z j := Finset.single_le_sum (fun j _ => hp j) (Finset.mem_univ i) exact le_antisymm (le_trans hi hs) (hp i) subst z refine ⟨0, ?_, by simp⟩ simp [spacingSimplex] · have hrpos : 0 < r := lt_of_le_of_ne hr (Ne.symm hr0) constructor · rintro ⟨y, ⟨hp, hs⟩, rfl⟩ constructor · intro i simpa [Pi.smul_apply, smul_eq_mul] using mul_nonneg hr (hp i) · simpa [Pi.smul_apply, smul_eq_mul, ← Finset.mul_sum] using (mul_le_mul_of_nonneg_left hs hr) · rintro ⟨hp, hs⟩ refine ⟨r⁻¹ • z, ?_, ?_⟩ · constructor · intro i exact smul_nonneg (inv_nonneg.mpr hr) (hp i) · have hs' : (∑ i, (r⁻¹ • z) i) = r⁻¹ * ∑ i, z i := by simp [Pi.smul_apply, smul_eq_mul, Finset.mul_sum] rw [hs'] calc r⁻¹ * ∑ i, z i ≤ r⁻¹ * r := mul_le_mul_of_nonneg_left hs (inv_nonneg.mpr hr) _ = 1 := inv_mul_cancel₀ hr0 · simp [smul_smul, hr0] rw [← hscale, Measure.addHaar_smul, hunit] simp only [Module.finrank_pi, Module.finrank_self, Finset.sum_const_zero, Fintype.card_fin, nsmul_eq_mul, mul_one] rw [abs_of_nonneg (pow_nonneg hr n), ENNReal.ofReal_div_of_pos (by positivity)] simp [ENNReal.ofReal_natCast, div_eq_mul_inv]

theorem simplex_tail_section (n : ℕ) (t : ℝ) (ht : t ∈ Icc (0 : ℝ) 1) : {w : Fin n → ℝ | cons t w ∈ spacingSimplex (n + 1)} = scaledSpacingSimplex n (1 - t) := by ext w simp only [Set.mem_ofPred_eq, spacingSimplex, scaledSpacingSimplex] constructor · rintro ⟨hpos, hsum⟩ constructor · intro i simpa using hpos i.succ · rw [Fin.sum_cons] at hsum linarith · rintro ⟨hpos, hsum⟩ constructor · intro i refine Fin.cases ?_ ?_ i · exact ht.1 · intro j simpa using hpos j · rw [Fin.sum_cons] linarith

theorem simplex_first_coordinate_square_fubini (n : ℕ) : (∫ z in spacingSimplex (n + 1), (z (0 : Fin (n + 1))) ^ 2 ∂volume) = ∫ t in Icc (0 : ℝ) 1, t ^ 2 * (volume (scaledSpacingSimplex n (1 - t))).toReal := by let e : (ℝ × (Fin n → ℝ)) ≃ᵐ (Fin (n + 1) → ℝ) := (piFinSuccAbove (fun _ => ℝ) 0).symm let S : Set (ℝ × (Fin n → ℝ)) := e ⁻¹' spacingSimplex (n + 1) have hem : MeasurePreserving e := (volume_preserving_piFinSuccAbove (fun _ : Fin (n + 1) => ℝ) 0).symm _ have hsimplex : MeasurableSet (spacingSimplex (n + 1)) := by have hclosed : IsClosed (spacingSimplex (n + 1)) := by change IsClosed {z : Fin (n + 1) → ℝ | (∀ i, 0 ≤ z i) ∧ (∑ i, z i) ≤ 1} apply IsClosed.inter · have hp : IsClosed (⋂ i : Fin (n + 1), (fun z : Fin (n + 1) → ℝ => z i) ⁻¹' Ici (0 : ℝ)) := isClosed_iInter (fun i => isClosed_Ici.preimage (continuous_apply i)) have heq : {z : Fin (n + 1) → ℝ | ∀ i, 0 ≤ z i} = ⋂ i : Fin (n + 1), (fun z : Fin (n + 1) → ℝ => z i) ⁻¹' Ici 0 := by ext z simp change IsClosed {z : Fin (n + 1) → ℝ | ∀ i, 0 ≤ z i} rw [heq] exact hp · exact isClosed_Iic.preimage (continuous_finsetSum _ (fun i _ => continuous_apply i)) exact hclosed.measurableSet have hS : MeasurableSet S := hsimplex.preimage e.measurable have hfinite : volume (spacingSimplex (n + 1)) ≠ ⊤ := by change volume (scaledSpacingSimplex (n + 1) 1) ≠ ⊤ rw [scaledSpacingSimplex_volume (n + 1) 1 (by norm_num)] simp have hInt : IntegrableOn (fun z : Fin (n + 1) → ℝ => z 0 ^ 2) (spacingSimplex (n + 1)) volume := by apply Measure.integrableOn_of_bounded hfinite (((measurable_pi_apply 0).pow_const 2).aestronglyMeasurable) (M := 1) apply ae_restrict_of_forall_mem hsimplex intro z hz have h0 : 0 ≤ z 0 := hz.1 0 have hle : z 0 ≤ 1 := by calc z 0 ≤ ∑ i, z i := Finset.single_le_sum (fun i _ => hz.1 i) (Finset.mem_univ 0) _ ≤ 1 := hz.2 rw [Real.norm_eq_abs, abs_of_nonneg (sq_nonneg _)] nlinarith have hpreInt : IntegrableOn (fun p : ℝ × (Fin n → ℝ) => p.1 ^ 2) S ((volume : Measure ℝ).prod volume) := by rw [← Measure.volume_eq_prod] rw [← hem.integrableOn_comp_preimage e.measurableEmbedding] at hInt convert hInt using 1 funext p simp [e, MeasurableEquiv.piFinSuccAbove_symm_apply, Fin.consEquiv] have hprodInt : Integrable (S.indicator (fun p : ℝ × (Fin n → ℝ) => p.1 ^ 2)) ((volume : Measure ℝ).prod volume) := by exact hpreInt.integrable_indicator hS have hsection (t : ℝ) (ht : t ∈ Icc (0 : ℝ) 1) : {w : Fin n → ℝ | (t, w) ∈ S} = scaledSpacingSimplex n (1 - t) := by simpa [S, e, MeasurableEquiv.piFinSuccAbove_symm_apply, Fin.insertNth_zero, Fin.consEquiv] using simplex_tail_section n t ht have hsubset (p : ℝ × (Fin n → ℝ)) (hp : p ∈ S) : p.1 ∈ Icc (0 : ℝ) 1 := by have hp' : cons p.1 p.2 ∈ spacingSimplex (n + 1) := by simpa [S, e, MeasurableEquiv.piFinSuccAbove_symm_apply, Fin.insertNth_zero, Fin.consEquiv] using hp have h0 : 0 ≤ p.1 := hp'.1 0 have hle : p.1 ≤ 1 := by calc p.1 ≤ ∑ i, (cons p.1 p.2) i := by simpa using (Finset.single_le_sum (fun i _ => hp'.1 i) (Finset.mem_univ (0 : Fin (n + 1)))) _ ≤ 1 := hp'.2 exact ⟨h0, hle⟩ have hfiber (t : ℝ) : (∫ w : Fin n → ℝ, S.indicator (fun p : ℝ × (Fin n → ℝ) => p.1 ^ 2) (t, w) ∂volume) = if ht : t ∈ Icc (0 : ℝ) 1 then t ^ 2 * (volume (scaledSpacingSimplex n (1 - t))).toReal else 0 := by split_ifs with ht · have hs : MeasurableSet {w : Fin n → ℝ | (t, w) ∈ S} := hS.preimage measurable_prodMk_left calc _ = ∫ w in {w : Fin n → ℝ | (t, w) ∈ S}, t ^ 2 ∂volume := by rw [← integral_indicator hs] congr 1 _ = t ^ 2 * (volume (scaledSpacingSimplex n (1 - t))).toReal := by rw [setIntegral_const, hsection t ht] simp [measureReal_def, smul_eq_mul, mul_comm] · have hzero : ∀ w : Fin n → ℝ, (t, w) ∉ S := by intro w hw exact ht (hsubset (t, w) hw) simp [indicator, hzero] calc (∫ z in spacingSimplex (n + 1), z 0 ^ 2 ∂volume) = ∫ p in S, p.1 ^ 2 ∂volume := by rw [← hem.map_eq, setIntegral_map_equiv] rfl _ = ∫ p : ℝ × (Fin n → ℝ), S.indicator (fun p : ℝ × (Fin n → ℝ) => p.1 ^ 2) p ∂volume := by rw [integral_indicator hS] _ = ∫ t : ℝ, ∫ w : Fin n → ℝ, S.indicator (fun p : ℝ × (Fin n → ℝ) => p.1 ^ 2) (t, w) ∂volume := by rw [Measure.volume_eq_prod] exact integral_prod _ hprodInt _ = ∫ t in Icc (0 : ℝ) 1, t ^ 2 * (volume (scaledSpacingSimplex n (1 - t))).toReal := by simp_rw [hfiber] rw [← integral_indicator measurableSet_Icc] congr 1 funext t simp [indicator, dite_eq_ite]

theorem simplex_first_coordinate_square_slice (n : ℕ) : (∫ z in spacingSimplex (n + 1), (z (0 : Fin (n + 1))) ^ 2 ∂volume) = ∫ t in (0 : ℝ)..1, t ^ 2 * ((1 - t) ^ n / (n.factorial : ℝ)) := by rw [simplex_first_coordinate_square_fubini, intervalIntegral.integral_of_le (by norm_num : (0 : ℝ) ≤ 1), ← integral_Icc_eq_integral_Ioc] apply setIntegral_congr_fun measurableSet_Icc intro t ht have hr : 0 ≤ 1 - t := sub_nonneg.mpr ht.2 change t ^ 2 * (volume (scaledSpacingSimplex n (1 - t))).toReal = t ^ 2 * ((1 - t) ^ n / (n.factorial : ℝ)) rw [scaledSpacingSimplex_volume n (1 - t) hr] rw [ENNReal.toReal_ofReal (div_nonneg (pow_nonneg hr n) (by positivity))]

theorem unit_beta_square_integral (n : ℕ) : (∫ t in (0 : ℝ)..1, t ^ 2 * (1 - t) ^ n) = 2 * (n.factorial : ℝ) / ((n + 3).factorial : ℝ) := by have hbeta : (∫ t in (0 : ℝ)..1, ((t ^ 2 * (1 - t) ^ n : ℝ) : ℂ)) = Complex.betaIntegral 3 (n + 1) := by rw [Complex.betaIntegral] apply intervalIntegral.integral_congr intro t ht have ht0 : 0 ≤ t := by simpa using ht.1 have ht1 : t ≤ 1 := by simpa using ht.2 dsimp simp only [Complex.ofReal_mul, Complex.ofReal_cpow ht0, Complex.ofReal_pow, Complex.ofReal_sub, Complex.ofReal_one, Complex.cpow_natCast] norm_num have heval := Complex.betaIntegral_eq_Gamma_mul_div 3 (n + 1) (by norm_num) (by simp; positivity) rw [← hbeta] at heval have hg3 : Complex.Gamma 3 = 2 := by convert Complex.Gamma_nat_eq_factorial 2 using 1 <;> norm_num have hgn : Complex.Gamma (n + 1) = (n.factorial : ℂ) := by simpa using Complex.Gamma_nat_eq_factorial n have hgn3 : Complex.Gamma (3 + (n + 1)) = ((n + 3).factorial : ℂ) := by convert Complex.Gamma_nat_eq_factorial (n + 3) using 1 <;> push_cast <;> ring rw [hg3, hgn, hgn3] at heval rw [intervalIntegral.integral_ofReal] at heval exact Complex.ofReal_inj.mp (by simpa using heval)

theorem cdf_continuous_of_withDensity (μ : Measure ℝ) [IsProbabilityMeasure μ] (p : ℝ → ℝ) (hμ : μ = volume.withDensity (fun x => ofReal (p x))) : Continuous (fun x => cdf μ x) := by haveI : NullSingletonClass μ := hμ ▸ inferInstance exact cdf_continuous_of_noAtoms μ

theorem cdf_increment_eq_interval_mass (μ : Measure ℝ) [IsProbabilityMeasure μ] {x y : ℝ} (hxy : x ≤ y) : cdf μ y - cdf μ x = μ.real (Ioc x y) := by rw [ProbabilityTheory.cdf_eq_real, ProbabilityTheory.cdf_eq_real] have hdisj : Disjoint (Iic x) (Ioc x y) := by rw [Set.disjoint_left] intro z hz hz' exact (not_lt_of_ge hz) hz'.1 have hunion : Iic x ∪ Ioc x y = Iic y := by ext z simp only [Set.mem_union, Set.mem_Iic, Set.mem_Ioc] constructor · rintro (hz | ⟨_, hz⟩) · exact hz.trans hxy · exact hz · intro hz exact le_or_gt z x |>.elim (fun h => inl h) (fun h => inr ⟨h, hz⟩) have hadd := measureReal_union hdisj measurableSet_Ioc (μ := μ) (s₁ := Iic x) (s₂ := Ioc x y) rw [hunion] at hadd linarith

theorem sortedSample_map_monotone (n : ℕ) (f : ℝ → ℝ) (hf : Monotone f) (x : Fin n → ℝ) : sortedSample n (fun i => f (x i)) = fun i => f (sortedSample n x i) := by unfold sortedSample have hmono : Monotone ((fun j : Fin n => f (x j)) ∘ sort x) := hf.comp (Tuple.monotone_sort x) exact ((Tuple.comp_sort_eq_comp_iff_monotone (f := fun j : Fin n => f (x j)) (σ := sort x)).2 hmono).symm

theorem cdf_pushforward_uniform01 (μ : Measure ℝ) [IsProbabilityMeasure μ] (p : ℝ → ℝ) (hμ : μ = volume.withDensity (fun x => ofReal (p x))) : μ.map (fun x => cdf μ x) = uniform01 := by exact cdf_pushforward_of_continuous μ (cdf_continuous_of_withDensity μ p hμ)

theorem cdf_increment_bounds (μ : Measure ℝ) [IsProbabilityMeasure μ] (a b cg Cg : ℝ) (p : ℝ → ℝ) (hcg : 0 < cg) (hCg : cg ≤ Cg) (hμ : μ = volume.withDensity (fun x => ofReal (p x))) (hbound : ∀ᵐ x ∂(volume.restrict (Icc a b)), cg ≤ p x ∧ p x ≤ Cg) {x y : ℝ} (hax : a ≤ x) (hxy : x ≤ y) (hyb : y ≤ b) : cg * (y - x) ≤ cdf μ y - cdf μ x ∧ cdf μ y - cdf μ x ≤ Cg * (y - x) := by rw [cdf_increment_eq_interval_mass μ hxy] exact withDensity_interval_mass_bounds μ a b cg Cg p hcg hCg hμ hbound hax hxy hyb

theorem iid_cdf_pushforward_uniform01 (μ : Measure ℝ) [IsProbabilityMeasure μ] (p : ℝ → ℝ) (hμ : μ = volume.withDensity (fun x => ofReal (p x))) (n : ℕ) : (iidSample μ n).map (fun x i => cdf μ (x i)) = iidSample uniform01 n := by have hc := cdf_continuous_of_withDensity μ p hμ have hmap := cdf_pushforward_uniform01 μ p hμ haveI : IsProbabilityMeasure (μ.map (fun x => cdf μ x)) := Measure.isProbabilityMeasure_map hc.measurable.aemeasurable change (Measure.pi (fun _ : Fin n => μ)).map (fun x i => cdf μ (x i)) = Measure.pi (fun _ : Fin n => uniform01) rw [Measure.pi_map_pi (fun _ : Fin n => hc.measurable.aemeasurable)] simp only [hmap]

theorem iid_support_interval_ae (μ : Measure ℝ) [IsProbabilityMeasure μ] (a b : ℝ) (hsupp : μ (Icc a b)ᶜ = 0) (n : ℕ) : ∀ᵐ x ∂iidSample μ n, ∀ i, x i ∈ Icc a b := by have hcoord : ∀ᵐ y ∂μ, y ∈ Icc a b := mem_ae_iff.mpr hsupp change ∀ᵐ x ∂Measure.pi (fun _ : Fin n => μ), ∀ i, x i ∈ Icc a b exact Filter.eventually_all.mpr (fun i => Measure.tendsto_eval_ae_ae.eventually hcoord)

theorem sortedGap_square_integrable_of_interval_support (μ : Measure ℝ) [IsProbabilityMeasure μ] (a b : ℝ) (hsupp : μ (Icc a b)ᶜ = 0) (n k : ℕ) (hk : k + 1 < n) : Integrable (fun x => (sortedGap n k x) ^ 2) (iidSample μ n) := by classical let lo : Fin n := ⟨k, by omega⟩ let hi : Fin n := ⟨k + 1, hk⟩ have hsort : AEMeasurable (sortedSample n) (iidSample μ n) := by let s (σ : Perm (Fin n)) : Set (Fin n → ℝ) := {x | Monotone (x ∘ σ)} have hs (σ : Perm (Fin n)) : MeasurableSet (s σ) := by have hc : Continuous (fun x : Fin n → ℝ => x ∘ σ) := by fun_prop exact (isClosed_monotone.preimage hc).measurableSet have hcover : (⋃ σ, s σ) = univ := by ext x simp only [Set.mem_iUnion, Set.mem_univ, iff_true] exact ⟨Tuple.sort x, Tuple.monotone_sort x⟩ have hpiece (σ : Perm (Fin n)) : AEMeasurable (sortedSample n) ((iidSample μ n).restrict (s σ)) := by have hp : Measurable (fun x : Fin n → ℝ => x ∘ σ) := by fun_prop apply hp.aemeasurable.congr exact ae_restrict_of_forall_mem (hs σ) (fun x hx => (show (fun x => x ∘ σ) x = sortedSample n x from (Tuple.comp_sort_eq_comp_iff_monotone (f := x) (σ := σ)).2 hx)) simpa only [hcover, Measure.restrict_univ] using (AEMeasurable.iUnion hpiece) have hmeas : AEStronglyMeasurable (fun x => (sortedGap n k x) ^ 2) (iidSample μ n) := by have hp : Measurable (fun y : Fin n → ℝ => (y hi - y lo) ^ 2) := by fun_prop have h := hp.aestronglyMeasurable.comp_aemeasurable hsort convert h using 1 funext x simp [sortedGap, hk, sortedSample, lo, hi] have hfinite : (iidSample μ n) univ ≠ ⊤ := by simp [iidSample] have hbound : ∀ᵐ x ∂iidSample μ n, ‖(sortedGap n k x) ^ 2‖ ≤ (b - a) ^ 2 := by filter_upwards [iid_support_interval_ae μ a b hsupp n] with x hx have hmono : sortedSample n x lo ≤ sortedSample n x hi := (Tuple.monotone_sort x) (by simp [lo, hi, Fin.le_def]) have hlo : a ≤ sortedSample n x lo := (hx (sort x lo)).1 have hhi : sortedSample n x hi ≤ b := (hx (sort x hi)).2 have hgap : sortedGap n k x = sortedSample n x hi - sortedSample n x lo := by simp [sortedGap, hk, lo, hi] have hg0 : 0 ≤ sortedGap n k x := by rw [hgap]; linarith have hgle : sortedGap n k x ≤ b - a := by rw [hgap]; linarith rw [Real.norm_eq_abs, abs_of_nonneg (sq_nonneg _)] exact (sq_le_sq₀ hg0 (by linarith)).2 hgle exact integrableOn_univ.mp (Measure.integrableOn_of_bounded hfinite hmeas (by simpa only [Measure.restrict_univ] using hbound) : IntegrableOn (fun x => (sortedGap n k x) ^ 2) univ (iidSample μ n))

theorem sortedGap_cdf_linear_bounds (μ : Measure ℝ) [IsProbabilityMeasure μ] (a b cg Cg : ℝ) (p : ℝ → ℝ) (hcg : 0 < cg) (hCg : cg ≤ Cg) (hμ : μ = volume.withDensity (fun x => ofReal (p x))) (hbound : ∀ᵐ x ∂(volume.restrict (Icc a b)), cg ≤ p x ∧ p x ≤ Cg) (n k : ℕ) (hk : k + 1 < n) (x : Fin n → ℝ) (hx : ∀ i, x i ∈ Icc a b) : cg * sortedGap n k x ≤ sortedGap n k (fun i => cdf μ (x i)) ∧ sortedGap n k (fun i => cdf μ (x i)) ≤ Cg * sortedGap n k x := by let lo : Fin n := ⟨k, by omega⟩ let hi : Fin n := ⟨k + 1, hk⟩ have hxy : sortedSample n x lo ≤ sortedSample n x hi := (Tuple.monotone_sort x) (by simp [lo, hi, Fin.le_def]) have hax : a ≤ sortedSample n x lo := (hx (sort x lo)).1 have hyb : sortedSample n x hi ≤ b := (hx (sort x hi)).2 have hinc := cdf_increment_bounds μ a b cg Cg p hcg hCg hμ hbound hax hxy hyb have hsort := sortedSample_map_monotone n (fun z => cdf μ z) (ProbabilityTheory.monotone_cdf μ) x simpa only [sortedGap, dif_pos hk, lo, hi, hsort] using hinc

theorem sortedGap_cdf_square_bounds (μ : Measure ℝ) [IsProbabilityMeasure μ] (a b cg Cg : ℝ) (p : ℝ → ℝ) (hcg : 0 < cg) (hCg : cg ≤ Cg) (hμ : μ = volume.withDensity (fun x => ofReal (p x))) (hbound : ∀ᵐ x ∂(volume.restrict (Icc a b)), cg ≤ p x ∧ p x ≤ Cg) (n k : ℕ) (hk : k + 1 < n) (x : Fin n → ℝ) (hx : ∀ i, x i ∈ Icc a b) : cg ^ 2 * (sortedGap n k x) ^ 2 ≤ (sortedGap n k (fun i => cdf μ (x i))) ^ 2 ∧ (sortedGap n k (fun i => cdf μ (x i))) ^ 2 ≤ Cg ^ 2 * (sortedGap n k x) ^ 2 := by have hmono := Tuple.monotone_sort x have hg0 : 0 ≤ sortedGap n k x := by simp only [sortedGap, dif_pos hk] exact sub_nonneg.mpr (hmono (by simp [Fin.le_def])) have hlin := sortedGap_cdf_linear_bounds μ a b cg Cg p hcg hCg hμ hbound n k hk x hx have hcg0 : 0 ≤ cg * sortedGap n k x := mul_nonneg hcg.le hg0 have hCg0 : 0 ≤ Cg * sortedGap n k x := mul_nonneg (le_trans hcg.le hCg) hg0 have hfg0 : 0 ≤ sortedGap n k (fun i => cdf μ (x i)) := le_trans hcg0 hlin.1 have hlow := (sq_le_sq₀ hcg0 hfg0).2 hlin.1 have hupp := (sq_le_sq₀ hfg0 hCg0).2 hlin.2 constructor <;> nlinarith [hlow, hupp]

theorem cdf_transformed_gap_second_moment (μ : Measure ℝ) [IsProbabilityMeasure μ] (n k : ℕ) (hk : k + 1 < n) (hcont : Continuous (cdf μ)) (hmap : (iidSample μ n).map (fun x i => cdf μ (x i)) = iidSample uniform01 n) : ∫ x, (sortedGap n k (fun i => cdf μ (x i))) ^ 2 ∂iidSample μ n = (2 : ℝ) / ((n + 1 : ℕ) * (n + 2 : ℕ)) := by -- Use integral_map for the coordinatewise CDF. The gap function is -- a.e. strongly measurable under the uniform product law because it is -- integrable there; the uniform law lives on the unit cube. have hmeas : Measurable (fun x : Fin n → ℝ => fun i => cdf μ (x i)) := measurable_pi_lambda _ fun i => hcont.measurable.comp (measurable_pi_apply i) have hstrong : AEStronglyMeasurable (fun x => (sortedGap n k x) ^ 2) (iidSample uniform01 n) := (uniform_gap_square_integrable n k hk).aestronglyMeasurable rw [← hmap] at hstrong rw [← integral_map hmeas.aemeasurable hstrong, hmap] exact uniform_gap_second_moment n k hk

theorem real_gap_second_moment_bounds (μ : Measure ℝ) [IsProbabilityMeasure μ] (a b cg Cg : ℝ) (p : ℝ → ℝ) (hcg : 0 < cg) (hCg : cg ≤ Cg) (hμ : μ = volume.withDensity (fun x => ofReal (p x))) (hsupp : μ (Icc a b)ᶜ = 0) (hbound : ∀ᵐ x ∂(volume.restrict (Icc a b)), cg ≤ p x ∧ p x ≤ Cg) (n k : ℕ) (hk : k + 1 < n) : (1 / Cg ^ 2) * ((2 : ℝ) / ((n + 1 : ℕ) * (n + 2 : ℕ))) ≤ ∫ x, (sortedGap n k x) ^ 2 ∂iidSample μ n ∧ (∫ x, (sortedGap n k x) ^ 2 ∂iidSample μ n) ≤ (1 / cg ^ 2) * ((2 : ℝ) / ((n + 1 : ℕ) * (n + 2 : ℕ))) := by let F : (Fin n → ℝ) → (Fin n → ℝ) := fun x i => cdf μ (x i) have hcont := cdf_continuous_of_withDensity μ p hμ have hmap := iid_cdf_pushforward_uniform01 μ p hμ n have hmeas : Measurable F := measurable_pi_lambda _ fun i => hcont.measurable.comp (measurable_pi_apply i) have horig : Integrable (fun x => (sortedGap n k x) ^ 2) (iidSample μ n) := sortedGap_square_integrable_of_interval_support μ a b hsupp n k hk have htrans : Integrable (fun x => (sortedGap n k (F x)) ^ 2) (iidSample μ n) := by have hu := uniform_gap_square_integrable n k hk rw [← hmap] at hu simpa only [Function.comp_def] using hu.comp_measurable hmeas have hpoint : ∀ᵐ x ∂iidSample μ n, cg ^ 2 * (sortedGap n k x) ^ 2 ≤ (sortedGap n k (F x)) ^ 2 ∧ (sortedGap n k (F x)) ^ 2 ≤ Cg ^ 2 * (sortedGap n k x) ^ 2 := by filter_upwards [iid_support_interval_ae μ a b hsupp n] with x hx exact sortedGap_cdf_square_bounds μ a b cg Cg p hcg hCg hμ hbound n k hk x hx have hlow : cg ^ 2 * (∫ x, (sortedGap n k x) ^ 2 ∂iidSample μ n) ≤ ∫ x, (sortedGap n k (F x)) ^ 2 ∂iidSample μ n := by rw [← integral_const_mul] exact integral_mono_ae (horig.const_mul _) htrans (hpoint.mono fun x hx => hx.1) have hupp : (∫ x, (sortedGap n k (F x)) ^ 2 ∂iidSample μ n) ≤ Cg ^ 2 * (∫ x, (sortedGap n k x) ^ 2 ∂iidSample μ n) := by rw [← integral_const_mul] exact integral_mono_ae htrans (horig.const_mul _) (hpoint.mono fun x hx => hx.2) have hmoment := cdf_transformed_gap_second_moment μ n k hk hcont hmap change (∫ x, (sortedGap n k (F x)) ^ 2 ∂iidSample μ n) = _ at hmoment rw [hmoment] at hlow hupp have hcg2 : 0 < cg ^ 2 := sq_pos_of_pos hcg have hCg2 : 0 < Cg ^ 2 := sq_pos_of_pos (lt_of_lt_of_le hcg hCg) constructor · have h : ((2 : ℝ) / ((n + 1 : ℕ) * (n + 2 : ℕ))) / Cg ^ 2 ≤ ∫ x, (sortedGap n k x) ^ 2 ∂iidSample μ n := (div_le_iff₀ hCg2).2 (by simpa only [mul_comm] using hupp) simpa only [one_div, div_eq_mul_inv, mul_comm, one_mul, mul_one] using h · have h : (∫ x, (sortedGap n k x) ^ 2 ∂iidSample μ n) ≤ ((2 : ℝ) / ((n + 1 : ℕ) * (n + 2 : ℕ))) / cg ^ 2 := (le_div_iff₀ hcg2).2 (by simpa only [mul_comm] using hlow) simpa only [one_div, div_eq_mul_inv, mul_comm, one_mul, mul_one] using h

theorem simplex_coordinate_second_moment (n : ℕ) (i : Fin n) : (n.factorial : ℝ) * (∫ z in spacingSimplex n, (z i) ^ 2 ∂volume) = (2 : ℝ) / ((n + 1 : ℕ) * (n + 2 : ℕ)) := by cases n with | zero => exact elim0 i | succ m => rw [simplex_coordinate_square_eq_first] change (m + 1).factorial * (∫ z in spacingSimplex (m + 1), (z (0 : Fin (m + 1))) ^ 2 ∂volume) = _ rw [simplex_first_coordinate_square_slice] have hfactorial : (m + 1).factorial = (m + 1) * m.factorial := Nat.factorial_succ m simp_rw [← mul_div_assoc] rw [intervalIntegral.integral_div] rw [unit_beta_square_integral] norm_num [hfactorial, Nat.factorial_succ] have hm : (m.factorial : ℝ) ≠ 0 := by positivity field_simp ring

theorem uniform_gap_second_moment (n k : ℕ) (hk : k + 1 < n) : ∫ x, (sortedGap n k x) ^ 2 ∂iidSample uniform01 n = (2 : ℝ) / ((n + 1 : ℕ) * (n + 2 : ℕ)) := by have hfirst := firstNSpacings_aemeasurable n let i : Fin n := ⟨k + 1, hk⟩ have hgap (x : Fin n → ℝ) : sortedGap n k x = firstNSpacings n x i := by simp [sortedGap, firstNSpacings, i, hk] calc (∫ x, (sortedGap n k x) ^ 2 ∂iidSample uniform01 n) = ∫ z, (z i) ^ 2 ∂(iidSample uniform01 n).map (firstNSpacings n) := by rw [integral_map hfirst ((measurable_pi_apply i).pow_const 2).aestronglyMeasurable] simp only [hgap] _ = (n.factorial : ℝ) * (∫ z in spacingSimplex n, (z i) ^ 2 ∂volume) := by rw [uniform_firstN_spacings_law, integral_smul_measure] simp _ = _ := simplex_coordinate_second_moment n i

theorem uniform_gap_square_integrable (n k : ℕ) (hk : k + 1 < n) : Integrable (fun x => (sortedGap n k x) ^ 2) (iidSample uniform01 n) := by let i : Fin n := ⟨k + 1, hk⟩ have hgap (x : Fin n → ℝ) : sortedGap n k x = firstNSpacings n x i := by simp [sortedGap, firstNSpacings, i, hk] have hmeas : AEStronglyMeasurable (fun x => (sortedGap n k x) ^ 2) (iidSample uniform01 n) := by have h := ((measurable_pi_apply i).pow_const 2).aestronglyMeasurable.comp_aemeasurable (firstNSpacings_aemeasurable n) convert h using 1 funext x simp [hgap] have hfinite : (iidSample uniform01 n) univ ≠ ⊤ := by have : IsProbabilityMeasure uniform01 := ⟨by simp [uniform01]⟩ simp [iidSample] have hcube : MeasurableSet (unitCube n) := by change MeasurableSet {x : Fin n → ℝ | ∀ i, x i ∈ Icc (0 : ℝ) 1} have heq : {x : Fin n → ℝ | ∀ i, x i ∈ Icc (0 : ℝ) 1} = ⋂ i : Fin n, (fun x : Fin n → ℝ => x i) ⁻¹' Icc 0 1 := by ext x simp rw [heq] exact MeasurableSet.iInter (fun i => measurableSet_Icc.preimage (measurable_pi_apply i)) have hbound : ∀ᵐ x ∂iidSample uniform01 n, ‖(sortedGap n k x) ^ 2‖ ≤ (1 : ℝ) := by rw [iid_uniform_cube_law] apply ae_restrict_of_forall_mem hcube intro x hx have hmono : Monotone (sortedSample n x) := Tuple.monotone_sort x have h0 : 0 ≤ sortedSample n x ⟨k, by omega⟩ := (hx (sort x ⟨k, by omega⟩)).1 have h1 : sortedSample n x i ≤ 1 := (hx (sort x i)).2 have hle : sortedSample n x ⟨k, by omega⟩ ≤ sortedSample n x i := hmono (by simp [i, Fin.le_def]) have hgap' : sortedGap n k x = sortedSample n x i - sortedSample n x ⟨k, by omega⟩ := by simp [sortedGap, hk, i] have hb : 0 ≤ sortedGap n k x ∧ sortedGap n k x ≤ 1 := by rw [hgap'] constructor <;> linarith rw [Real.norm_eq_abs, abs_of_nonneg (sq_nonneg _)] nlinarith exact integrableOn_univ.mp (Measure.integrableOn_of_bounded hfinite hmeas (by simpa only [Measure.restrict_univ] using hbound) : IntegrableOn (fun x => (sortedGap n k x) ^ 2) univ (iidSample uniform01 n))