Stat.Order­Statistic.Weighted­Concomitant

theorem integral_bernsteinCell {N : ℕ} (hN : 0 < N) (a : Fin N → ℝ) (hsum : ∑ j : Fin N, a j = 1) : ∫ u in Icc (0 : ℝ) 1, bernsteinCell N a u ∂volume = 1 := by have hint (j : Fin N) : IntegrableOn (fun u : ℝ => a j * ((N : ℝ) * (choose (N - 1) (j : ℕ) : ℝ) * u ^ (j : ℕ) * (1 - u) ^ (N - 1 - (j : ℕ)))) (Icc (0 : ℝ) 1) volume := by apply Continuous.integrableOn_Icc fun_prop calc (∫ u in Icc (0 : ℝ) 1, bernsteinCell N a u ∂volume) = ∫ u in Icc (0 : ℝ) 1, ∑ j : Fin N, a j * ((N : ℝ) * (choose (N - 1) (j : ℕ) : ℝ) * u ^ (j : ℕ) * (1 - u) ^ (N - 1 - (j : ℕ))) ∂volume := by congr 1 funext u simp only [bernsteinCell, Finset.mul_sum] apply Finset.sum_congr rfl intro j hj ring _ = ∑ j : Fin N, a j := by rw [integral_finsetSum (s := univ) (fun j hj => hint j)] apply Finset.sum_congr rfl intro j hj rw [integral_const_mul, integral_bernstein_basis hN j, mul_one] _ = 1 := hsum

theorem uniform_tagged_rank_cell_integral {N : ℕ} (hN : 0 < N) (i j : Fin N) (f : ℝ → ℝ) (hf : AEMeasurable f uniform01) (hbound : ∀ᵐ u ∂uniform01, |f u| ≤ 1) : (∫ u, (if (sort u).symm i = j then f (u i) else 0) ∂iidSample uniform01 N) = ∫ v in Icc (0 : ℝ) 1, f v * ((Nat.choose (N - 1) j.val : ℝ) * v ^ j.val * (1 - v) ^ (N - 1 - j.val)) ∂volume := by classical haveI : IsProbabilityMeasure uniform01 := ⟨by simp [uniform01]⟩ let g := hf.mk f have hg : Measurable g := hf.measurable_mk have hfg : f =ᵐ[uniform01] g := hf.ae_eq_mk have hgbound : ∀ᵐ v ∂uniform01, |g v| ≤ 1 := by filter_upwards [hbound, hfg] with v hv heq simpa only [← heq] using hv have hmain (g : ℝ → ℝ) (hg : Measurable g) (hgbound : ∀ᵐ v ∂uniform01, |g v| ≤ 1) : (∫ u, (if (sort u).symm i = j then g (u i) else 0) ∂iidSample uniform01 N) = ∫ v in Icc (0 : ℝ) 1, g v * ((Nat.choose (N - 1) j.val : ℝ) * v ^ j.val * (1 - v) ^ (N - 1 - j.val)) ∂volume := by cases N with | zero => omega | succ n => let ν : Measure (Fin (n + 1) → ℝ) := Measure.pi (fun _ => uniform01) let ρ : Measure (Fin n → ℝ) := Measure.pi (fun _ => uniform01) let e := piFinSuccAbove (fun _ : Fin (n + 1) => ℝ) i let A (v : ℝ) : Set (Fin n → ℝ) := {w | ((Finset.univ : Finset (Fin n)).filter (fun k => w k < v)).card = j.val} let C : Set (Fin (n + 1) → ℝ) := {u | (((Finset.univ : Finset (Fin (n + 1))).erase i).filter (fun k => u k < u i)).card = j.val} have hcount (v : ℝ) (u : Fin (n + 1) → ℝ) : (((Finset.univ : Finset (Fin (n + 1))).erase i).filter (fun k => u k < v)).card = ((Finset.univ : Finset (Fin n)).filter (fun k => i.removeNth u k < v)).card := by have hindex : ((Finset.univ : Finset (Fin (n + 1))).erase i) = (Finset.univ : Finset (Fin n)).image i.succAbove := by ext k simp only [Finset.mem_erase, Finset.mem_univ, and_true, mem_image, Finset.mem_univ, true_and] rw [← Set.mem_range] simp [Fin.range_succAbove] rw [hindex, Finset.filter_image, Finset.card_image_of_injective] · rfl · exact Fin.succAbove_right_injective have hA (v : ℝ) : MeasurableSet (A v) := by dsimp [A] apply measurableSet_eq_fun · simp_rw [Finset.card_filter] apply Finset.measurable_sum intro k _ apply Measurable.ite · exact measurableSet_lt (measurable_pi_apply k) measurable_const · exact measurable_const · exact measurable_const · exact measurable_const have hC : MeasurableSet C := by dsimp [C] apply measurableSet_eq_fun · simp_rw [Finset.card_filter] apply Finset.measurable_sum intro k _ apply Measurable.ite · exact measurableSet_lt (measurable_pi_apply k) (measurable_pi_apply i) · exact measurable_const · exact measurable_const · exact measurable_const have hmass (v : ℝ) (hv : v ∈ Icc (0 : ℝ) 1) : ρ (A v) = ofReal ((Nat.choose n j.val : ℝ) * v ^ j.val * (1 - v) ^ (n - j.val)) := by let B : Set (Fin (n + 1) → ℝ) := {u | (((Finset.univ : Finset (Fin (n + 1))).erase i).filter (fun k => u k < v)).card = j.val} have hB : B = e ⁻¹' (univ ×ˢ A v) := by ext u simp only [Set.mem_preimage, Set.mem_prod, Set.mem_univ, true_and] change (((Finset.univ : Finset (Fin (n + 1))).erase i).filter (fun k => u k < v)).card = j.val ↔ ((Finset.univ : Finset (Fin n)).filter (fun k => i.removeNth u k < v)).card = j.val rw [hcount] have he := measurePreserving_piFinSuccAbove (fun _ : Fin (n + 1) => uniform01) i have hBmass : ρ (A v) = ν B := by rw [hB, he.measure_preimage ((MeasurableSet.univ.prod (hA v)).nullMeasurableSet)] rw [Measure.prod_prod] simp [ρ] simpa [ν, ρ, B] using hBmass.trans (uniform_other_lt_count_mass i j hv) let F : (Fin (n + 1) → ℝ) → ℝ := fun u => if u ∈ C then g (u i) else 0 have hFmeas : Measurable F := by apply Measurable.ite hC · exact hg.comp (measurable_pi_apply i) · exact measurable_const have hpi_bound : ∀ᵐ u ∂ν, |g (u i)| ≤ 1 := by have hmap : ν.map (fun u => u i) = uniform01 := by exact (measurePreserving_eval (fun _ : Fin (n + 1) => uniform01) i).map_eq exact ae_of_ae_map (μ := ν) (f := fun u : Fin (n + 1) → ℝ => u i) (p := fun v => |g v| ≤ 1) (measurable_pi_apply i).aemeasurable (by simpa [hmap] using hgbound) have hFint : Integrable F ν := by apply Integrable.of_bound hFmeas.aestronglyMeasurable 1 filter_upwards [hpi_bound] with u hu by_cases hc : u ∈ C · simpa [F, hc, Real.norm_eq_abs] using hu · simp [F, hc] have hrank : (fun u : Fin (n + 1) → ℝ => if (sort u).symm i = j then g (u i) else 0) =ᵐ[ν] F := by filter_upwards [iid_uniform_coordinates_injective_ae (N := n + 1)] with u hu have hiff : (sort u).symm i = j ↔ u ∈ C := by change (sort u).symm i = j ↔ (((Finset.univ : Finset (Fin (n + 1))).erase i).filter (fun k => u k < u i)).card = j.val rw [← uniform_tagged_rank_eq_count u i hu] exact Fin.ext_iff simp only [F, hiff] have he := measurePreserving_piFinSuccAbove (fun _ : Fin (n + 1) => uniform01) i have hcomp : (fun z => F (e.symm z)) ∘ e = F := by funext u simp have hsplit : (∫ u, F u ∂ν) = ∫ v, ∫ w : Fin n → ℝ, F (e.symm (v, w)) ∂ρ ∂uniform01 := by calc _ = ∫ z : ℝ × (Fin n → ℝ), F (e.symm z) ∂uniform01.prod ρ := by have hh := he.integral_comp' (fun z => F (e.symm z)) change (∫ u, ((fun z => F (e.symm z)) ∘ e) u ∂ν) = _ at hh rw [hcomp] at hh exact hh _ = _ := by apply integral_prod apply (he.integrable_comp_emb e.measurableEmbedding).mp change Integrable (((fun z => F (e.symm z)) ∘ e)) ν rw [hcomp] exact hFint have hinner (v : ℝ) : (∫ w : Fin n → ℝ, (if w ∈ A v then g v else 0) ∂ρ) = (ρ (A v)).toReal * g v := by simpa [indicator, Measure.real, smul_eq_mul] using (integral_indicator_const (g v) (hA v) (μ := ρ)) have hfiber (v : ℝ) (w : Fin n → ℝ) : F (e.symm (v, w)) = if w ∈ A v then g v else 0 := by have heval : (e.symm (v, w)) i = v := by simp [e] have hrem : i.removeNth (e.symm (v, w)) = w := by have hh := congrArg snd (e.apply_symm_apply (v, w)) exact hh simp only [F] change (if (((Finset.univ : Finset (Fin (n + 1))).erase i).filter (fun k => (e.symm (v, w)) k < (e.symm (v, w)) i)).card = j.val then g ((e.symm (v, w)) i) else 0) = if ((Finset.univ : Finset (Fin n)).filter (fun k => w k < v)).card = j.val then g v else 0 rw [heval, hcount v (e.symm (v, w)), hrem] have hkernel_nonneg (v : ℝ) (hv : v ∈ Icc (0 : ℝ) 1) : 0 ≤ (Nat.choose n j.val : ℝ) * v ^ j.val * (1 - v) ^ (n - j.val) := by have hv0 : 0 ≤ v := hv.1 have hv1 : 0 ≤ 1 - v := sub_nonneg.mpr hv.2 positivity calc (∫ u, (if (sort u).symm i = j then g (u i) else 0) ∂iidSample uniform01 (n + 1)) = ∫ u, F u ∂ν := by exact integral_congr_ae hrank _ = ∫ v, ∫ w : Fin n → ℝ, F (e.symm (v, w)) ∂ρ ∂uniform01 := hsplit _ = ∫ v, (ρ (A v)).toReal * g v ∂uniform01 := by congr 1 funext v simp_rw [hfiber] exact hinner v _ = ∫ v, g v * ((Nat.choose n j.val : ℝ) * v ^ j.val * (1 - v) ^ (n - j.val)) ∂uniform01 := by apply integral_congr_ae filter_upwards [ae_restrict_mem measurableSet_Icc] with v hv rw [hmass v hv, ENNReal.toReal_ofReal (hkernel_nonneg v hv)] ring _ = _ := by simp only [uniform01, Nat.succ_sub_one] calc (∫ u, (if (sort u).symm i = j then f (u i) else 0) ∂iidSample uniform01 N) = ∫ u, (if (sort u).symm i = j then g (u i) else 0) ∂iidSample uniform01 N := by apply integral_congr_ae have hmap : (iidSample uniform01 N).map (fun u => u i) = uniform01 := (measurePreserving_eval (fun _ : Fin N => uniform01) i).map_eq have hcomp : ∀ᵐ u ∂iidSample uniform01 N, f (u i) = g (u i) := by exact ae_of_ae_map (μ := iidSample uniform01 N) (f := fun u : Fin N → ℝ => u i) (p := fun v => f v = g v) (measurable_pi_apply i).aemeasurable (by rw [hmap]; exact hfg) filter_upwards [hcomp] with u hu split_ifs <;> simp [hu] _ = ∫ v in Icc (0 : ℝ) 1, g v * ((Nat.choose (N - 1) j.val : ℝ) * v ^ j.val * (1 - v) ^ (N - 1 - j.val)) ∂volume := hmain g hg hgbound _ = _ := by apply integral_congr_ae have hfg' : f =ᵐ[volume.restrict (Icc (0 : ℝ) 1)] g := by simpa only [uniform01] using hfg filter_upwards [hfg'] with v hv simp [hv]

