Finding a good sample

Two estimates for finding, by uniform sampling, a point of a finite type at which a function is large.

Reverse averaging. If f ≤ 1 has average μ, then f ≤ θ + (1 - θ) 𝟙[θ ≤ f] pointwise, so μ ≤ θ + (1 - θ) dens {θ ≤ f} (Fintype.expect_le_add_mul_dens_filter): f is at least θ on a set of density at least (μ - θ) / (1 - θ) when θ < 1 (Fintype.expect_sub_div_le_dens_filter), and at least μ - θ when 0 ≤ θ (Fintype.expect_sub_le_dens_filter). This is the reverse of Markov's inequality Fintype.mul_dens_filter_le_expect, for functions bounded above instead of below.

Repeated trials. k independent uniform samples all miss a set of density p with probability (1 - p) ^ k (Fintype.dens_filter_forall_apply_notMem), so some sample lands in it with probability 1 - (1 - p) ^ k (Fintype.dens_filter_exists_apply_mem). This is at least 1 / 2 once k p ≥ 1 (Fintype.half_le_dens_filter_exists_apply_mem): by Bernoulli's inequality (1 + p) ^ k ≥ 1 + k p ≥ 2, while (1 - p) ^ k (1 + p) ^ k = (1 - p ^ 2) ^ k ≤ 1 (one_sub_pow_le_half).

Main results

• Fintype.expect_le_add_mul_dens_filter, Fintype.expect_sub_div_le_dens_filter, Fintype.expect_sub_le_dens_filter: reverse averaging.
• Fintype.dens_filter_forall_apply_notMem, Fintype.dens_filter_exists_apply_mem, Fintype.cast_dens_filter_exists_apply_mem: the exact law of repeated trials.
• Fintype.one_sub_pow_le_dens_filter_exists_apply_mem, Fintype.half_le_dens_filter_exists_apply_mem: lower bounds for repeated trials.
• one_sub_pow_le_half: k trials of success probability p ≥ 1 / k all fail with probability at most 1 / 2.

theorem one_sub_pow_le_half {𝕜 : Type u_1} [Field 𝕜] [LinearOrder 𝕜] [IsStrictOrderedRing 𝕜] {p : 𝕜} (hp₀ : 0 ≤ p) (hp₁ : p ≤ 1) {k : ℕ} (hk : 1 ≤ ↑k * p) : (1 - p) ^ k ≤ 1 / 2

If 0 ≤ p ≤ 1 and k p ≥ 1, then (1 - p) ^ k ≤ 1 / 2: k independent trials, each succeeding with probability p, all fail with probability at most 1 / 2.

Reverse averaging

theorem Fintype.expect_le_add_mul_dens_filter {α : Type u_2} {𝕜 : Type u_3} [Fintype α] [Field 𝕜] [LinearOrder 𝕜] [IsStrictOrderedRing 𝕜] [Nonempty α] {f : α → 𝕜} (hf : ∀ (a : α), f a ≤ 1) (θ : 𝕜) [DecidablePred fun (a : α) => θ ≤ f a] : (Finset.univ.expect fun (a : α) => f a) ≤ θ + (1 - θ) * ↑{a : α | θ ≤ f a}.dens

Reverse averaging. A function bounded above by 1 averages to at most θ plus 1 - θ times the density of the set where it is at least θ.

theorem Fintype.expect_sub_div_le_dens_filter {α : Type u_2} {𝕜 : Type u_3} [Fintype α] [Field 𝕜] [LinearOrder 𝕜] [IsStrictOrderedRing 𝕜] [Nonempty α] {f : α → 𝕜} (hf : ∀ (a : α), f a ≤ 1) {θ : 𝕜} [DecidablePred fun (a : α) => θ ≤ f a] (hθ : θ < 1) : ((Finset.univ.expect fun (a : α) => f a) - θ) / (1 - θ) ≤ ↑{a : α | θ ≤ f a}.dens

Reverse averaging. If θ < 1, a function bounded above by 1 with average μ is at least θ on a set of density at least (μ - θ) / (1 - θ).

