Maintaining the density rectangle through one message #
A weighted pigeonhole argument bounds the entropy loss of a message cell.
Use the improved mirror set when the existing limit condition faces the wrong
speaker. A density limit at rate below 3/4 precludes a fixed separating coordinate.
theorem
Complexity.BooleanAnalysis.exists_large_message_fiber_internal
{ι : Type u_1}
[Fintype ι]
{M : Type u_2}
[Fintype M]
[DecidableEq M]
(X : Finset (ι → Bool))
(hX : X.Nonempty)
(send : (ι → Bool) → M)
{m : ℝ}
(hm : ↑(Fintype.card M) ≤ 2 ^ m)
:
∃ (a : M), {x ∈ X | send x = a}.Nonempty ∧ uniformDeficit ({x ∈ X | send x = a}) ≤ uniformDeficit X + m
theorem
Complexity.BooleanAnalysis.IsDensityLimit.agrees_internal
{ι : Type u_1}
[Fintype ι]
[DecidableEq ι]
{Y : Finset (ι → Bool)}
{p k : ℝ}
{x : ι → Bool}
(hlim : IsDensityLimit Y p k x)
(hp : 0 ≤ p)
(hp' : p < 3 / 4)
(i : ι)
:
∃ y ∈ Y, y i = x i
theorem
Complexity.BooleanAnalysis.IsDensityLimit.mono_deficit_internal
{ι : Type u_1}
[Fintype ι]
[DecidableEq ι]
{Y : Finset (ι → Bool)}
{p k k' : ℝ}
{x : ι → Bool}
(hlim : IsDensityLimit Y p k x)
(hp : 0 ≤ p)
(hp' : p ≤ 1)
(hkk' : k ≤ k')
:
IsDensityLimit Y p k' x
theorem
Complexity.KarchmerWigderson.DensityRectangle.swap_internal
{ι : Type u_1}
[Fintype ι]
[DecidableEq ι]
{X Y : Finset (ι → Bool)}
{p k : ℝ}
(h : DensityRectangle X Y p k)
:
DensityRectangle Y X p k
theorem
Complexity.KarchmerWigderson.DensityRectangle.not_separated_internal
{ι : Type u_1}
[Fintype ι]
[DecidableEq ι]
{X Y : Finset (ι → Bool)}
{p k : ℝ}
(h : DensityRectangle X Y p k)
(hp : p < 3 / 4)
(i : ι)
:
theorem
Complexity.KarchmerWigderson.DensityRectangle.select_left_message_internal
{ι : Type u_1}
[Fintype ι]
[DecidableEq ι]
{M : Type u_2}
[Fintype M]
[DecidableEq M]
{X Y : Finset (ι → Bool)}
{p p' k k' m : ℝ}
(h : DensityRectangle X Y p k)
(send : (ι → Bool) → M)
(hM : ↑(Fintype.card M) ≤ 2 ^ m)
(hk : 1 ≤ k)
(hkk : 194 * k ≤ k')
(hcost : 2 * k + 2 + m ≤ k')
(hscale : 32768 * k * p ≤ p')
(hp' : p' ≤ 1 / 4)
:
∃ (a : M), ∃ X' ⊆ X, (∀ x ∈ X', send x = a) ∧ DensityRectangle X' Y p' k'