theorem adjacentOrderMix_indicator_L1 {N k : ℕ} (hN : 0 < N) (hk : k < N) {δ : ℝ} (hδ : δ ∈ Icc (0 : ℝ) 1) : (∫ u in Icc (0 : ℝ) 1, |((adjacentOrderMix N k δ) (Iic u)).toReal - (if (k + δ) / N ≤ u then (1 : ℝ) else 0)| ∂volume) ≤ sqrt (((k + δ) / N) * (1 - (k + δ) / N) / (N + 1) + δ * (1 - δ) / (N * (N + 1))) := by haveI : IsProbabilityMeasure uniform01 := ⟨by simp [uniform01]⟩ haveI : IsProbabilityMeasure (iidSample uniform01 (N - 1)) := by dsimp [iidSample] infer_instance let μ := adjacentOrderMix N k δ have hmass : (∫ _u : ℝ, (1 : ℝ) ∂μ) = 1 := by have hmap (r : ℕ) : (∫ _u : ℝ, (1 : ℝ) ∂(iidSample uniform01 (N - 1)).map (orderEndpoint (N - 1) r)) = 1 := by rw [integral_map (orderEndpoint_aemeasurable (N - 1) r) measurable_const.aestronglyMeasurable] simp change (∫ _u : ℝ, (1 : ℝ) ∂adjacentOrderMix N k δ) = 1 rw [adjacentOrderMix_integral hN hk hδ (fun _ : ℝ => (1 : ℝ)) (integrable_const _) (integrable_const _), hmap k, hmap (k + 1)] ring haveI : IsProbabilityMeasure μ := by have hreal : (μ univ).toReal = 1 := by simpa [integral_const, Measure.real] using hmass exact isProbabilityMeasure_iff_real.mpr hreal have hsupp : ∀ᵐ x ∂μ, x ∈ Icc (0 : ℝ) 1 := by change ∀ᵐ x ∂adjacentOrderMix N k δ, x ∈ Icc (0 : ℝ) 1 rw [adjacentOrderMix_eq_endpoints hN hk, ae_add_measure_iff] constructor · exact Measure.ae_smul_measure ((ae_map_iff (orderEndpoint_aemeasurable (N - 1) k) measurableSet_Icc).2 (orderEndpoint_mem_Icc (N - 1) k)) _ · exact Measure.ae_smul_measure ((ae_map_iff (orderEndpoint_aemeasurable (N - 1) (k + 1)) measurableSet_Icc).2 (orderEndpoint_mem_Icc (N - 1) (k + 1))) _ have ht : (k + δ) / N ∈ Icc (0 : ℝ) 1 := by have hNr : (0 : ℝ) < N := by exact_mod_cast hN have hkr : (k : ℝ) + 1 ≤ N := by exact_mod_cast hk constructor · exact div_nonneg (add_nonneg (Nat.cast_nonneg _) hδ.1) (le_of_lt hNr) · apply (div_le_iff₀ hNr).2 linarith [hδ.2] calc (∫ u in Icc (0 : ℝ) 1, |((adjacentOrderMix N k δ) (Iic u)).toReal - (if (k + δ) / N ≤ u then (1 : ℝ) else 0)| ∂volume) = ∫ x, |x - ((k + δ) / N)| ∂μ := by exact integral_abs_cdf_sub_step_eq_mean_abs μ hsupp ht _ ≤ _ := adjacentOrderMix_abs_deviation_le_sqrt hN hk hδ

