Stat.Random­Graph.Path­Occupancy

theorem connected_run_cover {K : ℕ} (s : Finset (Fin K)) (hs : s.Nonempty) (hc : PathConnected s) : ∃ a ∈ s, ∀ b ∈ s, a.val ≤ b.val ∧ b.val < a.val + s.card := by obtain ⟨a, ha, hmin⟩ := Finset.exists_min_image s val hs refine ⟨a, ha, fun b hb => ⟨hmin b hb, ?_⟩⟩ have hsub : Icc a.val b.val ⊆ s.image val := by intro n hn obtain ⟨han, hnb⟩ := Finset.mem_Icc.mp hn let c : Fin K := ⟨n, lt_of_le_of_lt hnb b.isLt⟩ exact Finset.mem_image.mpr ⟨c, hc a ha b hb c han hnb, rfl⟩ have hcard := (Finset.card_le_card hsub).trans Finset.card_image_le rw [Nat.card_Icc] at hcard have hab := hmin b hb omega

theorem pairedScore_le_subsets {n K : ℕ} (M : ℕ) (x : Fin n → Fin K) (R : Fin n → Fin n → Prop) (b : Fin n → Bool) (hR : Admissible M x R) : pairedScore M R x b ≤ (1 / 2 : ℝ) * ∑ C ∈ Finset.univ.powerset, ∑ D ∈ Finset.univ.powerset, if Disjoint C D ∧ PathConnected (C.image x) ∧ PathConnected (D.image x) then pairWeight M C D x b else 0 := by let f : Finset (Fin n) → Finset (Fin n) → ℝ := fun C D => if Disjoint C D ∧ PathConnected (C.image x) ∧ PathConnected (D.image x) then pairWeight M C D x b else 0 have hn : ∀ C D, 0 ≤ f C D := by intro C D dsimp [f] split_ifs · unfold pairWeight split_ifs <;> positivity · exact le_rfl have hsub : components R ⊆ Finset.univ.powerset := by intro C _ exact Finset.mem_powerset.mpr (Finset.subset_univ C) unfold pairedScore apply mul_le_mul_of_nonneg_left _ (by norm_num) calc _ = ∑ C ∈ components R, ∑ D ∈ (components R).erase C, f C D := by apply Finset.sum_congr rfl intro C hC apply Finset.sum_congr rfl intro D hD obtain ⟨hne, hD⟩ := Finset.mem_erase.mp hD have hdis := (components_partition R).2.2 C hC D hD hne.symm dsimp [f] rw [if_pos ⟨hdis, (component_geometry M x R hR C hC).1, (component_geometry M x R hR D hD).1⟩] _ ≤ ∑ C ∈ components R, ∑ D ∈ Finset.univ.powerset, f C D := by apply Finset.sum_le_sum intro C _ exact Finset.sum_le_sum_of_subset_of_nonneg ((Finset.erase_subset C (components R)).trans hsub) (fun D _ _ => hn C D) _ ≤ _ := Finset.sum_le_sum_of_subset_of_nonneg hsub (by intro C _ _ exact Finset.sum_nonneg (fun D _ => hn C D))

