Dependent Random Choice

noncomputable def s {G : Type u_1} [DecidableEq G] [Fintype G] [AddCommGroup G] [MeasurableSpace G] (p : NNReal) (ε : ℝ) (B₁ B₂ A : Finset G) : Finset G

Equations

• s p ε B₁ B₂ A = {x : G | (1 - ε) * ‖𝟭 A ○ 𝟭 A‖_[↑p, mu B₁ ○ mu B₂] < (𝟭 A ○ 𝟭 A) x}

@[simp]

theorem mem_s {G : Type u_1} [DecidableEq G] [Fintype G] [AddCommGroup G] [MeasurableSpace G] {p : NNReal} {ε : ℝ} {B₁ B₂ A : Finset G} {x : G} : x ∈ s p ε B₁ B₂ A ↔ (1 - ε) * ‖𝟭 A ○ 𝟭 A‖_[↑p, mu B₁ ○ mu B₂] < (𝟭 A ○ 𝟭 A) x

theorem mem_s' {G : Type u_1} [DecidableEq G] [Fintype G] [AddCommGroup G] [MeasurableSpace G] {p : NNReal} {ε : ℝ} {B₁ B₂ A : Finset G} {x : G} : x ∈ s p ε B₁ B₂ A ↔ (1 - ε) * ‖mu A ○ mu A‖_[↑p, mu B₁ ○ mu B₂] < (mu A ○ mu A) x

theorem drc {G : Type u_1} [DecidableEq G] [Fintype G] [AddCommGroup G] {p : ℕ} {B₁ B₂ A : Finset G} [MeasurableSpace G] [DiscreteMeasurableSpace G] (hp₂ : 2 ≤ p) (f : G → NNReal) (hf : ∃ x ∈ B₁ - B₂, x ∈ A - A ∧ x ∈ Function.support f) (hB : (B₁ ∩ B₂).Nonempty) (hA : A.Nonempty) : ∃ A₁ ⊆ B₁, ∃ A₂ ⊆ B₂, RCLike.wInner 1 (mu A₁ ○ mu A₂) (NNReal.toReal ∘ f) * ‖𝟭 A ○ 𝟭 A‖_[↑p, mu B₁ ○ mu B₂] ^ p ≤ 2 * ∑ x : G, (mu B₁ ○ mu B₂) x * (𝟭 A ○ 𝟭 A) x ^ p * ↑(f x) ∧ 4⁻¹ * ‖𝟭 A ○ 𝟭 A‖_[↑p, mu B₁ ○ mu B₂] ^ (2 * p) / ↑A.card ^ (2 * p) ≤ ↑A₁.card / ↑B₁.card ∧ 4⁻¹ * ‖𝟭 A ○ 𝟭 A‖_[↑p, mu B₁ ○ mu B₂] ^ (2 * p) / ↑A.card ^ (2 * p) ≤ ↑A₂.card / ↑B₂.card

theorem sifting {G : Type u_1} [DecidableEq G] [Fintype G] [AddCommGroup G] {p : ℕ} {A : Finset G} {ε δ : ℝ} [MeasurableSpace G] [DiscreteMeasurableSpace G] (B₁ B₂ : Finset G) (hε : 0 < ε) (hε₁ : ε ≤ 1) (hδ : 0 < δ) (hp : Even p) (hp₂ : 2 ≤ p) (hpε : ε⁻¹ * Real.log (2 / δ) ≤ ↑p) (hB : (B₁ ∩ B₂).Nonempty) (hA : A.Nonempty) (hf : ∃ x ∈ B₁ - B₂, x ∈ A - A ∧ x ∉ s (↑p) ε B₁ B₂ A) : ∃ A₁ ⊆ B₁, ∃ A₂ ⊆ B₂, 1 - δ ≤ ∑ x ∈ s (↑p) ε B₁ B₂ A, (mu A₁ ○ mu A₂) x ∧ 4⁻¹ * ‖𝟭 A ○ 𝟭 A‖_[↑p, mu B₁ ○ mu B₂] ^ (2 * p) / ↑A.card ^ (2 * p) ≤ ↑A₁.card / ↑B₁.card ∧ 4⁻¹ * ‖𝟭 A ○ 𝟭 A‖_[↑p, mu B₁ ○ mu B₂] ^ (2 * p) / ↑A.card ^ (2 * p) ≤ ↑A₂.card / ↑B₂.card

theorem sifting_cor {G : Type u_1} [DecidableEq G] [Fintype G] [AddCommGroup G] {p : ℕ} {A : Finset G} {ε δ : ℝ} [MeasurableSpace G] [DiscreteMeasurableSpace G] (hε : 0 < ε) (hε₁ : ε ≤ 1) (hδ : 0 < δ) (hp : Even p) (hp₂ : 2 ≤ p) (hpε : ε⁻¹ * Real.log (2 / δ) ≤ ↑p) (hA : A.Nonempty) : ∃ (A₁ : Finset G) (A₂ : Finset G), 1 - δ ≤ ∑ x ∈ s (↑p) ε Finset.univ Finset.univ A, (mu A₁ ○ mu A₂) x ∧ 4⁻¹ * ↑A.dens ^ (2 * p) ≤ ↑A₁.dens ∧ 4⁻¹ * ↑A.dens ^ (2 * p) ≤ ↑A₂.dens

Special case of sifting when B₁ = B₂ = univ.