theorem sum_powerCell_sq_le {N : ℕ} (hN : 0 < N) {s : ℝ} (hs : 1 ≤ s) : ∑ j : Fin N, (powerCell N s j) ^ 2 ≤ s / N := by haveI : NeZero N := ⟨Nat.ne_of_gt hN⟩ have hmax : ∀ j : Fin N, powerCell N s j ≤ s / N := by intro j calc powerCell N s j ≤ powerCell N s ⟨0, hN⟩ := powerCell_antitone hs (Fin.zero_le j) _ ≤ s / N := powerCell_zero_le hN hs calc ∑ j : Fin N, (powerCell N s j) ^ 2 ≤ ∑ j : Fin N, (s / N) * powerCell N s j := by apply Finset.sum_le_sum intro j _ have h₁ := powerCell_nonneg hs j have h₂ := hmax j nlinarith [mul_nonneg h₁ (sub_nonneg.mpr h₂)] _ = s / N := by rw [← Finset.mul_sum, sum_powerCell hN hs, mul_one]

theorem integral_powerCurvature_mul_sqrt_le {s : ℝ} (hs : 1 < s) : (∫ t in Icc (0 : ℝ) 1, powerCurvature s t * sqrt t ∂volume) ≤ sqrt s := by have hr : IntervalIntegrable (fun x : ℝ => x ^ (s - 2)) volume 0 1 := intervalIntegral.intervalIntegrable_rpow' (by linarith) have hr' : IntervalIntegrable (fun t : ℝ => (1 - t) ^ (s - 2)) volume 0 1 := by convert (hr.comp_sub_left 1).symm using 1 <;> norm_num have hq : Integrable (powerCurvature s) (volume.restrict (Icc (0 : ℝ) 1)) := by apply (intervalIntegrable_iff_integrableOn_Icc_of_le (by norm_num : (0 : ℝ) ≤ 1)).mp change IntervalIntegrable (fun t : ℝ => s * (s - 1) * (1 - t) ^ (s - 2)) volume 0 1 exact hr'.const_mul (s * (s - 1)) have hpos : ∀ t ∈ Icc (0 : ℝ) 1, 0 ≤ powerCurvature s t := by intro t ht unfold powerCurvature exact mul_nonneg (mul_nonneg (by linarith) (by linarith)) (Real.rpow_nonneg (by linarith [ht.2]) _) have hsm : AEStronglyMeasurable (fun t : ℝ => sqrt t) (volume.restrict (Icc (0 : ℝ) 1)) := by fun_prop have hsqrt : Integrable (fun t : ℝ => powerCurvature s t * sqrt t) (volume.restrict (Icc (0 : ℝ) 1)) := by apply hq.mul_bdd (c := 1) hsm filter_upwards [ae_restrict_mem measurableSet_Icc] with t ht rw [Real.norm_eq_abs, abs_of_nonneg (Real.sqrt_nonneg t)] exact Real.sqrt_le_one.mpr ht.2 have htint : Integrable (fun t : ℝ => t * powerCurvature s t) (volume.restrict (Icc (0 : ℝ) 1)) := by apply hq.bdd_mul (by fun_prop) · filter_upwards [ae_restrict_mem measurableSet_Icc] with t ht rw [Real.norm_eq_abs, abs_of_nonneg ht.1] exact ht.2 have hroot : 0 < sqrt s := Real.sqrt_pos.2 (by linarith) have hbound : ∀ t ∈ Icc (0 : ℝ) 1, powerCurvature s t * sqrt t ≤ (sqrt s / 2) * (t * powerCurvature s t) + (1 / (2 * sqrt s)) * powerCurvature s t := by intro t ht have hsq := sq_nonneg (sqrt s * sqrt t - 1) have htsq : (sqrt t) ^ 2 = t := Real.sq_sqrt ht.1 have hssq : (sqrt s) ^ 2 = s := Real.sq_sqrt (by linarith) have hp := hpos t ht have hroot_ne : sqrt s ≠ 0 := ne_of_gt hroot have hscalar : sqrt t ≤ sqrt s / 2 * t + 1 / (2 * sqrt s) := by calc sqrt t ≤ (s * t + 1) / (2 * sqrt s) := by apply (le_div_iff₀ (by positivity : (0 : ℝ) < 2 * sqrt s)).mpr nlinarith [hsq] _ = sqrt s / 2 * t + 1 / (2 * sqrt s) := by field_simp nlinarith [hssq] calc powerCurvature s t * sqrt t = sqrt t * powerCurvature s t := by ring _ ≤ (sqrt s / 2 * t + 1 / (2 * sqrt s)) * powerCurvature s t := mul_le_mul_of_nonneg_right hscalar hp _ = _ := by ring calc (∫ t in Icc (0 : ℝ) 1, powerCurvature s t * sqrt t ∂volume) ≤ ∫ t in Icc (0 : ℝ) 1, (sqrt s / 2) * (t * powerCurvature s t) + (1 / (2 * sqrt s)) * powerCurvature s t ∂volume := by apply integral_mono_ae hsqrt ((htint.const_mul _).add (hq.const_mul _)) filter_upwards [ae_restrict_mem measurableSet_Icc] with t ht exact hbound t ht _ = sqrt s := by rw [integral_add (htint.const_mul _) (hq.const_mul _), integral_const_mul, integral_const_mul, integral_mul_powerCurvature_unit hs, integral_powerCurvature_unit hs] have hsq : (sqrt s) ^ 2 = s := Real.sq_sqrt (by linarith) field_simp nlinarith

theorem rankConcomitant_replacement_sensitivity {N : ℕ} (a : Fin N → ℝ) (ha : ∀ j, 0 ≤ a j) (hmono : Antitone a) (x : Fin N → ℝ × ℝ) (i : Fin N) (y : ℝ × ℝ) (hx : ∀ j, (x j).2 ∈ Icc (0 : ℝ) 1) (hy : y.2 ∈ Icc (0 : ℝ) 1) (hinj : Injective (fun j => (x j).1)) (hinj' : Injective (fun j => ((coordinateReplace i x y) j).1)) : |rankConcomitant a x - rankConcomitant a (coordinateReplace i x y)| ≤ a (rankPosition x i) + a (rankPosition (coordinateReplace i x y) i) := by classical let x' := coordinateReplace i x y have hback : coordinateReplace i x' (x i) = x := by funext j by_cases hji : j = i · subst j simp [x', coordinateReplace] · simp [x', coordinateReplace, hji] have hsum : (∑ j : Fin N, a (rankPosition x j)) = ∑ j : Fin N, a (rankPosition x' j) := by rw [sum_rankPosition_weights, sum_rankPosition_weights] have hnew : rankConcomitant a x' = (∑ j ∈ (Finset.univ : Finset (Fin N)).erase i, a (rankPosition x' j) * (x j).2) + a (rankPosition x' i) * y.2 := by rw [rankConcomitant_eq_sum_rankPosition, ← Finset.sum_erase_add Finset.univ _ (Finset.mem_univ i)] congr 1 · apply Finset.sum_congr rfl intro j hj have hji : j ≠ i := (Finset.mem_erase.mp hj).1 simp [x', coordinateReplace, hji] · simp [x', coordinateReplace] rcases le_total (x i).1 y.1 with hxy | hyx · have hcd : ∀ j, j ≠ i → a (rankPosition x j) ≤ a (rankPosition x' j) := by intro j hji exact hmono (rankPosition_replace_le x i j y hji hxy hinj hinj') have hb := weighted_replacement_bound (fun j => a (rankPosition x j)) (fun j => a (rankPosition x' j)) (fun j => (x j).2) i y.2 (fun j => ha _) (fun j => ha _) hx hy hcd hsum rw [rankConcomitant_eq_sum_rankPosition, hnew] exact hb · have hcd : ∀ j, j ≠ i → a (rankPosition x' j) ≤ a (rankPosition x j) := by intro j hji apply hmono simpa only [hback] using (rankPosition_replace_le x' i j (x i) hji (by simpa [x', coordinateReplace] using hyx) hinj' (by simpa [hback] using hinj)) have hmark : ∀ j, (x' j).2 ∈ Icc (0 : ℝ) 1 := by intro j by_cases hji : j = i · subst j simpa [x', coordinateReplace] using hy · simpa [x', coordinateReplace, hji] using hx j have hold : rankConcomitant a x = (∑ j ∈ (Finset.univ : Finset (Fin N)).erase i, a (rankPosition x j) * (x' j).2) + a (rankPosition x i) * (x i).2 := by rw [rankConcomitant_eq_sum_rankPosition, ← Finset.sum_erase_add Finset.univ _ (Finset.mem_univ i)] congr 1 apply Finset.sum_congr rfl intro j hj have hji : j ≠ i := (Finset.mem_erase.mp hj).1 simp [x', coordinateReplace, hji] have hb := weighted_replacement_bound (fun j => a (rankPosition x' j)) (fun j => a (rankPosition x j)) (fun j => (x' j).2) i (x i).2 (fun j => ha _) (fun j => ha _) hmark (hx i) hcd hsum.symm change |rankConcomitant a x - rankConcomitant a x'| ≤ a (rankPosition x i) + a (rankPosition x' i) calc |rankConcomitant a x - rankConcomitant a x'| = |rankConcomitant a x' - rankConcomitant a x| := abs_sub_comm _ _ _ = |(∑ j : Fin N, a (rankPosition x' j) * (x' j).2) - ((∑ j ∈ (Finset.univ : Finset (Fin N)).erase i, a (rankPosition x j) * (x' j).2) + a (rankPosition x i) * (x i).2)| := by rw [rankConcomitant_eq_sum_rankPosition, hold] _ ≤ _ := by simpa only [add_comm] using hb