theorem fixed_subset_assignment_mark_probability {n K : ℕ} {μ : Measure Ω} {X : Fin n → Ω → Fin K} {B : Fin n → Ω → Bool} {ε : ℝ} (h : UniformMarkedSample μ X B ε) (s t : Finset (Fin n)) (a : s → Fin K) (b : t → Bool) : μ {ω | (∀ i : s, X i ω = a i) ∧ (∀ i : t, B i ω = b i)} = (K : ℝ≥0∞)⁻¹ ^ s.card * ∏ i : t, ofReal (if b i = true then ε else 1 - ε) := by classical have hi := h.marks_independent.precomp (g := fun i : t => (i : Fin n)) val_injective have hp := hi.measure_inter_preimage_eq_mul Finset.univ (sets := fun i => {b i}) (fun _ _ => MeasurableSet.singleton _) have hm : μ {ω | ∀ i : t, B i ω = b i} = ∏ i : t, ofReal (if b i = true then ε else 1 - ε) := by have he : (⋂ i ∈ (Finset.univ : Finset t), B (i : Fin n) ⁻¹' {b i}) = {ω | ∀ i : t, B i ω = b i} := by ext ω; simp rw [he] at hp simp only [preimage, Set.mem_singleton_iff] at hp exact hp.trans (Finset.prod_congr rfl (fun i _ => h.marks_bernoulli i (b i))) have hb := h.blocks_independent.measure_inter_preimage_eq_mul {x | ∀ i : s, x i = a i} {y | ∀ i : t, y i = b i} (by simpa only [preimage, Set.mem_singleton_iff, Set.iInter_ofPred] using (MeasurableSet.iInter fun i : s => (measurable_pi_apply (i : Fin n) : Measurable (fun x : Fin n → Fin K => x i)) (MeasurableSet.singleton (a i)))) (by simpa only [preimage, Set.mem_singleton_iff, Set.iInter_ofPred] using (MeasurableSet.iInter fun i : t => (measurable_pi_apply (i : Fin n) : Measurable (fun x : Fin n → Bool => x i)) (MeasurableSet.singleton (b i)))) change μ {ω | (∀ i : s, X i ω = a i) ∧ (∀ i : t, B i ω = b i)} = _ at hb rw [hb] change μ {ω | ∀ i : s, X i ω = a i} * μ {ω | ∀ i : t, B i ω = b i} = _ rw [fixed_subset_assignment_probability h, hm]

theorem occupancySeries_geometric_le (p n K : ℕ) (hp : p ≤ 11) (hK : 0 < K) (hdensity : (n : ℝ) / K ≤ (2 : ℝ) ^ (-40 : ℤ)) : occupancySeries p n K ≤ 2 * (2 : ℝ) ^ p * occupancyZ n K ^ 2 := by obtain ⟨hz, hzsmall⟩ := occupancyZ_small n K hK hdensity have hratio : (2 : ℝ) ^ p * occupancyZ n K ≤ 1 / 2 := by calc _ ≤ (2 : ℝ) ^ 11 * (2 : ℝ) ^ (-35 : ℤ) := by exact mul_le_mul (pow_le_pow_right₀ (by norm_num : (1 : ℝ) ≤ 2) hp) hzsmall hz (by positivity) _ ≤ 1 / 2 := by norm_num let t : ℕ → ℝ := fun j => (j + 2 : ℝ) ^ p * occupancyZ n K ^ (j + 2) have ht : ∀ j, 0 ≤ t j := by intro j dsimp [t] positivity have hstep : ∀ j, t (j + 1) ≤ t j / 2 := by intro j have hbase : (j : ℝ) + 1 + 2 ≤ 2 * ((j : ℝ) + 2) := by have : (0 : ℝ) ≤ j := Nat.cast_nonneg j linarith calc t (j + 1) ≤ (2 * ((j : ℝ) + 2)) ^ p * occupancyZ n K ^ (j + 1 + 2) := by dsimp [t] push_cast gcongr _ = t j * ((2 : ℝ) ^ p * occupancyZ n K) := by dsimp [t] rw [show j + 1 + 2 = (j + 2) + 1 by omega, pow_succ, mul_pow] ring _ ≤ t j * (1 / 2) := mul_le_mul_of_nonneg_left hratio (ht j) _ = t j / 2 := by ring have hsum : ∀ N, (∑ j ∈ range N, t j) + 2 * t N ≤ 2 * t 0 := by intro N induction N with | zero => simp | succ N ih => rw [Finset.sum_range_succ] have := hstep N change (∑ j ∈ range N, t j) + t N + 2 * t (N + 1) ≤ 2 * t 0 linarith have hb := hsum (n - 1) have hn := ht (n - 1) have : (∑ j ∈ range (n - 1), t j) ≤ 2 * t 0 := by linarith simpa [occupancySeries, t, mul_assoc] using this

theorem single_component_occupancy {n M K : ℕ} {μ : Measure Ω} {X : Fin n → Ω → Fin K} {B : Fin n → Ω → Bool} {ε : ℝ} (h : UniformMarkedSample μ X B ε) (hn : 2 ≤ n) (hM : 2 ≤ M) (heven : 2 ∣ M) (hKM : 16 * M ≤ K) (R : Ω → Fin n → Fin n → Prop) (hR : ∀ i j, MeasurableSet {ω | R ω i j}) (hlocal : ∀ ω, Admissible M (fun i => X i ω) (R ω)) : (∫ ω, singleScore (R ω) (fun i => B i ω) ∂μ) ≤ ε ^ 2 * K * occupancySeries 11 n K := by have hK : 0 < K := by omega calc _ ≤ ε ^ 2 * K * ∑ m ∈ Icc 2 n, (n.choose m : ℝ) * (m : ℝ) ^ 10 * 8 ^ m * (m : ℝ) ^ m / (K : ℝ) ^ m := single_expectation_labelled_le h M hK R hR hlocal _ ≤ ε ^ 2 * K * occupancySeries 11 n K := mul_le_mul_of_nonneg_left (finite_labelled_weight_majorant 10 n K hn hK) (by positivity)

theorem paired_component_occupancy {n M K : ℕ} {μ : Measure Ω} {X : Fin n → Ω → Fin K} {B : Fin n → Ω → Bool} {ε : ℝ} (h : UniformMarkedSample μ X B ε) (hn : 2 ≤ n) (hM : 2 ≤ M) (heven : 2 ∣ M) (hdiv : M ∣ K) (hKM : 16 * M ≤ K) (R : Ω → Fin n → Fin n → Prop) (hR : ∀ i j, MeasurableSet {ω | R ω i j}) (hlocal : ∀ ω, Admissible M (fun i => X i ω) (R ω)) : (∫ ω, pairedScore M (R ω) (fun i => X i ω) (fun i => B i ω) ∂μ) ≤ 2 * ε ^ 2 * (K : ℝ) ^ 2 / M * (occupancySeries 6 n K) ^ 2 := by have hK : 0 < K := by omega have hMp : 0 < M := by omega have hsum_nonneg : 0 ≤ (∑ m ∈ Icc 2 n, (n.choose m : ℝ) * (m : ℝ) ^ 5 * 8 ^ m * (m : ℝ) ^ m / (K : ℝ) ^ m) := by exact Finset.sum_nonneg (fun m _ => by positivity) have hmajorant := finite_labelled_weight_majorant 5 n K hn hK calc _ ≤ 2 * ε ^ 2 * (K : ℝ) ^ 2 / M * (∑ m ∈ Icc 2 n, (n.choose m : ℝ) * (m : ℝ) ^ 5 * 8 ^ m * (m : ℝ) ^ m / (K : ℝ) ^ m) ^ 2 := paired_expectation_labelled_le h M hMp hK heven hdiv R hR hlocal _ ≤ 2 * ε ^ 2 * (K : ℝ) ^ 2 / M * (occupancySeries 6 n K) ^ 2 := by apply mul_le_mul_of_nonneg_left _ (by positivity) exact pow_le_pow_left₀ hsum_nonneg hmajorant 2

theorem unordered_same_pair_count (K M : ℕ) (hM : 0 < M) (hK : 0 < K) (heven : 2 ∣ M) (hdiv : M ∣ K) : M * card {p : Fin K × Fin K // p.1.val < p.2.val ∧ pairClass K M p.1 = pairClass K M p.2} ≤ K ^ 2 := by classical let U := {p : Fin K × Fin K // p.1.val < p.2.val ∧ pairClass K M p.1 = pairClass K M p.2} let O := {p : Fin K × Fin K // pairClass K M p.1 = pairClass K M p.2} let f : Bool × U → O := fun t => if t.1 then ⟨(t.2.val.2, t.2.val.1), t.2.property.2.symm⟩ else ⟨t.2.val, t.2.property.2⟩ have hf : Injective f := by rintro ⟨b, p⟩ ⟨c, q⟩ h have hv := congrArg val h cases b <;> cases c · have hpq : p = q := Subtype.ext (by simpa [f] using hv) subst q; rfl · have h₁ := congrArg (fun t : Fin K × Fin K => t.1.val) hv have h₂ := congrArg (fun t : Fin K × Fin K => t.2.val) hv simp only [f, Bool.false_eq_true, ↓reduceIte] at h₁ h₂ have hp := p.property.1 have hq := q.property.1 omega · have h₁ := congrArg (fun t : Fin K × Fin K => t.1.val) hv have h₂ := congrArg (fun t : Fin K × Fin K => t.2.val) hv simp only [f, Bool.false_eq_true, ↓reduceIte] at h₁ h₂ have hp := p.property.1 have hq := q.property.1 omega · have hpq : p = q := Subtype.ext (by apply Prod.ext · exact congrArg snd hv · exact congrArg fst hv) subst q; rfl have hc : 2 * card U ≤ card O := by have := Nat.card_le_card_of_injective f hf simpa [Nat.card_prod, Nat.card_eq_fintype_card] using this have ho := ordered_same_pair_count K M hM hK heven hdiv have hb := Nat.mul_le_mul_left M hc change M * card U ≤ K ^ 2 change M * card O = 2 * K ^ 2 at ho nlinarith

theorem connected_assignment_count {ι : Type*} [Fintype ι] (K : ℕ) (hm : 1 ≤ card ι) : card {x : ι → Fin K // ConnectedAssignment x} ≤ K * card ι ^ card ι := by obtain ⟨encode, hinj, _⟩ := connected_assignment_encoding K hm simpa [Nat.card_prod, Nat.card_fun, Nat.card_fin, Nat.card_eq_fintype_card] using Nat.card_le_card_of_injective encode hinj

theorem connected_same_pair_assignment_count {ι κ : Type*} [Fintype ι] [Fintype κ] (K M : ℕ) (hm : 1 ≤ card ι) (hl : 1 ≤ card κ) (hM : 0 < M) (hK : 0 < K) (heven : 2 ∣ M) (hdiv : M ∣ K) : M * card {p : (ι → Fin K) × (κ → Fin K) // ConnectedAssignment p.1 ∧ ConnectedAssignment p.2 ∧ SamePair K M p.1 p.2} ≤ 2 * K ^ 2 * card ι ^ card ι * card κ ^ card κ := by classical obtain ⟨eι, heι, haι⟩ := connected_assignment_encoding K hm obtain ⟨eκ, heκ, haκ⟩ := connected_assignment_encoding K hl let P := {p : (ι → Fin K) × (κ → Fin K) // ConnectedAssignment p.1 ∧ ConnectedAssignment p.2 ∧ SamePair K M p.1 p.2} let O := {p : Fin K × Fin K // pairClass K M p.1 = pairClass K M p.2} let x (p : P) : {x : ι → Fin K // ConnectedAssignment x} := ⟨p.val.1, p.property.1⟩ let y (p : P) : {y : κ → Fin K // ConnectedAssignment y} := ⟨p.val.2, p.property.2.1⟩ have hanchors (p : P) : pairClass K M (eι (x p)).1 = pairClass K M (eκ (y p)).1 := by obtain ⟨i, _, hi⟩ := Finset.mem_image.mp (haι (x p)).1 obtain ⟨j, _, hj⟩ := Finset.mem_image.mp (haκ (y p)).1 obtain ⟨c, _, hx, hy⟩ := p.property.2.2 rw [← hi, ← hj] exact (hx i).trans (hy j).symm let encode : P → O × ((ι → Fin (card ι)) × (κ → Fin (card κ))) := fun p => (⟨((eι (x p)).1, (eκ (y p)).1), hanchors p⟩, (eι (x p)).2, (eκ (y p)).2) have hinj : Injective encode := by intro p q hpq have hx : x p = x q := heι (Prod.ext (congrArg (fun t => t.1.val.1) hpq) (congrArg (fun t => t.2.1) hpq)) have hy : y p = y q := heκ (Prod.ext (congrArg (fun t => t.1.val.2) hpq) (congrArg (fun t => t.2.2) hpq)) exact Subtype.ext (Prod.ext (congrArg val hx) (congrArg val hy)) have hc : card P ≤ card O * (card ι ^ card ι * card κ ^ card κ) := by simpa [Nat.card_prod, Nat.card_fun, Nat.card_fin, Nat.card_eq_fintype_card] using Nat.card_le_card_of_injective encode hinj have ho : M * card O = 2 * K ^ 2 := ordered_same_pair_count K M hM hK heven hdiv calc M * card P ≤ M * (card O * (card ι ^ card ι * card κ ^ card κ)) := Nat.mul_le_mul_left M hc _ = (M * card O) * (card ι ^ card ι * card κ ^ card κ) := by ring _ = 2 * K ^ 2 * card ι ^ card ι * card κ ^ card κ := by rw [ho]; ring

theorem paired_expectation_labelled_le {n K : ℕ} {μ : Measure Ω} {X : Fin n → Ω → Fin K} {B : Fin n → Ω → Bool} {ε : ℝ} (h : UniformMarkedSample μ X B ε) (M : ℕ) (hM : 0 < M) (hK : 0 < K) (heven : 2 ∣ M) (hdiv : M ∣ K) (R : Ω → Fin n → Fin n → Prop) (hR : ∀ i j, MeasurableSet {ω | R ω i j}) (hlocal : ∀ ω, Admissible M (fun i => X i ω) (R ω)) : (∫ ω, pairedScore M (R ω) (fun i => X i ω) (fun i => B i ω) ∂μ) ≤ 2 * ε ^ 2 * (K : ℝ) ^ 2 / M * (∑ m ∈ Icc 2 n, (n.choose m : ℝ) * (m : ℝ) ^ 5 * 8 ^ m * (m : ℝ) ^ m / (K : ℝ) ^ m) ^ 2 := by classical let : IsProbabilityMeasure μ := h.probability let E : Finset (Fin n) → Finset (Fin n) → Set Ω := fun C D => {ω | PathConnected (C.image (fun i => X i ω)) ∧ PathConnected (D.image (fun i => X i ω)) ∧ 1 ≤ markCount C (fun i => B i ω) ∧ 1 ≤ markCount D (fun i => B i ω) ∧ SameCoarsePair M C D (fun i => X i ω)} let w : ℕ → ℝ := fun m => (m : ℝ) ^ 4 * 8 ^ m let q : ℕ → ℝ := fun m => if 2 ≤ m then (m : ℝ) ^ 5 * 8 ^ m * (m : ℝ) ^ m / (K : ℝ) ^ m else 0 let a : ℝ := 2 * ε ^ 2 * (K : ℝ) ^ 2 / M let f : Finset (Fin n) → Finset (Fin n) → Ω → ℝ := fun C D => if Disjoint C D ∧ 2 ≤ C.card ∧ 2 ≤ D.card then (E C D).indicator (fun _ => w C.card * w D.card) else fun _ => 0 have hinput : Measurable (fun ω => (fun i => X i ω, fun i => B i ω)) := (measurable_pi_lambda _ h.cells_measurable).prodMk (measurable_pi_lambda _ h.marks_measurable) have hE (C D : Finset (Fin n)) : MeasurableSet (E C D) := by exact hinput (Set.toFinite {p : (Fin n → Fin K) × (Fin n → Bool) | PathConnected (C.image p.1) ∧ PathConnected (D.image p.1) ∧ 1 ≤ markCount C p.2 ∧ 1 ≤ markCount D p.2 ∧ SameCoarsePair M C D p.1}).measurableSet have hf (C D : Finset (Fin n)) : Integrable (f C D) μ := by dsimp [f] split_ifs · exact (integrable_const _).indicator (hE C D) · exact integrable_const 0 have hq (m : ℕ) : 0 ≤ q m := by dsimp [q]; split_ifs <;> positivity have ha : 0 ≤ a := by dsimp [a]; positivity have hpoint (ω : Ω) : pairedScore M (R ω) (fun i => X i ω) (fun i => B i ω) ≤ (1 / 2 : ℝ) * ∑ C ∈ (Finset.univ : Finset (Fin n)).powerset, ∑ D ∈ (Finset.univ : Finset (Fin n)).powerset, f C D ω := by convert pairedScore_le_subsets M (fun i => X i ω) (R ω) (fun i => B i ω) (hlocal ω) using 1 congr 1 apply Finset.sum_congr rfl intro C _ apply Finset.sum_congr rfl intro D _ simp only [f, E, pairWeight, w] split_ifs <;> simp_all ring have hbound (C D : Finset (Fin n)) : (∫ ω, f C D ω ∂μ) ≤ a * q C.card * q D.card := by by_cases hc : Disjoint C D ∧ 2 ≤ C.card ∧ 2 ≤ D.card · rw [show (∫ ω, f C D ω ∂μ) = μ.real (E C D) * (w C.card * w D.card) by simp only [f, if_pos hc] exact (integral_indicator_const _ (hE C D)).trans (by simp [smul_eq_mul])] have hp := mul_le_mul_of_nonneg_right (subsets_connected_pair_marks_le h M hM hK heven hdiv C D hc.1 hc.2.1 hc.2.2) (show 0 ≤ w C.card * w D.card by dsimp [w]; positivity) calc _ ≤ (a * (C.card : ℝ) ^ (C.card + 1) * (D.card : ℝ) ^ (D.card + 1) / (K : ℝ) ^ (C.card + D.card)) * (w C.card * w D.card) := hp _ = _ := by simp only [q, if_pos hc.2.1, if_pos hc.2.2, w, pow_add, pow_one] ring · simp only [f, if_neg hc, integral_zero] exact mul_nonneg (mul_nonneg ha (hq _)) (hq _) have hgroup : (∑ C ∈ (Finset.univ : Finset (Fin n)).powerset, q C.card) = ∑ m ∈ Icc 2 n, (n.choose m : ℝ) * (m : ℝ) ^ 5 * 8 ^ m * (m : ℝ) ^ m / (K : ℝ) ^ m := by calc _ = ∑ m ∈ range (n + 1), (n.choose m : ℝ) * q m := by rw [Finset.sum_powerset_apply_card] simp only [Finset.card_univ, Fintype.card_fin, nsmul_eq_mul] _ = ∑ m ∈ Icc 2 n, (n.choose m : ℝ) * q m := by symm apply Finset.sum_subset · intro m hm simp only [Finset.mem_Icc] at hm simp only [Finset.mem_range] omega · intro m hm hnot have hsmall : ¬ 2 ≤ m := by simp only [Finset.mem_Icc, not_and_or, not_le] at hnot simp only [Finset.mem_range] at hm omega simp [q, hsmall] _ = _ := by apply Finset.sum_congr rfl intro m hm simp only [q, if_pos (Finset.mem_Icc.mp hm).1] ring have hsum : Integrable (fun ω => ∑ C ∈ (Finset.univ : Finset (Fin n)).powerset, ∑ D ∈ (Finset.univ : Finset (Fin n)).powerset, f C D ω) μ := integrable_finsetSum _ (fun C _ => integrable_finsetSum _ (fun D _ => hf C D)) calc _ ≤ ∫ ω, (1 / 2 : ℝ) * (∑ C ∈ (Finset.univ : Finset (Fin n)).powerset, ∑ D ∈ (Finset.univ : Finset (Fin n)).powerset, f C D ω) ∂μ := integral_mono (integrable_pairedScore μ M R X B hR h.cells_measurable h.marks_measurable) (hsum.const_mul _) hpoint _ = (1 / 2 : ℝ) * ∑ C ∈ (Finset.univ : Finset (Fin n)).powerset, ∑ D ∈ (Finset.univ : Finset (Fin n)).powerset, ∫ ω, f C D ω ∂μ := by rw [integral_const_mul, integral_finsetSum _ (fun C _ => integrable_finsetSum _ (fun D _ => hf C D))] congr 1 apply Finset.sum_congr rfl intro C _ exact integral_finsetSum _ (fun D _ => hf C D) _ ≤ (1 / 2 : ℝ) * ∑ C ∈ (Finset.univ : Finset (Fin n)).powerset, ∑ D ∈ (Finset.univ : Finset (Fin n)).powerset, a * q C.card * q D.card := by exact mul_le_mul_of_nonneg_left (Finset.sum_le_sum (fun C _ => Finset.sum_le_sum (fun D _ => hbound C D))) (by norm_num : (0 : ℝ) ≤ 1 / 2) _ ≤ ∑ C ∈ (Finset.univ : Finset (Fin n)).powerset, ∑ D ∈ (Finset.univ : Finset (Fin n)).powerset, a * q C.card * q D.card := by have hs : 0 ≤ ∑ C ∈ (Finset.univ : Finset (Fin n)).powerset, ∑ D ∈ (Finset.univ : Finset (Fin n)).powerset, a * q C.card * q D.card := Finset.sum_nonneg (fun C _ => Finset.sum_nonneg (fun D _ => mul_nonneg (mul_nonneg ha (hq _)) (hq _))) exact mul_le_of_le_one_left hs (by norm_num) _ = a * (∑ C ∈ (Finset.univ : Finset (Fin n)).powerset, q C.card) ^ 2 := by rw [pow_two, Finset.sum_mul_sum] simp only [Finset.mul_sum, mul_assoc] _ = _ := by rw [hgroup]

theorem subsets_connected_pair_marks_le {n K : ℕ} {μ : Measure Ω} {X : Fin n → Ω → Fin K} {B : Fin n → Ω → Bool} {ε : ℝ} (h : UniformMarkedSample μ X B ε) (M : ℕ) (hM : 0 < M) (hK : 0 < K) (heven : 2 ∣ M) (hdiv : M ∣ K) (C D : Finset (Fin n)) (hdisj : Disjoint C D) (hC : 2 ≤ C.card) (hD : 2 ≤ D.card) : (μ {ω | PathConnected (C.image (fun i => X i ω)) ∧ PathConnected (D.image (fun i => X i ω)) ∧ 1 ≤ markCount C (fun i => B i ω) ∧ 1 ≤ markCount D (fun i => B i ω) ∧ SameCoarsePair M C D (fun i => X i ω)}).toReal ≤ 2 * ε ^ 2 * (K : ℝ) ^ 2 / M * (C.card : ℝ) ^ (C.card + 1) * (D.card : ℝ) ^ (D.card + 1) / (K : ℝ) ^ (C.card + D.card) := by classical have : IsProbabilityMeasure μ := h.probability let A := {p : (C → Fin K) × (D → Fin K) // ConnectedAssignment p.1 ∧ ConnectedAssignment p.2 ∧ SamePair K M p.1 p.2} let E : A → Set Ω := fun a => {ω | (∀ i : C, X i ω = a.val.1 i) ∧ (∀ i : D, X i ω = a.val.2 i) ∧ 1 ≤ markCount C (fun i => B i ω) ∧ 1 ≤ markCount D (fun i => B i ω)} have himage (S : Finset (Fin n)) (ω : Ω) : Finset.univ.image (fun i : S => X i ω) = S.image (fun i => X i ω) := by ext x simp only [mem_image, Finset.mem_univ, true_and] constructor · rintro ⟨i, hi⟩ exact ⟨i, i.property, hi⟩ · rintro ⟨i, hi, hix⟩ exact ⟨⟨i, hi⟩, hix⟩ have hsub : {ω | PathConnected (C.image (fun i => X i ω)) ∧ PathConnected (D.image (fun i => X i ω)) ∧ 1 ≤ markCount C (fun i => B i ω) ∧ 1 ≤ markCount D (fun i => B i ω) ∧ SameCoarsePair M C D (fun i => X i ω)} ⊆ ⋃ a, E a := by rintro ω ⟨hc, hd, hmc, hmd, hp⟩ have hac : ConnectedAssignment (fun i : C => X i ω) := by simpa only [ConnectedAssignment, himage] using hc have had : ConnectedAssignment (fun i : D => X i ω) := by simpa only [ConnectedAssignment, himage] using hd obtain ⟨p, hpm, hpc, hpd⟩ := hp have hap : SamePair K M (fun i : C => X i ω) (fun i : D => X i ω) := ⟨p, hpm, (fun i => hpc i i.property), (fun i => hpd i i.property)⟩ exact Set.mem_iUnion.mpr ⟨⟨((fun i : C => X i ω), (fun i : D => X i ω)), hac, had, hap⟩, (fun _ => rfl), (fun _ => rfl), hmc, hmd⟩ have hbound (a : A) : μ.real (E a) ≤ ε ^ 2 * (C.card : ℝ) * (D.card : ℝ) / (K : ℝ) ^ (C.card + D.card) := assignment_pair_marks_probability_le h C D hdisj a.val.1 a.val.2 have hcard : (Fintype.card A : ℝ) ≤ 2 * (K : ℝ) ^ 2 * (C.card : ℝ) ^ C.card * (D.card : ℝ) ^ D.card / M := by have hc := connected_same_pair_assignment_count (ι := C) (κ := D) K M (by simpa only [Fintype.card_coe] using (show 1 ≤ C.card by omega)) (by simpa only [Fintype.card_coe] using (show 1 ≤ D.card by omega)) hM hK heven hdiv have hc' : M * Fintype.card A ≤ 2 * K ^ 2 * C.card ^ C.card * D.card ^ D.card := by simpa only [Nat.card_eq_fintype_card, Fintype.card_coe] using hc apply (le_div_iff₀ (Nat.cast_pos.mpr hM)).mpr have hc'' : (M : ℝ) * (Fintype.card A : ℝ) ≤ 2 * (K : ℝ) ^ 2 * (C.card : ℝ) ^ C.card * (D.card : ℝ) ^ D.card := by exact_mod_cast hc' simpa only [mul_comm] using hc'' have hnonneg : 0 ≤ ε ^ 2 * (C.card : ℝ) * (D.card : ℝ) / (K : ℝ) ^ (C.card + D.card) := by positivity calc _ ≤ μ.real (⋃ a, E a) := measureReal_mono hsub _ ≤ ∑ a : A, μ.real (E a) := measureReal_iUnion_fintype_le E _ ≤ ∑ _a : A, ε ^ 2 * (C.card : ℝ) * (D.card : ℝ) / (K : ℝ) ^ (C.card + D.card) := Finset.sum_le_sum (fun a _ => hbound a) _ = (Fintype.card A : ℝ) * (ε ^ 2 * (C.card : ℝ) * (D.card : ℝ) / (K : ℝ) ^ (C.card + D.card)) := by simp _ ≤ (2 * (K : ℝ) ^ 2 * (C.card : ℝ) ^ C.card * (D.card : ℝ) ^ D.card / M) * (ε ^ 2 * (C.card : ℝ) * (D.card : ℝ) / (K : ℝ) ^ (C.card + D.card)) := mul_le_mul_of_nonneg_right hcard hnonneg _ = _ := by simp only [pow_add, pow_one]; ring

theorem integrable_pairedScore {n K : ℕ} (μ : Measure Ω) [IsFiniteMeasure μ] (M : ℕ) (R : Ω → Fin n → Fin n → Prop) (X : Fin n → Ω → Fin K) (B : Fin n → Ω → Bool) (hR : ∀ i j, MeasurableSet {ω | R ω i j}) (hX : ∀ i, Measurable (X i)) (hB : ∀ i, Measurable (B i)) : Integrable (fun ω => pairedScore M (R ω) (fun i => X i ω) (fun i => B i ω)) μ := by classical let score : Finset (Finset (Fin n)) × ((Fin n → Fin K) × (Fin n → Bool)) → ℝ := fun p => (1 / 2 : ℝ) * ∑ C ∈ p.1, ∑ D ∈ p.1.erase C, pairWeight M C D p.2.1 p.2.2 have hinput : Measurable (fun ω => (components (R ω), (fun i => X i ω, fun i => B i ω))) := (measurable_components R hR).prodMk ((measurable_pi_lambda _ hX).prodMk (measurable_pi_lambda _ hB)) exact ((SimpleFunc.ofFinite score).comp _ hinput).integrable_of_isFiniteMeasure

theorem subset_connected_two_marks_le {n K : ℕ} {μ : Measure Ω} {X : Fin n → Ω → Fin K} {B : Fin n → Ω → Bool} {ε : ℝ} (h : UniformMarkedSample μ X B ε) (hK : 0 < K) (C : Finset (Fin n)) (hC : 2 ≤ C.card) : (μ {ω | PathConnected (C.image (fun i => X i ω)) ∧ 2 ≤ markCount C (fun i => B i ω)}).toReal ≤ ε ^ 2 * K * (C.card : ℝ) ^ (C.card + 2) / (K : ℝ) ^ C.card := by classical have : IsProbabilityMeasure μ := h.probability let A := {a : C → Fin K // ConnectedAssignment a} let E : A → Set Ω := fun a => {ω | (∀ i : C, X i ω = a.val i) ∧ 2 ≤ markCount C (fun i => B i ω)} have himage (ω : Ω) : Finset.univ.image (fun i : C => X i ω) = C.image (fun i => X i ω) := by ext x simp only [mem_image, Finset.mem_univ, true_and] constructor · rintro ⟨i, hi⟩ exact ⟨i, i.property, hi⟩ · rintro ⟨i, hi, hix⟩ exact ⟨⟨i, hi⟩, hix⟩ have hsub : {ω | PathConnected (C.image (fun i => X i ω)) ∧ 2 ≤ markCount C (fun i => B i ω)} ⊆ ⋃ a, E a := by rintro ω ⟨hc, hm⟩ have ha : ConnectedAssignment (fun i : C => X i ω) := by simpa only [ConnectedAssignment, himage] using hc exact Set.mem_iUnion.mpr ⟨⟨(fun i : C => X i ω), ha⟩, (fun _ => rfl), hm⟩ have hbound (a : A) : μ.real (E a) ≤ ε ^ 2 * (C.card : ℝ) ^ 2 / (K : ℝ) ^ C.card := assignment_two_marks_probability_le h C a.val have hcard : (Fintype.card A : ℝ) ≤ (K : ℝ) * (C.card : ℝ) ^ C.card := by have hc := connected_assignment_count (ι := C) K (by simpa only [Fintype.card_coe] using (show 1 ≤ C.card by omega)) have hc' : Fintype.card A ≤ K * C.card ^ C.card := by simpa only [Nat.card_eq_fintype_card, Fintype.card_coe] using hc exact_mod_cast hc' have hnonneg : 0 ≤ ε ^ 2 * (C.card : ℝ) ^ 2 / (K : ℝ) ^ C.card := div_nonneg (mul_nonneg (sq_nonneg ε) (sq_nonneg _)) (pow_nonneg (le_of_lt (Nat.cast_pos.mpr hK)) _) calc _ ≤ μ.real (⋃ a, E a) := measureReal_mono hsub _ ≤ ∑ a : A, μ.real (E a) := measureReal_iUnion_fintype_le E _ ≤ ∑ _a : A, ε ^ 2 * (C.card : ℝ) ^ 2 / (K : ℝ) ^ C.card := Finset.sum_le_sum (fun a _ => hbound a) _ = (Fintype.card A : ℝ) * (ε ^ 2 * (C.card : ℝ) ^ 2 / (K : ℝ) ^ C.card) := by simp _ ≤ ((K : ℝ) * (C.card : ℝ) ^ C.card) * (ε ^ 2 * (C.card : ℝ) ^ 2 / (K : ℝ) ^ C.card) := mul_le_mul_of_nonneg_right hcard hnonneg _ = _ := by rw [pow_add]; ring

theorem single_expectation_labelled_le {n K : ℕ} {μ : Measure Ω} {X : Fin n → Ω → Fin K} {B : Fin n → Ω → Bool} {ε : ℝ} (h : UniformMarkedSample μ X B ε) (M : ℕ) (hK : 0 < K) (R : Ω → Fin n → Fin n → Prop) (hR : ∀ i j, MeasurableSet {ω | R ω i j}) (hlocal : ∀ ω, Admissible M (fun i => X i ω) (R ω)) : (∫ ω, singleScore (R ω) (fun i => B i ω) ∂μ) ≤ ε ^ 2 * K * ∑ m ∈ Icc 2 n, (n.choose m : ℝ) * (m : ℝ) ^ 10 * 8 ^ m * (m : ℝ) ^ m / (K : ℝ) ^ m := by classical let : IsProbabilityMeasure μ := h.probability let E : Finset (Fin n) → Set Ω := fun C => {ω | PathConnected (C.image (fun i => X i ω)) ∧ 2 ≤ markCount C (fun i => B i ω)} let w : ℕ → ℝ := fun m => (m : ℝ) ^ 8 * 8 ^ m let f : Finset (Fin n) → Ω → ℝ := fun C => (E C).indicator (fun _ => w C.card) let g : ℕ → ℝ := fun m => if 2 ≤ m then ε ^ 2 * K * (m : ℝ) ^ 10 * 8 ^ m * (m : ℝ) ^ m / (K : ℝ) ^ m else 0 have hinput : Measurable (fun ω => (fun i => X i ω, fun i => B i ω)) := (measurable_pi_lambda _ h.cells_measurable).prodMk (measurable_pi_lambda _ h.marks_measurable) have hE (C : Finset (Fin n)) : MeasurableSet (E C) := by exact hinput (Set.toFinite {p : (Fin n → Fin K) × (Fin n → Bool) | PathConnected (C.image p.1) ∧ 2 ≤ markCount C p.2}).measurableSet have hf (C : Finset (Fin n)) : Integrable (f C) μ := (integrable_const (w C.card)).indicator (hE C) have hpoint (ω : Ω) : singleScore (R ω) (fun i => B i ω) ≤ ∑ C ∈ Finset.univ.powerset, f C ω := by convert singleScore_le_subsets M (fun i => X i ω) (R ω) (fun i => B i ω) (hlocal ω) using 1 apply Finset.sum_congr rfl intro C _ simp only [f, E, indicator, Set.mem_ofPred_eq, singleWeight, w] split_ifs <;> simp_all have hbound (C : Finset (Fin n)) : (∫ ω, f C ω ∂μ) ≤ g C.card := by by_cases hC : 2 ≤ C.card · rw [show (∫ ω, f C ω ∂μ) = μ.real (E C) * w C.card by exact (integral_indicator_const _ (hE C)).trans (by simp [smul_eq_mul])] have hp := mul_le_mul_of_nonneg_right (subset_connected_two_marks_le h hK C hC) (show 0 ≤ w C.card by dsimp [w]; positivity) calc _ ≤ (ε ^ 2 * K * (C.card : ℝ) ^ (C.card + 2) / (K : ℝ) ^ C.card) * w C.card := hp _ = g C.card := by simp only [g, if_pos hC, w, pow_add] ring · have hempty : E C = ∅ := by apply Set.eq_empty_iff_forall_notMem.mpr intro ω hω have hc : markCount C (fun i => B i ω) ≤ C.card := Finset.card_filter_le _ _ exact hC (le_trans hω.2 hc) simp [f, hempty, g, hC] calc _ ≤ ∫ ω, ∑ C ∈ Finset.univ.powerset, f C ω ∂μ := integral_mono (integrable_singleScore μ R B hR h.marks_measurable) (integrable_finsetSum _ (fun C _ => hf C)) hpoint _ = ∑ C ∈ Finset.univ.powerset, ∫ ω, f C ω ∂μ := integral_finsetSum _ (fun C _ => hf C) _ ≤ ∑ C ∈ Finset.univ.powerset, g C.card := Finset.sum_le_sum (fun C _ => hbound C) _ = ∑ m ∈ range (n + 1), (n.choose m : ℝ) * g m := by rw [Finset.sum_powerset_apply_card] simp only [Finset.card_univ, Fintype.card_fin, nsmul_eq_mul] _ = ∑ m ∈ Icc 2 n, (n.choose m : ℝ) * g m := by symm apply Finset.sum_subset · intro m hm simp only [Finset.mem_Icc] at hm simp only [Finset.mem_range] omega · intro m _ hm have hsmall : ¬ 2 ≤ m := by simp only [Finset.mem_Icc, not_and_or, not_le] at hm simp only [Finset.mem_range] at * omega simp [g, hsmall] _ = _ := by rw [Finset.mul_sum] apply Finset.sum_congr rfl intro m hm simp only [g, if_pos (Finset.mem_Icc.mp hm).1] ring