Mixtures of valid finite samples

Each component has total mass at most one. Removing a small exceptional set from every sample space retains positive mass and preserves thickness provided one component witnesses escape from each central slab.

noncomputable def EGZ.Expansion.sampleWeight {I : Type u_1} {β : Type u_2} [Fintype I] (A : I → Type u_3) [(i : I) → Fintype (A i)] (value : (i : I) → A i → β) (valid : (i : I) → A i → Prop) (v : β) : ℝ

Equal mixture of the valid samples, retaining their vector values.

Equations

• EGZ.Expansion.sampleWeight A value valid v = ∑ i : I, EGZ.Expansion.finiteProb fun (x : A i) => valid i x ∧ value i x = v

theorem EGZ.Expansion.sampleWeight_nonneg {I : Type u_1} {β : Type u_2} [Fintype I] (A : I → Type u_3) [(i : I) → Fintype (A i)] (value : (i : I) → A i → β) (valid : (i : I) → A i → Prop) (v : β) : 0 ≤ sampleWeight A value valid v

theorem EGZ.Expansion.finiteProb_sum_fibres {β : Type u_2} [Fintype β] {α : Type u_4} [Fintype α] (f : α → β) (Q : α → Prop) (P : β → Prop) : (∑ v : β, if P v then finiteProb fun (x : α) => Q x ∧ f x = v else 0) = finiteProb fun (x : α) => Q x ∧ P (f x)

theorem EGZ.Expansion.sampleWeight_massOn {I : Type u_1} {β : Type u_2} [Fintype I] [Fintype β] (A : I → Type u_3) [(i : I) → Fintype (A i)] (value : (i : I) → A i → β) (valid : (i : I) → A i → Prop) (P : β → Prop) : (∑ v : β, if P v then sampleWeight A value valid v else 0) = ∑ i : I, finiteProb fun (x : A i) => valid i x ∧ P (value i x)

Mass on a set of vectors is the sum of the corresponding valid-sample probabilities over all components.

theorem EGZ.Expansion.sampleWeight_mass {I : Type u_1} {β : Type u_2} [Fintype I] [Fintype β] (A : I → Type u_3) [(i : I) → Fintype (A i)] (value : (i : I) → A i → β) (valid : (i : I) → A i → Prop) : ∑ v : β, sampleWeight A value valid v = ∑ i : I, finiteProb (valid i)

theorem EGZ.Expansion.sampleWeight_mass_le {I : Type u_1} {β : Type u_2} [Fintype I] [Fintype β] (A : I → Type u_3) [(i : I) → Fintype (A i)] (value : (i : I) → A i → β) (valid : (i : I) → A i → Prop) [∀ (i : I), Nonempty (A i)] : ∑ v : β, sampleWeight A value valid v ≤ ↑(Fintype.card I)

theorem EGZ.Expansion.sampleWeight_mass_ge {I : Type u_1} {β : Type u_2} [Fintype I] [Fintype β] (A : I → Type u_3) [(i : I) → Fintype (A i)] (value : (i : I) → A i → β) (valid : (i : I) → A i → Prop) [∀ (i : I), Nonempty (A i)] {e : ℝ} (hbad : ∀ (i : I), (finiteProb fun (x : A i) => ¬valid i x) ≤ e) : ↑(Fintype.card I) * (1 - e) ≤ ∑ v : β, sampleWeight A value valid v

theorem EGZ.Expansion.sampleWeight_pos_exists {I : Type u_1} {β : Type u_2} [Fintype I] (A : I → Type u_3) [(i : I) → Fintype (A i)] (value : (i : I) → A i → β) (valid : (i : I) → A i → Prop) {v : β} (hv : 0 < sampleWeight A value valid v) : ∃ (i : I) (x : A i), valid i x ∧ value i x = v

theorem EGZ.Expansion.finiteProb_and_ge_sub {A : Type u_1} [Fintype A] (P Q : A → Prop) : (finiteProb Q - finiteProb fun (x : A) => ¬P x) ≤ finiteProb fun (x : A) => P x ∧ Q x

Removing an exceptional set loses at most its probability from any event, without any independence assumption.

theorem EGZ.Expansion.sampleWeight_mass_pos {p d : ℕ} [NeZero p] {I : Type u_1} [Fintype I] [Nonempty I] (A : I → Type u_2) [(i : I) → Fintype (A i)] [∀ (i : I), Nonempty (A i)] (value : (i : I) → A i → FpCoord p d) (valid : (i : I) → A i → Prop) {η : ℝ} (hηone : η ≤ 1) (hbad : ∀ (i : I), (finiteProb fun (x : A i) => ¬valid i x) ≤ η / 2) : 0 < ∑ v : FpCoord p d, sampleWeight A value valid v

theorem EGZ.Expansion.sampleWeight_centrallyThick {p d W : ℕ} [NeZero p] {I : Type u_1} [Fintype I] [Nonempty I] (A : I → Type u_2) [(i : I) → Fintype (A i)] [∀ (i : I), Nonempty (A i)] (value : (i : I) → A i → FpCoord p d) (valid : (i : I) → A i → Prop) {η : ℝ} (hη : 0 < η) (hbad : ∀ (i : I), (finiteProb fun (x : A i) => ¬valid i x) ≤ η / 2) (hout : ∀ (ξ : FpCoord p d →ₗ[ZMod p] ZMod p), ξ ≠ 0 → ∃ (i : I), η ≤ finiteProb fun (x : A i) => ¬HasBoundedRepresentative p W (ξ (value i x))) : IsCentrallyThick (sampleWeight A value valid) W (η / (2 * ↑(Fintype.card I)))