theorem ae_eq_of_comp_continuous_cdf (ν : Measure ℝ) [IsProbabilityMeasure ν] (hcont : Continuous (fun t => cdf ν t)) (f g : ℝ → ℝ) (h : (fun t => f (cdf ν t)) =ᵐ[ν] (fun t => g (cdf ν t))) : f =ᵐ[uniform01] g := by let ρ : Measure ℝ := unifOI change (∀ᵐ t ∂ν, f (cdf ν t) = g (cdf ν t)) at h have hq : (fun u => f (cdf ν (quantile ν u))) =ᵐ[ρ] (fun u => g (cdf ν (quantile ν u))) := by have h' := ae_of_ae_map (aemeasurable_quantile_unifOI ν) (p := fun t => f (cdf ν t) = g (cdf ν t)) (by simpa only [quantile_map_uniform] using h) change (∀ᵐ u ∂ρ, f (cdf ν (quantile ν u)) = g (cdf ν (quantile ν u))) exact h' have hc : (fun u => cdf ν (quantile ν u)) =ᵐ[ρ] id := by filter_upwards [ae_restrict_mem measurableSet_Ioo] with u hu exact Causalean.Stat.cdf_quantile_eq ν hu.1 hu.2 hcont.continuousAt have hfg : f =ᵐ[ρ] g := by filter_upwards [hq, hc] with u heq hid simpa only [id_eq, hid] using heq change f =ᵐ[volume.restrict (Icc (0 : ℝ) 1)] g rw [← restrict_Ioo_eq_restrict_Icc] exact hfg

