Stat.Concentration.Conditional­Bernstein

theorem jointCount_sub_conditionalMean (key : D → C) (K : Kernel D Y) (bin : Set Y) (c : C) (x : Fin n → D) (y : Fin n → Y) : (jointCount key bin c x y : ℝ) - conditionalMean key K bin c x = ∑ i, centeredSummand key K bin c x i y := by classical simp only [jointCount, Nat.cast_sum, conditionalMean, centeredSummand, mul_sub, Finset.sum_sub_distrib] congr 1 apply Finset.sum_congr rfl intro i _ by_cases hc : key (x i) = c <;> by_cases hy : y i ∈ bin <;> simp [cellIndicator, binIndicator, hc, hy]

theorem bernstein_sum_totalVariance_abs_gt {Ω : Type*} [MeasurableSpace Ω] {μ : Measure Ω} [IsProbabilityMeasure μ] {n : ℕ} {X : Fin n → Ω → ℝ} {v u : ℝ} (hv : 0 ≤ v) (hu : 0 ≤ u) (hindep : iIndepFun X μ) (hmeas : ∀ i, Measurable (X i)) (hint : ∀ i, Integrable (X i) μ) (hsqint : ∀ i, Integrable (fun ω => X i ω ^ 2) μ) (hmean : ∀ i, ∫ ω, X i ω ∂μ = 0) (habs : ∀ i, ∀ᵐ ω ∂μ, |X i ω| ≤ 1) (hsecond : (∑ i, ∫ ω, X i ω ^ 2 ∂μ) ≤ v) : μ.real {ω | bernsteinRadius v u < |∑ i, X i ω|} ≤ 2 * exp (-u) := by classical by_cases hn : n = 0 · subst n have hempty : {ω | bernsteinRadius v u < |∑ i : Fin 0, X i ω|} = ∅ := by ext ω simp [not_lt.mpr (bernsteinRadius_nonneg v hu)] rw [hempty] simp only [measureReal_empty] positivity by_cases hu0 : u = 0 · subst u have hprob : μ.real {ω | bernsteinRadius v 0 < |∑ i, X i ω|} ≤ 1 := by calc _ ≤ μ.real univ := measureReal_mono (Set.subset_univ _) _ = 1 := probReal_univ simp only [neg_zero, Real.exp_zero, mul_one] linarith by_cases hv0 : v = 0 · subst v have hnonneg (i : Fin n) : 0 ≤ ∫ ω, X i ω ^ 2 ∂μ := integral_nonneg (fun ω => sq_nonneg (X i ω)) have hzero (i : Fin n) : ∫ ω, X i ω ^ 2 ∂μ = 0 := by have hle := Finset.single_le_sum (fun j _ => hnonneg j) (Finset.mem_univ i) exact le_antisymm (hle.trans hsecond) (hnonneg i) have hXzero (i : Fin n) : ∀ᵐ ω ∂μ, X i ω = 0 := by have hsqzero := (integral_eq_zero_iff_of_nonneg (fun ω => sq_nonneg (X i ω)) (hsqint i)).mp (hzero i) filter_upwards [hsqzero] with ω hω change X i ω ^ 2 = 0 at hω nlinarith have hall : ∀ᵐ ω ∂μ, ∀ i, X i ω = 0 := (ae_all_iff).mpr hXzero have hnull : μ {ω | bernsteinRadius 0 u < |∑ i, X i ω|} = 0 := by have hae : ∀ᵐ ω ∂μ, ¬bernsteinRadius 0 u < |∑ i, X i ω| := by filter_upwards [hall] with ω hω simp [hω, not_lt.mpr (bernsteinRadius_nonneg 0 hu)] simpa only [not_not] using ae_iff.mp hae rw [(measureReal_eq_zero_iff).mpr hnull] positivity have hvpos : 0 < v := lt_of_le_of_ne hv (Ne.symm hv0) have hrnonneg : 0 ≤ bernsteinRadius v u := bernsteinRadius_nonneg v hu have hden : 0 < 2 * (v + bernsteinRadius v u / 3) := by positivity have hradius : 2 * u * (v + bernsteinRadius v u / 3) ≤ bernsteinRadius v u ^ 2 := by have hsqrt := Real.sq_sqrt (show 0 ≤ 2 * v * u by positivity) have hsu : 0 ≤ sqrt (2 * v * u) * u := mul_nonneg (Real.sqrt_nonneg _) hu dsimp [bernsteinRadius] nlinarith [sq_nonneg u] have hexp : exp (-bernsteinRadius v u ^ 2 / (2 * (v + bernsteinRadius v u / 3))) ≤ exp (-u) := by apply Real.exp_le_exp.mpr rw [div_le_iff₀ hden] nlinarith [hradius] have hupper (i : Fin n) : ∀ᵐ ω ∂μ, X i ω ≤ 1 := (habs i).mono (fun ω hω => (le_abs_self _).trans hω) have hlower (i : Fin n) : ∀ᵐ ω ∂μ, -X i ω ≤ 1 := (habs i).mono (fun ω hω => (neg_le_abs _).trans hω) have hpos := (bernstein_sum_totalVariance_ge hvpos hrnonneg hindep hmeas hint hsqint hmean hupper hsecond).trans hexp have hnegindep : iIndepFun (fun i ω => -X i ω) μ := hindep.comp (fun _ x => -x) (fun _ => measurable_neg) have hnegsq (i : Fin n) : Integrable (fun ω => (-X i ω) ^ 2) μ := by simpa only [neg_sq] using hsqint i have hnegmean (i : Fin n) : ∫ ω, -X i ω ∂μ = 0 := by rw [integral_neg, hmean i, neg_zero] have hnegsecond : (∑ i, ∫ ω, (-X i ω) ^ 2 ∂μ) ≤ v := by simpa only [neg_sq] using hsecond have hneg := (bernstein_sum_totalVariance_ge hvpos hrnonneg hnegindep (fun i => (hmeas i).neg) (fun i => (hint i).neg) hnegsq hnegmean hlower hnegsecond).trans hexp calc μ.real {ω | bernsteinRadius v u < |∑ i, X i ω|} ≤ μ.real ({ω | bernsteinRadius v u ≤ ∑ i, X i ω} ∪ {ω | bernsteinRadius v u ≤ ∑ i, -X i ω}) := by refine measureReal_mono ?_ (by finiteness) intro ω hω change bernsteinRadius v u < |∑ i, X i ω| at hω rcases lt_abs.mp hω with hω | hω · exact inl hω.le · exact inr (by simpa only [Set.mem_ofPred_eq, Finset.sum_neg_distrib] using hω.le) _ ≤ μ.real {ω | bernsteinRadius v u ≤ ∑ i, X i ω} + μ.real {ω | bernsteinRadius v u ≤ ∑ i, -X i ω} := measureReal_union_le _ _ _ ≤ 2 * exp (-u) := by linarith