theorem Fintype.expect_sub_le_dens_filter {α : Type u_2} {𝕜 : Type u_3} [Fintype α] [Field 𝕜] [LinearOrder 𝕜] [IsStrictOrderedRing 𝕜] [Nonempty α] {f : α → 𝕜} (hf : ∀ (a : α), f a ≤ 1) {θ : 𝕜} [DecidablePred fun (a : α) => θ ≤ f a] (hθ : 0 ≤ θ) : (Finset.univ.expect fun (a : α) => f a) - θ ≤ ↑{a : α | θ ≤ f a}.dens

Reverse averaging. If 0 ≤ θ, a function bounded above by 1 with average μ is at least θ on a set of density at least μ - θ.

Repeated trials

theorem Fintype.dens_filter_forall_apply_notMem {ι : Type u_1} {α : Type u_2} [Fintype ι] [Fintype α] [DecidableEq ι] (s : Finset α) [DecidableEq α] [DecidablePred fun (ω : ι → α) => ∀ (j : ι), ω j ∉ s] : {ω : ι → α | ∀ (j : ι), ω j ∉ s}.dens = sᶜ.dens ^ card ι

Repeated trials. card ι independent uniform samples all miss s with probability dens sᶜ ^ card ι.

theorem Fintype.dens_filter_exists_apply_mem {ι : Type u_1} {α : Type u_2} [Fintype ι] [Fintype α] [DecidableEq ι] (s : Finset α) [Nonempty α] [DecidablePred fun (ω : ι → α) => ∃ (j : ι), ω j ∈ s] : {ω : ι → α | ∃ (j : ι), ω j ∈ s}.dens = 1 - (1 - s.dens) ^ card ι

Repeated trials. Some of card ι independent uniform samples lands in s with probability 1 - (1 - dens s) ^ card ι.

theorem Fintype.cast_dens_filter_exists_apply_mem {ι : Type u_1} {α : Type u_2} {𝕜 : Type u_3} [Fintype ι] [Fintype α] [DecidableEq ι] (s : Finset α) [Nonempty α] [DecidablePred fun (ω : ι → α) => ∃ (j : ι), ω j ∈ s] [Field 𝕜] [CharZero 𝕜] : ↑{ω : ι → α | ∃ (j : ι), ω j ∈ s}.dens = 1 - (1 - ↑s.dens) ^ card ι

Repeated trials, in a field: some of card ι independent uniform samples lands in s with probability 1 - (1 - dens s) ^ card ι.

theorem Fintype.one_sub_pow_le_dens_filter_exists_apply_mem {ι : Type u_1} {α : Type u_2} {𝕜 : Type u_3} [Fintype ι] [Fintype α] [DecidableEq ι] {s : Finset α} [Nonempty α] [DecidablePred fun (ω : ι → α) => ∃ (j : ι), ω j ∈ s] [Field 𝕜] [LinearOrder 𝕜] [IsStrictOrderedRing 𝕜] {q : 𝕜} (hq : q ≤ ↑s.dens) : 1 - (1 - q) ^ card ι ≤ ↑{ω : ι → α | ∃ (j : ι), ω j ∈ s}.dens

Repeated trials. If a uniform sample lands in s with probability at least q, some of card ι independent uniform samples lands in s with probability at least 1 - (1 - q) ^ card ι.

theorem Fintype.half_le_dens_filter_exists_apply_mem {ι : Type u_1} {α : Type u_2} {𝕜 : Type u_3} [Fintype ι] [Fintype α] [DecidableEq ι] {s : Finset α} [Nonempty α] [DecidablePred fun (ω : ι → α) => ∃ (j : ι), ω j ∈ s] [Field 𝕜] [LinearOrder 𝕜] [IsStrictOrderedRing 𝕜] {q : 𝕜} (hq₀ : 0 ≤ q) (hq : q ≤ ↑s.dens) (hι : 1 ≤ ↑(card ι) * q) : 1 / 2 ≤ ↑{ω : ι → α | ∃ (j : ι), ω j ∈ s}.dens

Repeated trials. If a uniform sample lands in s with probability at least q ≥ 0 and card ι * q ≥ 1, some of card ι independent uniform samples lands in s with probability at least 1 / 2.