theorem integral_rankConcomitant_eq_bernstein {N : ℕ} (hN : 0 < N) (μ : Measure (ℝ × ℝ)) [IsProbabilityMeasure μ] (hcont : Continuous (fun t => cdf (μ.map fst) t)) (hmark : ∀ᵐ p ∂μ, p.2 ∈ Icc (0 : ℝ) 1) (a : Fin N → ℝ) (m : ℝ → ℝ) (hm : (fun p : ℝ × ℝ => m (cdf (μ.map fst) p.1)) =ᵐ[μ] μ[(fun p : ℝ × ℝ => p.2) | comap (fun p : ℝ × ℝ => cdf (μ.map fst) p.1) inferInstance]) : (∫ x, rankConcomitant a x ∂Measure.pi (fun _ : Fin N => μ)) = ∫ u in Icc (0 : ℝ) 1, m u * bernsteinCell N a u ∂volume := by classical let ν : Measure (Fin N → ℝ × ℝ) := Measure.pi (fun _ => μ) haveI : IsProbabilityMeasure uniform01 := ⟨by simp [uniform01]⟩ let ρ : Measure (Fin N → ℝ) := iidSample uniform01 N haveI : IsProbabilityMeasure ρ := by dsimp [ρ, iidSample] infer_instance let F : ℝ × ℝ → ℝ := fun p => cdf (μ.map fst) p.1 let T : (Fin N → ℝ × ℝ) → (Fin N → ℝ) := fun x i => F (x i) have hT : Measurable T := measurable_pi_iff.mpr fun i => hcont.measurable.comp (measurable_fst.comp (measurable_pi_apply i)) have hmap : ν.map T = ρ := cdf_transport_iid μ hcont have hm_meas : AEMeasurable m uniform01 := aemeasurable_conditionalMean_uniform μ hcont m hm have hm_bound : ∀ᵐ u ∂uniform01, |m u| ≤ 1 := (conditionalMean_mem_Icc_ae μ hcont hmark m hm).mono fun u hu => abs_le.mpr ⟨by linarith [hu.1], hu.2⟩ let g := hm_meas.mk m have hg : Measurable g := hm_meas.measurable_mk have hmg : m =ᵐ[uniform01] g := hm_meas.ae_eq_mk let B (j : Fin N) (u : ℝ) : ℝ := (choose (N - 1) j.val : ℝ) * u ^ j.val * (1 - u) ^ (N - 1 - j.val) let Q (i j : Fin N) (u : Fin N → ℝ) : ℝ := if (sort u).symm i = j then m (u i) else 0 have htag_meas (i j : Fin N) : AEStronglyMeasurable (Q i j) ρ := by let C : Set (Fin N → ℝ) := {u | (((Finset.univ : Finset (Fin N)).erase i).filter (fun k => u k < u i)).card = j.val} have hC : MeasurableSet C := by apply measurableSet_eq_fun · simp_rw [Finset.card_filter] apply Finset.measurable_sum intro k _ apply Measurable.ite · exact measurableSet_lt (measurable_pi_apply k) (measurable_pi_apply i) · exact measurable_const · exact measurable_const · exact measurable_const have hcoord : ∀ᵐ u ∂ρ, m (u i) = g (u i) := by apply ae_of_ae_map (μ := ρ) (f := fun u : Fin N → ℝ => u i) (p := fun v => m v = g v) (measurable_pi_apply i).aemeasurable have heval : ρ.map (fun u : Fin N → ℝ => u i) = uniform01 := (measurePreserving_eval (fun _ : Fin N => uniform01) i).map_eq rw [heval] exact hmg have haux : AEStronglyMeasurable (fun u : Fin N → ℝ => if u ∈ C then m (u i) else 0) ρ := by have haux' : AEStronglyMeasurable (fun u : Fin N → ℝ => if u ∈ C then g (u i) else 0) ρ := ((hg.comp (measurable_pi_apply i)).ite hC measurable_const).aestronglyMeasurable apply haux'.congr filter_upwards [hcoord] with u hu by_cases hc : u ∈ C <;> simp [hc, hu] apply haux.congr filter_upwards [iid_uniform_coordinates_injective_ae (N := N)] with u hu have hiff : (sort u).symm i = j ↔ u ∈ C := by change (sort u).symm i = j ↔ (((Finset.univ : Finset (Fin N)).erase i).filter (fun k => u k < u i)).card = j.val rw [← uniform_tagged_rank_eq_count u i hu] exact Fin.ext_iff simp [Q, hiff] have htag_int (i j : Fin N) : Integrable (Q i j) ρ := by apply Integrable.of_bound (htag_meas i j) 1 have hcoord : ∀ᵐ u ∂ρ, |m (u i)| ≤ 1 := by apply ae_of_ae_map (μ := ρ) (f := fun u : Fin N → ℝ => u i) (p := fun v => |m v| ≤ 1) (measurable_pi_apply i).aemeasurable have heval : ρ.map (fun u : Fin N → ℝ => u i) = uniform01 := (measurePreserving_eval (fun _ : Fin N => uniform01) i).map_eq rw [heval] exact hm_bound filter_upwards [hcoord] with u hu by_cases h : (sort u).symm i = j · simpa [Q, h, Real.norm_eq_abs] using hu · simp [Q, h] have hterm (i j : Fin N) : (∫ x, (if (sort (fun k => (x k).1)).symm i = j then m (F (x i)) else 0) ∂ν) = ∫ u in Icc (0 : ℝ) 1, m u * B j u ∂volume := by calc _ = ∫ x, Q i j (T x) ∂ν := by apply integral_congr_ae filter_upwards [sort_cdf_eq_ae μ hcont] with x hx simp only [Q, T, F, ← hx] _ = ∫ u, Q i j u ∂ρ := by have hh : (∫ u, Q i j u ∂ν.map T) = ∫ x, Q i j (T x) ∂ν := integral_map hT.aemeasurable (by rw [hmap]; exact htag_meas i j) rw [hmap] at hh exact hh.symm _ = _ := uniform_tagged_rank_cell_integral hN i j m hm_meas hm_bound have hpoint (x : Fin N → ℝ × ℝ) (z : Fin N → ℝ) : (∑ j : Fin N, a j * z ((sort (fun k => (x k).1)) j)) = ∑ i : Fin N, ∑ j : Fin N, if (sort (fun k => (x k).1)).symm i = j then a j * z i else 0 := by let σ := sort (fun k => (x k).1) have h := Equiv.sum_comp σ (fun i : Fin N => ∑ j : Fin N, if σ.symm i = j then a j * z i else 0) simpa only [σ, Equiv.symm_apply_apply, Finset.sum_ite_eq, Finset.mem_univ, if_true] using h have hmean_int (i j : Fin N) : Integrable (fun x : Fin N → ℝ × ℝ => if (sort (fun k => (x k).1)).symm i = j then a j * m (F (x i)) else 0) ν := by have hcomp : Integrable (fun x => a j * Q i j (T x)) ν := by have hi := (htag_int i j).const_mul (a j) have hi' : Integrable (fun u => a j * Q i j u) (ν.map T) := by rw [hmap] exact hi simpa only [Function.comp_def] using hi'.comp_aemeasurable hT.aemeasurable apply hcomp.congr filter_upwards [sort_cdf_eq_ae μ hcont] with x hx simp only [Q, T, F, ← hx] split_ifs <;> simp have hm_int : Integrable m uniform01 := by apply Integrable.of_bound hm_meas.aestronglyMeasurable 1 simpa only [Real.norm_eq_abs] using hm_bound have hrhs_int (j : Fin N) : IntegrableOn (fun u => m u * (a j * B j u)) (Icc (0 : ℝ) 1) volume := by have hB : Continuous (B j) := by dsimp [B] fun_prop have hmI : IntegrableOn m (Icc (0 : ℝ) 1) volume := by change Integrable m (volume.restrict (Icc (0 : ℝ) 1)) simpa only [uniform01] using hm_int exact hmI.mul_continuousOn (continuous_const.mul hB).continuousOn isCompact_Icc calc (∫ x, rankConcomitant a x ∂ν) = ∫ x, ∑ j : Fin N, a j * m (F (x (sort (fun i => (x i).1) j))) ∂ν := integral_rankConcomitant_eq_conditionalMean μ hcont hmark a m hm _ = ∫ x, ∑ i : Fin N, ∑ j : Fin N, (if (sort (fun k => (x k).1)).symm i = j then a j * m (F (x i)) else 0) ∂ν := by apply integral_congr_ae exact Filter.Eventually.of_forall fun x => by simpa only using hpoint x (fun i => m (F (x i))) _ = ∑ i : Fin N, ∑ j : Fin N, ∫ x, (if (sort (fun k => (x k).1)).symm i = j then a j * m (F (x i)) else 0) ∂ν := by rw [integral_finsetSum (s := Finset.univ) (fun i _ => integrable_finsetSum _ (fun j _ => hmean_int i j))] congr 1 funext i rw [integral_finsetSum (s := Finset.univ) (fun j _ => hmean_int i j)] _ = ∑ i : Fin N, ∑ j : Fin N, a j * ∫ u in Icc (0 : ℝ) 1, m u * B j u ∂volume := by apply Finset.sum_congr rfl intro i _ apply Finset.sum_congr rfl intro j _ calc _ = a j * ∫ x, (if (sort (fun k => (x k).1)).symm i = j then m (F (x i)) else 0) ∂ν := by rw [← integral_const_mul] congr 1 funext x split_ifs <;> simp [*] _ = _ := congrArg (a j * ·) (hterm i j) _ = ∫ u in Icc (0 : ℝ) 1, m u * bernsteinCell N a u ∂volume := by calc _ = (N : ℝ) * ∑ j : Fin N, a j * ∫ u in Icc (0 : ℝ) 1, m u * B j u ∂volume := by simp only [Finset.sum_const, Finset.card_fin, nsmul_eq_mul] _ = (N : ℝ) * ∫ u in Icc (0 : ℝ) 1, ∑ j : Fin N, m u * (a j * B j u) ∂volume := by rw [integral_finsetSum (s := Finset.univ) (fun j _ => hrhs_int j)] congr 1 apply Finset.sum_congr rfl intro j _ rw [← integral_const_mul] apply integral_congr_ae exact Filter.Eventually.of_forall fun u => by ring _ = _ := by rw [← integral_const_mul] apply integral_congr_ae exact Filter.Eventually.of_forall fun u => by simp only [bernsteinCell, B, Finset.mul_sum] apply Finset.sum_congr rfl intro j _ ring