theorem fibre_simultaneous_tail_le [Fintype C] [Fintype B] (key : D → C) (K : Kernel D Y) [IsMarkovKernel K] (bins : B → Set Y) (hbins : ∀ b, MeasurableSet (bins b)) (x : Fin n → D) {pMax u : ℝ} (hpMax : 0 ≤ pMax) (hu : 0 ≤ u) (hprob : ∀ c b i, key (x i) = c → binProbability K (bins b) (x i) ≤ pMax) : (finProductKernel n K x).real (Prod.mk x ⁻¹' histogramBadEvent key K bins pMax u) ≤ 2 * (Fintype.card C : ℝ) * (Fintype.card B : ℝ) * exp (-u) := by classical let events : C × B → Set (Fin n → Y) := fun q => {y | bernsteinRadius (pMax * (cellCount key q.1 x : ℝ)) u < |(jointCount key (bins q.2) q.1 x y : ℝ) - conditionalMean key K (bins q.2) q.1 x|} have hevent : Prod.mk x ⁻¹' histogramBadEvent key K bins pMax u = ⋃ q : C × B, events q := by ext y simp only [histogramBadEvent, Set.mem_preimage, Set.mem_ofPred_eq, Set.mem_iUnion, events] exact ⟨fun ⟨c, b, h⟩ => ⟨(c, b), h⟩, fun ⟨q, h⟩ => ⟨q.1, q.2, h⟩⟩ rw [hevent] calc _ ≤ ∑ q : C × B, (finProductKernel n K x).real (events q) := measureReal_iUnion_fintype_le events _ ≤ ∑ _q : C × B, 2 * exp (-u) := Finset.sum_le_sum (fun q _ => fibre_pair_tail_le key K q.1 x (hbins q.2) hpMax hu (hprob q.1 q.2)) _ = _ := by simp only [Finset.sum_const, Finset.card_univ, Fintype.card_prod, nsmul_eq_mul, Nat.cast_mul] ring

theorem integral_sq_centered_bin (hbin : MeasurableSet bin) : (∫ y, (binIndicator bin y - μ.real bin) ^ 2 ∂μ) = μ.real bin * (1 - μ.real bin) := by have hi : Integrable (binIndicator bin) μ := (integrable_const (1 : ℝ)).indicator hbin have hexpand : (fun y => (binIndicator bin y - μ.real bin) ^ 2) = (fun y => (1 - 2 * μ.real bin) * binIndicator bin y + μ.real bin ^ 2) := by funext y by_cases hy : y ∈ bin · simp [binIndicator, hy] ring · simp [binIndicator, hy] rw [hexpand, integral_add (hi.const_mul _) (integrable_const _), integral_const_mul] simp only [binIndicator, integral_indicator_const (1 : ℝ) hbin, smul_eq_mul, mul_one, integral_const, probReal_univ, one_mul] ring

theorem iid_joint_map_split {D Y : Type*} [MeasurableSpace D] [MeasurableSpace Y] (n : ℕ) (Q : Measure D) [IsProbabilityMeasure Q] (K : Kernel D Y) [IsMarkovKernel K] : (Measure.pi (fun _ : Fin n => Q ⊗ₘ K)).map (fun z => (fun i => (z i).1, fun i => (z i).2)) = Measure.pi (fun _ : Fin n => Q) ⊗ₘ Causalean.Stat.finProductKernel n K := by classical let d₀ : D := choice (nonempty_of_isProbabilityMeasure Q) let split := MeasurableEquiv.arrowProdEquivProdArrow D Y (Fin n) let pairLaw : Measure (D × Y) := Q ⊗ₘ K let designLaw : Measure (Fin n → D) := Measure.pi (fun _ : Fin n => Q) let markKernel := Causalean.Stat.finProductKernel n K let : IsProbabilityMeasure pairLaw := by dsimp only [pairLaw] infer_instance let : IsProbabilityMeasure (Measure.pi (fun _ : Fin n => pairLaw)) := inferInstance let : IsProbabilityMeasure designLaw := by dsimp only [designLaw] infer_instance let : IsMarkovKernel markKernel := by dsimp only [markKernel] infer_instance let lhs := (Measure.pi (fun _ : Fin n => pairLaw)).map split let rhs := designLaw ⊗ₘ markKernel change lhs = rhs refine Measure.FiniteSpanningSetsIn.ext ?_ (isPiSystem_pi.prod isPiSystem_pi) ?_ ?_ · refine (generateFrom_eq_prod generateFrom_pi generateFrom_pi ?_ ?_).symm · exact (Measure.FiniteSpanningSetsIn.pi (fun _ : Fin n => Q.toFiniteSpanningSetsIn)).isCountablySpanning · exact (Measure.FiniteSpanningSetsIn.pi (fun _ : Fin n => (K d₀).toFiniteSpanningSetsIn)).isCountablySpanning · let base := (Measure.pi (fun _ : Fin n => Q)).prod (Measure.pi (fun _ : Fin n => (K d₀))) let hbase := (Measure.FiniteSpanningSetsIn.pi (fun _ : Fin n => Q.toFiniteSpanningSetsIn)).prod (Measure.FiniteSpanningSetsIn.pi (fun _ : Fin n => (K d₀).toFiniteSpanningSetsIn)) exact ⟨hbase.set, hbase.set_mem, fun i => measure_lt_top _ _, hbase.spanning⟩ · rintro _ ⟨s, ⟨s, hs, rfl⟩, ⟨_, ⟨t, ht, rfl⟩, rfl⟩⟩ have hs' : ∀ i, MeasurableSet (s i) := fun i => hs i (Set.mem_univ i) have ht' : ∀ i, MeasurableSet (t i) := fun i => ht i (Set.mem_univ i) have hdesignSet : MeasurableSet (Set.univ.pi s) := MeasurableSet.pi Set.finite_univ.countable (fun i _ => hs' i) have hmarkSet : MeasurableSet (Set.univ.pi t) := MeasurableSet.pi Set.finite_univ.countable (fun i _ => ht' i) simp only [lhs, rhs] rw [Measure.map_apply split.measurable (hdesignSet.prod hmarkSet)] rw [show split ⁻¹' (Set.univ.pi s ×ˢ Set.univ.pi t) = Set.univ.pi (fun i => s i ×ˢ t i) by ext x simp only [split, MeasurableEquiv.arrowProdEquivProdArrow, MeasurableEquiv.coe_mk, Set.mem_preimage, Set.mem_prod, Set.mem_pi, Set.mem_univ, true_implies, Equiv.arrowProdEquivProdArrow_apply, forall_and]] rw [Measure.pi_pi, Measure.compProd_apply_prod hdesignSet hmarkSet] simp_rw [pairLaw, Measure.compProd_apply_prod (hs' _) (ht' _)] simp only [markKernel] simp_rw [finProductKernel_apply, Measure.pi_pi] let X : Fin n → (Fin n → D) → ENNReal := fun i d => indicator (s i) (fun x => K x (t i)) (d i) have hXmeas : ∀ i, Measurable (X i) := fun i => ((K.measurable_coe (ht' i)).indicator (hs' i)).comp (measurable_pi_apply i) have hXindep : iIndepFun X designLaw := by have heval : iIndepFun (fun i (d : Fin n → D) => d i) designLaw := by simpa only [designLaw, id_eq] using (iIndepFun_pi (X := fun _ => id) (fun _ => measurable_id.aemeasurable)) change iIndepFun (fun i => (fun x => indicator (s i) (fun z => K z (t i)) x) ∘ fun d : Fin n → D => d i) designLaw exact heval.comp (fun i x => indicator (s i) (fun z => K z (t i)) x) (fun i => (K.measurable_coe (ht' i)).indicator (hs' i)) rw [← lintegral_indicator hdesignSet] change (∏ i, ∫⁻ x in s i, K x (t i) ∂Q) = ∫⁻ d, indicator (Set.univ.pi s) (fun d => ∏ i, K (d i) (t i)) d ∂designLaw rw [show (fun d => indicator (Set.univ.pi s) (fun d => ∏ i, K (d i) (t i)) d) = fun d => ∏ i, X i d by funext d by_cases hd : ∀ i, d i ∈ s i · rw [Set.indicator_of_mem (show d ∈ Set.univ.pi s from fun i _ => hd i)] exact Finset.prod_congr rfl fun i _ => by simp [X, hd i] · rw [Set.indicator_of_notMem (show d ∉ Set.univ.pi s by intro hmem exact hd fun i => hmem i (Set.mem_univ i))] push Not at hd obtain ⟨i, hi⟩ := hd symm exact Finset.prod_eq_zero (Finset.mem_univ i) (by simp [X, hi])] rw [lintegral_prod_eq_prod_lintegral_of_indepFun univ X hXindep hXmeas] apply Finset.prod_congr rfl intro i _ calc (∫⁻ x in s i, K x (t i) ∂Q) = ∫⁻ x, indicator (s i) (fun z => K z (t i)) x ∂Q := (lintegral_indicator (hs' i) _).symm _ = ∫⁻ d, X i d ∂designLaw := ((measurePreserving_eval (fun _ : Fin n => Q) i).lintegral_comp ((K.measurable_coe (ht' i)).indicator (hs' i))).symm

theorem fibre_pair_tail_le (hbin : MeasurableSet bin) {pMax u : ℝ} (hpMax : 0 ≤ pMax) (hu : 0 ≤ u) (hprob : ∀ i, key (x i) = c → binProbability K bin (x i) ≤ pMax) : (finProductKernel n K x).real {y | bernsteinRadius (pMax * (cellCount key c x : ℝ)) u < |(jointCount key bin c x y : ℝ) - conditionalMean key K bin c x|} ≤ 2 * exp (-u) := by have hv : 0 ≤ pMax * (cellCount key c x : ℝ) := mul_nonneg hpMax (Nat.cast_nonneg _) simpa only [jointCount_sub_conditionalMean] using bernstein_sum_totalVariance_abs_gt hv hu (iIndepFun_centeredSummand key K c x hbin) (measurable_centeredSummand key K c x hbin) (integrable_centeredSummand key K c x hbin) (integrable_sq_centeredSummand key K c x hbin) (integral_centeredSummand key K c x hbin) (fun i => Filter.Eventually.of_forall (abs_centeredSummand_le_one key K c x i)) (sum_second_moments_le key K c x hbin hprob)

theorem iid_joint_simultaneous_tail_le [Fintype C] [Fintype B] (Q : Measure D) [IsProbabilityMeasure Q] (K : Kernel D Y) [IsMarkovKernel K] (key : D → C) (bins : B → Set Y) (hcell : ∀ c, MeasurableSet {d | key d = c}) (hbins : ∀ b, MeasurableSet (bins b)) {pMax u : ℝ} (hpMax : 0 ≤ pMax) (hu : 0 ≤ u) (henvelope : ∀ᵐ d ∂Q, ∀ c b, key d = c → binProbability K (bins b) d ≤ pMax) : (Measure.pi (fun _ : Fin n => Q ⊗ₘ K)).real {z | ∃ c b, bernsteinRadius (pMax * (cellCount key c (fun i => (z i).1) : ℝ)) u < |(jointCount key (bins b) c (fun i => (z i).1) (fun i => (z i).2) : ℝ) - conditionalMean key K (bins b) c (fun i => (z i).1)|} ≤ 2 * (Fintype.card C : ℝ) * (Fintype.card B : ℝ) * exp (-u) := by have hsplit : Measurable (fun z : Fin n → D × Y => (fun i => (z i).1, fun i => (z i).2)) := (measurable_pi_lambda _ (fun i => (measurable_pi_apply i).fst)).prodMk (measurable_pi_lambda _ (fun i => (measurable_pi_apply i).snd)) have hmap := Measure.map_apply hsplit (measurableSet_histogramBadEvent (n := n) key K bins hcell hbins pMax u) (μ := Measure.pi (fun _ : Fin n => Q ⊗ₘ K)) rw [iid_joint_map_split n Q K] at hmap have hreal := congrArg toReal hmap change (Measure.pi (fun _ : Fin n => Q) ⊗ₘ finProductKernel n K).real (histogramBadEvent key K bins pMax u) = (Measure.pi (fun _ : Fin n => Q ⊗ₘ K)).real {z | ∃ c b, bernsteinRadius (pMax * (cellCount key c (fun i => (z i).1) : ℝ)) u < |(jointCount key (bins b) c (fun i => (z i).1) (fun i => (z i).2) : ℝ) - conditionalMean key K (bins b) c (fun i => (z i).1)|} at hreal rw [← hreal] exact attached_simultaneous_tail_le Q K key bins hcell hbins hpMax hu henvelope