theorem integral_tagged_rank_mark_eq_conditionalMean {N : ℕ} (μ : Measure (ℝ × ℝ)) [IsProbabilityMeasure μ] (hcont : Continuous (fun t => cdf (μ.map fst) t)) (hmark : ∀ᵐ p ∂μ, p.2 ∈ Icc (0 : ℝ) 1) (i j : Fin N) (m : ℝ → ℝ) (hm : (fun p : ℝ × ℝ => m (cdf (μ.map fst) p.1)) =ᵐ[μ] μ[(fun p : ℝ × ℝ => p.2) | comap (fun p : ℝ × ℝ => cdf (μ.map fst) p.1) inferInstance]) : (∫ x, (if (sort (fun k => (x k).1)).symm i = j then (x i).2 else 0) ∂Measure.pi (fun _ : Fin N => μ)) = ∫ x, (if (sort (fun k => (x k).1)).symm i = j then m (cdf (μ.map fst) (x i).1) else 0) ∂Measure.pi (fun _ : Fin N => μ) := by -- Conditional expectation is taken in the tagged factor. The rank event is -- measurable in the sigma algebra generated by the transported coordinates; -- use `sort_cdf_eq_ae` before conditioning to remove dependence on raw marks. classical obtain ⟨g, hg, hmg⟩ := conditionalMean_exists_measurable_version μ m hm let F : ℝ × ℝ → ℝ := fun p => cdf (μ.map fst) p.1 have hF : Measurable F := hcont.measurable.comp measurable_fst have hgm : (fun p => g (F p)) =ᵐ[μ] μ[(fun p : ℝ × ℝ => p.2) | comap F inferInstance] := hmg.symm.trans hm have hgbound : ∀ᵐ p ∂μ, |g (F p)| ≤ 1 := by filter_upwards [conditionalMean_comp_mem_Icc_ae μ hmark m hm, hmg] with p hp he rw [he] at hp exact abs_le.mpr ⟨by linarith [hp.1], hp.2⟩ have hreplace : (∫ x, (if (sort (fun k => (x k).1)).symm i = j then m (F (x i)) else 0) ∂Measure.pi (fun _ : Fin N => μ)) = ∫ x, (if (sort (fun k => (x k).1)).symm i = j then g (F (x i)) else 0) ∂Measure.pi (fun _ : Fin N => μ) := by apply integral_congr_ae have he : ∀ᵐ x ∂Measure.pi (fun _ : Fin N => μ), m (F (x i)) = g (F (x i)) := by exact ae_of_ae_map (μ := Measure.pi (fun _ : Fin N => μ)) (f := fun x : Fin N → ℝ × ℝ => x i) (p := fun p => m (F p) = g (F p)) (measurable_pi_apply i).aemeasurable (by rw [(measurePreserving_eval (fun _ : Fin N => μ) i).map_eq] exact hmg) filter_upwards [he] with x hx split_ifs <;> simp [hx] rw [hreplace] cases N with | zero => exact i.elim0 | succ n => let ν : Measure (Fin (n + 1) → ℝ × ℝ) := Measure.pi (fun _ => μ) let ρ : Measure (Fin n → ℝ × ℝ) := Measure.pi (fun _ => μ) let e := piFinSuccAbove (fun _ : Fin (n + 1) => ℝ × ℝ) i let C : Set (Fin (n + 1) → ℝ × ℝ) := {x | (((Finset.univ : Finset (Fin (n + 1))).erase i).filter (fun k => F (x k) < F (x i))).card = j.val} have hC : MeasurableSet C := by dsimp [C] apply measurableSet_eq_fun · simp_rw [Finset.card_filter] apply Finset.measurable_sum intro k _ apply Measurable.ite · exact measurableSet_lt (hF.comp (measurable_pi_apply k)) (hF.comp (measurable_pi_apply i)) · exact measurable_const · exact measurable_const · exact measurable_const have hrank : ∀ᵐ x ∂ν, ((sort (fun k => (x k).1)).symm i = j) ↔ x ∈ C := by have htransport := cdf_transport_iid (N := n + 1) μ hcont have hinj : ∀ᵐ x ∂ν, Injective (fun k => F (x k)) := by have hu := iid_uniform_coordinates_injective_ae (N := n + 1) rw [← htransport] at hu exact ae_of_ae_map (by apply aemeasurable apply measurable_pi_iff.mpr intro k exact hF.comp (measurable_pi_apply k) : AEMeasurable (fun x : Fin (n + 1) → ℝ × ℝ => fun k => F (x k)) ν) hu filter_upwards [sort_cdf_eq_ae μ hcont, hinj] with x hs hx have hc : ((sort (fun k => F (x k))).symm i = j) ↔ x ∈ C := by change ((sort (fun k => F (x k))).symm i = j) ↔ (((Finset.univ : Finset (Fin (n + 1))).erase i).filter (fun k => F (x k) < F (x i))).card = j.val rw [← uniform_tagged_rank_eq_count (fun k => F (x k)) i hx] exact Fin.ext_iff rw [hs] exact hc let L : (Fin (n + 1) → ℝ × ℝ) → ℝ := fun x => if x ∈ C then (x i).2 else 0 let R : (Fin (n + 1) → ℝ × ℝ) → ℝ := fun x => if x ∈ C then g (F (x i)) else 0 have hLint : Integrable L ν := by have hmeas : Measurable L := (measurable_snd.comp (measurable_pi_apply i)).ite hC measurable_const have hb : ∀ᵐ x ∂ν, |(x i).2| ≤ 1 := by have hbμ : ∀ᵐ p ∂μ, |p.2| ≤ 1 := hmark.mono fun p hp => abs_le.mpr ⟨by linarith [hp.1], hp.2⟩ exact ae_of_ae_map (μ := ν) (f := fun x : Fin (n + 1) → ℝ × ℝ => x i) (p := fun p => |p.2| ≤ 1) (measurable_pi_apply i).aemeasurable (by rw [(measurePreserving_eval (fun _ : Fin (n + 1) => μ) i).map_eq] exact hbμ) apply Integrable.of_bound hmeas.aestronglyMeasurable 1 filter_upwards [hb] with x hx by_cases hc : x ∈ C · simpa [L, hc, Real.norm_eq_abs] using hx · simp [L, hc] have hRint : Integrable R ν := by have hmeas : Measurable R := (hg.comp (hF.comp (measurable_pi_apply i))).ite hC measurable_const have hb : ∀ᵐ x ∂ν, |g (F (x i))| ≤ 1 := by exact ae_of_ae_map (μ := ν) (f := fun x : Fin (n + 1) → ℝ × ℝ => x i) (p := fun p => |g (F p)| ≤ 1) (measurable_pi_apply i).aemeasurable (by rw [(measurePreserving_eval (fun _ : Fin (n + 1) => μ) i).map_eq] exact hgbound) apply Integrable.of_bound hmeas.aestronglyMeasurable 1 filter_upwards [hb] with x hx by_cases hc : x ∈ C · simpa [R, hc, Real.norm_eq_abs] using hx · simp [R, hc] have hsplit (T : (Fin (n + 1) → ℝ × ℝ) → ℝ) (hT : Integrable T ν) : (∫ x, T x ∂ν) = ∫ w, ∫ p, T (e.symm (p, w)) ∂μ ∂ρ := by have he := measurePreserving_piFinSuccAbove (fun _ : Fin (n + 1) => μ) i have hcomp : (fun z => T (e.symm z)) ∘ e = T := by funext x simp calc _ = ∫ z : (ℝ × ℝ) × (Fin n → ℝ × ℝ), T (e.symm z) ∂μ.prod ρ := by have hh := he.integral_comp' (fun z => T (e.symm z)) change (∫ x, ((fun z => T (e.symm z)) ∘ e) x ∂ν) = _ at hh rw [hcomp] at hh exact hh _ = _ := by apply integral_prod_symm apply (he.integrable_comp_emb e.measurableEmbedding).mp change Integrable (((fun z => T (e.symm z)) ∘ e)) ν rw [hcomp] exact hT have hcount (p : ℝ × ℝ) (w : Fin n → ℝ × ℝ) : (((Finset.univ : Finset (Fin (n + 1))).erase i).filter (fun k => F ((e.symm (p, w)) k) < F p)).card = ((Finset.univ : Finset (Fin n)).filter (fun k => F (w k) < F p)).card := by have hindex : ((Finset.univ : Finset (Fin (n + 1))).erase i) = (Finset.univ : Finset (Fin n)).image i.succAbove := by ext k simp only [Finset.mem_erase, Finset.mem_univ, and_true, mem_image, Finset.mem_univ, true_and] rw [← Set.mem_range] simp [Fin.range_succAbove] rw [hindex, Finset.filter_image, Finset.card_image_of_injective] · simp [e] · exact Fin.succAbove_right_injective have hinner (w : Fin n → ℝ × ℝ) : (∫ p, L (e.symm (p, w)) ∂μ) = ∫ p, R (e.symm (p, w)) ∂μ := by let S : Set (ℝ × ℝ) := {p | ((Finset.univ : Finset (Fin n)).filter (fun k => F (w k) < F p)).card = j.val} have hS : MeasurableSet[comap F inferInstance] S := by dsimp [S] apply measurableSet_eq_fun · simp_rw [Finset.card_filter] apply Finset.measurable_sum intro k _ apply Measurable.ite · exact measurableSet_lt measurable_const (comap_measurable F) · exact measurable_const · exact measurable_const · exact measurable_const have hS' : MeasurableSet S := hF.comap_le S hS have hL : (fun p => L (e.symm (p, w))) = S.indicator (fun p => p.2) := by funext p have hi : (e.symm (p,w)) i = p := by simp [e] have hc : e.symm (p,w) ∈ C ↔ p ∈ S := by change (((Finset.univ : Finset (Fin (n + 1))).erase i).filter (fun k => F ((e.symm (p,w)) k) < F ((e.symm (p,w)) i))).card = j.val ↔ ((Finset.univ : Finset (Fin n)).filter (fun k => F (w k) < F p)).card = j.val rw [hi, hcount] simp only [L, indicator, hi, hc] have hR : (fun p => R (e.symm (p, w))) = S.indicator (fun p => g (F p)) := by funext p have hi : (e.symm (p,w)) i = p := by simp [e] have hc : e.symm (p,w) ∈ C ↔ p ∈ S := by change (((Finset.univ : Finset (Fin (n + 1))).erase i).filter (fun k => F ((e.symm (p,w)) k) < F ((e.symm (p,w)) i))).card = j.val ↔ ((Finset.univ : Finset (Fin n)).filter (fun k => F (w k) < F p)).card = j.val rw [hi, hcount] simp only [R, indicator, hi, hc] rw [hL, hR] rw [integral_indicator hS', integral_indicator hS'] calc (∫ p in S, p.2 ∂μ) = ∫ p in S, (μ[(fun p : ℝ × ℝ => p.2) | comap F inferInstance]) p ∂μ := (setIntegral_condExp hF.comap_le (Integrable.of_bound measurable_snd.aestronglyMeasurable 1 (hmark.mono fun p hp => by simpa only [Real.norm_eq_abs] using (abs_le.mpr ⟨by linarith [hp.1], hp.2⟩))) hS).symm _ = ∫ p in S, g (F p) ∂μ := by apply setIntegral_congr_ae hS' exact hgm.symm.mono (fun p hp _ => hp) calc (∫ x, (if (sort (fun k => (x k).1)).symm i = j then (x i).2 else 0) ∂ν) = ∫ x, L x ∂ν := by apply integral_congr_ae filter_upwards [hrank] with x hx simp only [L, if_congr hx rfl rfl] _ = ∫ w, ∫ p, L (e.symm (p, w)) ∂μ ∂ρ := hsplit L hLint _ = ∫ w, ∫ p, R (e.symm (p, w)) ∂μ ∂ρ := by exact integral_congr_ae (Filter.Eventually.of_forall hinner) _ = ∫ x, R x ∂ν := (hsplit R hRint).symm _ = ∫ x, (if (sort (fun k => (x k).1)).symm i = j then g (F (x i)) else 0) ∂ν := by apply integral_congr_ae filter_upwards [hrank] with x hx simp only [R, if_congr hx rfl rfl]

theorem simplex_coordinate_cross_moment (n : ℕ) (i j : Fin n) (hij : i ≠ j) : (n.factorial : ℝ) * (∫ z in spacingSimplex n, z i * z j ∂volume) = (1 : ℝ) / ((n + 1) * (n + 2)) := by cases n with | zero => exact elim0 i | succ n => cases n with | zero => exact False.elim (hij (Fin.ext (by have hi := i.isLt have hj := j.isLt omega))) | succ m => have hcross := simplex_cross_coordinate_eq_first_two m i j hij have hfubini := simplex_first_second_cross_fubini m have hinner (t : ℝ) (ht : t ∈ Icc (0 : ℝ) 1) : (∫ w in scaledSpacingSimplex (m + 1) (1 - t), w (0 : Fin (m + 1)) ∂volume) = (1 - t) ^ (m + 2) / ((m + 2) * ((m + 1).factorial : ℝ)) := by have h := scaled_simplex_coordinate_first_moment (m + 1) (1 - t) (sub_nonneg.mpr ht.2) (0 : Fin (m + 1)) have hfac : ((m + 1).factorial : ℝ) ≠ 0 := by positivity have hdim : ((m + 2 : ℕ) : ℝ) ≠ 0 := by positivity push_cast at h ⊢ field_simp at h ⊢ nlinarith [h] have hint : (∫ z in spacingSimplex (m + 2), z (0 : Fin (m + 2)) * z (1 : Fin (m + 2)) ∂volume) = (m + 2).factorial / (m + 4).factorial / ((m + 2) * ((m + 1).factorial : ℝ)) := by rw [hfubini] have heq : (∫ t in Icc (0 : ℝ) 1, t * (∫ w in scaledSpacingSimplex (m + 1) (1 - t), w (0 : Fin (m + 1)) ∂volume) ∂volume) = ∫ t in Icc (0 : ℝ) 1, t * ((1 - t) ^ (m + 2) / ((m + 2) * ((m + 1).factorial : ℝ))) ∂volume := by apply setIntegral_congr_fun measurableSet_Icc intro t ht change t * _ = t * _ rw [hinner t ht] rw [heq] simp_rw [← mul_div_assoc] rw [integral_div] rw [unit_beta_linear_integral (m + 2)] rw [hcross, hint] have hfac : ((m + 1).factorial : ℝ) ≠ 0 := by positivity simp only [Nat.factorial_succ] push_cast field_simp ring

theorem bernsteinCell_power_eq_sub_curvature_hinge_integral {N : ℕ} (hN : 0 < N) {s : ℝ} (hs : 1 < s) (u : ℝ) : bernsteinCell N (powerCell N s) u = s - ∫ t in Icc (0 : ℝ) 1, powerCurvature s t * bernsteinCell N (hingeCell N t) u ∂volume := by -- Integrate the preceding hinge representation over each cell, then use -- finite-sum linearity and the binomial partition of unity. This is valid -- for every real u because the Bernstein basis sum is identically one. let b (j : Fin N) : ℝ := (choose (N - 1) (j : ℕ) : ℝ) * u ^ (j : ℕ) * (1 - u) ^ (N - 1 - (j : ℕ)) have hNr : (N : ℝ) ≠ 0 := by exact_mod_cast (Nat.ne_of_gt hN) have hsum : (∑ j : Fin N, b j) = 1 := by have hpow := add_pow u (1 - u) (N - 1) rw [show N - 1 + 1 = N by omega, ← Fin.sum_univ_eq_sum_range] at hpow convert hpow.symm using 1 · apply Finset.sum_congr rfl intro j hj dsimp [b] ring · ring have hr : IntervalIntegrable (fun x : ℝ => x ^ (s - 2)) volume 0 1 := intervalIntegral.intervalIntegrable_rpow' (by linarith) have hr' : IntervalIntegrable (fun t : ℝ => (1 - t) ^ (s - 2)) volume 0 1 := by convert (hr.comp_sub_left 1).symm using 1 <;> norm_num have hq : Integrable (powerCurvature s) (volume.restrict (Icc (0 : ℝ) 1)) := by apply (intervalIntegrable_iff_integrableOn_Icc_of_le (by norm_num : (0 : ℝ) ≤ 1)).mp change IntervalIntegrable (fun t : ℝ => s * (s - 1) * (1 - t) ^ (s - 2)) volume 0 1 exact hr'.const_mul (s * (s - 1)) have hbound (j : Fin N) (t : ℝ) : ‖hingeCell N t j‖ ≤ (1 : ℝ) / N := by have hNr' : (0 : ℝ) < N := by exact_mod_cast hN have hw : (((j : ℕ) : ℝ) + 1) / N - ((j : ℕ) : ℝ) / N = (1 : ℝ) / N := by ring rw [hingeCell_eq_piecewise hN] split_ifs with ha hb · rw [Real.norm_eq_abs, abs_of_nonneg (by positivity)] · have hlt : ((j : ℕ) : ℝ) / N < t := lt_of_not_ge ha have hnonneg : 0 ≤ (((j : ℕ) : ℝ) + 1) / N - t := by linarith rw [Real.norm_eq_abs, abs_of_nonneg hnonneg] linarith · simp [hNr'.le] have hint (j : Fin N) : Integrable (fun t : ℝ => powerCurvature s t * hingeCell N t j) (volume.restrict (Icc (0 : ℝ) 1)) := by apply hq.mul_bdd (c := (1 : ℝ) / N) · have hc : Continuous (hingeCell N · j) := by unfold hingeCell fun_prop exact hc.aestronglyMeasurable · filter_upwards [] with t exact hbound j t have hint' (j : Fin N) : Integrable (fun t : ℝ => powerCurvature s t * hingeCell N t j * b j) (volume.restrict (Icc (0 : ℝ) 1)) := (hint j).mul_const _ have hswap : (∑ j : Fin N, (∫ t in Icc (0 : ℝ) 1, powerCurvature s t * hingeCell N t j ∂volume) * b j) = ∫ t in Icc (0 : ℝ) 1, ∑ j : Fin N, powerCurvature s t * hingeCell N t j * b j ∂volume := by rw [integral_finsetSum (s := univ) (fun j hj => hint' j)] apply Finset.sum_congr rfl intro j hj rw [integral_mul_const] calc bernsteinCell N (powerCell N s) u = N * ∑ j : Fin N, powerCell N s j * b j := by unfold bernsteinCell congr 1 apply Finset.sum_congr rfl intro j hj dsimp [b] ring _ = N * ∑ j : Fin N, (s / N - ∫ t in Icc (0 : ℝ) 1, powerCurvature s t * hingeCell N t j ∂volume) * b j := by congr 1 apply Finset.sum_congr rfl intro j hj rw [powerCell_eq_sub_curvature_hinge_integral hN hs j] _ = N * (s / N * (∑ j : Fin N, b j) - ∑ j : Fin N, (∫ t in Icc (0 : ℝ) 1, powerCurvature s t * hingeCell N t j ∂volume) * b j) := by congr 1 rw [Finset.mul_sum, ← Finset.sum_sub_distrib] apply Finset.sum_congr rfl intro j hj ring _ = s - ∫ t in Icc (0 : ℝ) 1, powerCurvature s t * bernsteinCell N (hingeCell N t) u ∂volume := by rw [hsum, mul_one, hswap, mul_sub, mul_div_cancel₀ s hNr] rw [← integral_const_mul] congr 1 apply integral_congr_ae filter_upwards [] with t simp only [bernsteinCell, Finset.mul_sum] apply Finset.sum_congr rfl intro j hj dsimp [b] ring

theorem power_bernstein_L1 {N : ℕ} (hN : 0 < N) {s : ℝ} (hs : 1 ≤ s) : (∫ u in Icc (0 : ℝ) 1, |bernsteinCell N (powerCell N s) u - powerDensity s u| ∂volume) ≤ 2 * sqrt (s / N) := by by_cases hlarge : (N : ℝ) < s · exact power_bernstein_L1_large hN hlarge · exact power_bernstein_L1_small hN hs (le_of_not_gt hlarge)

theorem integral_coordinateVariance_eq_half_replacement_sq {N : ℕ} {α : Type*} [MeasurableSpace α] (μ : Measure α) [IsProbabilityMeasure μ] (i : Fin N) (F : (Fin N → α) → ℝ) (hF : MemLp F 2 (Measure.pi (fun _ : Fin N => μ))) : (∫ x, variance (fun y => F (coordinateReplace i x y)) μ ∂Measure.pi (fun _ : Fin N => μ)) = (1 / 2 : ℝ) * ∫ x, ∫ y, (F x - F (coordinateReplace i x y)) ^ 2 ∂μ ∂Measure.pi (fun _ : Fin N => μ) := by rw [integral_coordinateVariance_eq_half_double_replacement_sq μ i F hF, integral_double_replacement_sq_eq_replacement_sq μ i F hF]

theorem variance_rankConcomitant_le_twice_sum_sq {N : ℕ} (μ : Measure (ℝ × ℝ)) [IsProbabilityMeasure μ] (hcont : Continuous (fun t => cdf (μ.map fst) t)) (hmark : ∀ᵐ p ∂μ, p.2 ∈ Icc (0 : ℝ) 1) (a : Fin N → ℝ) (ha : ∀ j, 0 ≤ a j) (hmono : Antitone a) : variance (rankConcomitant a) (Measure.pi (fun _ : Fin N => μ)) ≤ 2 * ∑ j : Fin N, (a j) ^ 2 := by classical have hT := variance_pi_le_sum_integral_coordinateVariance (fun _ : Fin N => μ) (rankConcomitant a) (rankConcomitant_memLp_two μ hmark a) by_cases hN : 0 < N · calc variance (rankConcomitant a) (Measure.pi (fun _ : Fin N => μ)) ≤ ∑ i : Fin N, ∫ x, variance (fun y => rankConcomitant a (coordinateReplace i x y)) μ ∂Measure.pi (fun _ : Fin N => μ) := hT _ ≤ ∑ i : Fin N, 2 * ∫ x, (a (rankPosition x i)) ^ 2 ∂Measure.pi (fun _ : Fin N => μ) := by apply Finset.sum_le_sum intro i _ exact integral_coordinateVariance_rankConcomitant_le μ hcont hmark a ha hmono i _ = 2 * ∑ j : Fin N, (a j) ^ 2 := by simp_rw [integral_rankPosition_weight_sq hN μ hcont a] simp only [Finset.sum_const, Finset.card_fin, nsmul_eq_mul] have hN' : (N : ℝ) ≠ 0 := by exact_mod_cast (Nat.ne_of_gt hN) field_simp · have h0 : N = 0 := Nat.eq_zero_of_not_pos hN subst N simpa using hT

theorem uniform_sorted_cdf_eq_binomial_tail {n : ℕ} (r : Fin n) {u : ℝ} (hu : u ∈ Icc (0 : ℝ) 1) : ((iidSample uniform01 n).map (fun x => sortedSample n x r)) (Iic u) = ofReal (∑ k ∈ Icc (r.val + 1) n, (Nat.choose n k : ℝ) * u ^ k * (1 - u) ^ (n - k)) := by -- Use `sortedSample_le_iff_count_le`, partition by the finite count, -- and sum `uniform_count_le_mass` over the upper tail. Mathlib's -- `MeasureTheory.sum_measure_preimage_singleton` gives the finite -- partition directly for the count function and `Icc (r.val+1) n`. -- Its measurability follows by a finite sum of indicators of the -- measurable coordinate events `{x | x i ≤ u}`. let count : (Fin n → ℝ) → ℕ := fun x => ((Finset.univ : Finset (Fin n)).filter (fun i => x i ≤ u)).card have hcount : Measurable count := by have hsum : Measurable (fun x : Fin n → ℝ => ∑ i : Fin n, if x i ≤ u then (1 : ℕ) else 0) := by apply Finset.measurable_sum intro i hi exact Measurable.ite ((measurable_pi_apply i) measurableSet_Iic) measurable_const measurable_const simpa only [count, Finset.card_filter] using hsum have hsorted : Measurable (fun x : Fin n → ℝ => sortedSample n x r) := by apply measurable_of_Iic intro t have ht : (fun x : Fin n → ℝ => sortedSample n x r) ⁻¹' Iic t = {x | r.val + 1 ≤ ((Finset.univ : Finset (Fin n)).filter (fun i => x i ≤ t)).card} := by ext x exact sortedSample_le_iff_count_le x r t rw [ht] have hcount_t : Measurable (fun x : Fin n → ℝ => ((Finset.univ : Finset (Fin n)).filter (fun i => x i ≤ t)).card) := by have hsum : Measurable (fun x : Fin n → ℝ => ∑ i : Fin n, if x i ≤ t then (1 : ℕ) else 0) := by apply Finset.measurable_sum intro i hi exact Measurable.ite ((measurable_pi_apply i) measurableSet_Iic) measurable_const measurable_const simpa only [Finset.card_filter] using hsum exact measurableSet_le measurable_const hcount_t have hpre : (fun x : Fin n → ℝ => sortedSample n x r) ⁻¹' Iic u = count ⁻¹' (Icc (r.val + 1) n : Set ℕ) := by ext x simp only [Set.mem_preimage, Set.mem_Iic, Finset.mem_coe, Finset.mem_Icc] constructor · intro hx exact ⟨(sortedSample_le_iff_count_le x r u).mp hx, by simpa only [count, Finset.card_univ, Fintype.card_fin] using Finset.card_le_card (filter_subset (fun i => x i ≤ u) Finset.univ)⟩ · intro hx exact (sortedSample_le_iff_count_le x r u).mpr hx.1 rw [Measure.map_apply hsorted measurableSet_Iic, hpre] rw [← MeasureTheory.sum_measure_preimage_singleton (μ := iidSample uniform01 n) (Icc (r.val + 1) n) (fun k hk => hcount (measurableSet_singleton k))] calc ∑ k ∈ Icc (r.val + 1) n, iidSample uniform01 n (count ⁻¹' {k}) = ∑ k ∈ Icc (r.val + 1) n, ofReal ((Nat.choose n k : ℝ) * u ^ k * (1 - u) ^ (n - k)) := by apply Finset.sum_congr rfl intro k hk exact uniform_count_le_mass n k hu _ = _ := by rw [ENNReal.ofReal_sum_of_nonneg] intro k hk have hu0 : 0 ≤ u := hu.1 have hu1 : 0 ≤ 1 - u := sub_nonneg.mpr hu.2 positivity