Guided distributions and the improved mirror set #
On a sufficiently dense fiber, sample uniformly from its intersection with Y;
on the remaining fibers, sample uniformly from the whole fiber. The density of
this sampling rule is at most 2^k. This is a distributional variant of the
fixed-size guiding sets in Oliver Korten's proof, avoiding a rounding operation.
The completion estimate bounds the guided failure probability by 1/16.
Intersecting Y with the (q,194*k)-limits of X gives a nonempty mirror set
of deficit at most 2*k+2, with q = 32768*k*p.
Source: Oliver Korten, Top-Down Lower Bounds for All Depths, ECCC TR26-221 (2026), https://eccc.weizmann.ac.il/report/2026/221/, Sections 3--4.
noncomputable def
Complexity.BooleanAnalysis.guidingDensity
{ι : Type u_1}
[Fintype ι]
[DecidableEq ι]
(Y : Finset (ι → Bool))
(k : ℝ)
(P x y : ι → Bool)
:
Density of the guiding rule relative to uniform coordinate modifications.
Dense fibers are restricted to Y; the other fibers are left uniform.
Equations
- One or more equations did not get rendered due to their size.
Instances For
noncomputable def
Complexity.BooleanAnalysis.guidedAverage
{ι : Type u_1}
[Fintype ι]
[DecidableEq ι]
(X Y : Finset (ι → Bool))
(p k : ℝ)
(f : (ι → Bool) → ℝ)
:
Expectation of a test function after a guided modification of a uniform
point of X, using a rate-p coordinate mask and deficit parameter k.
Equations
- One or more equations did not get rendered due to their size.
Instances For
theorem
Complexity.BooleanAnalysis.guidingDensity_nonneg_internal
{ι : Type u_1}
[Fintype ι]
[DecidableEq ι]
(Y : Finset (ι → Bool))
(k : ℝ)
(P x y : ι → Bool)
:
theorem
Complexity.BooleanAnalysis.expect_guidingDensity_internal
{ι : Type u_1}
[Fintype ι]
[DecidableEq ι]
(Y : Finset (ι → Bool))
(k : ℝ)
(P x : ι → Bool)
:
theorem
Complexity.BooleanAnalysis.guidingDensity_le_internal
{ι : Type u_1}
[Fintype ι]
[DecidableEq ι]
(Y : Finset (ι → Bool))
{k : ℝ}
(hk : 0 ≤ k)
(P x y : ι → Bool)
:
theorem
Complexity.BooleanAnalysis.guidedAverage_const_internal
{ι : Type u_1}
[Fintype ι]
[DecidableEq ι]
(X Y : Finset (ι → Bool))
(hX : X.Nonempty)
(p k c : ℝ)
:
theorem
Complexity.BooleanAnalysis.expect_resample_internal
{ι : Type u_1}
[Fintype ι]
[DecidableEq ι]
(f : (ι → Bool) → ℝ)
(P : ι → Bool)
:
(Finset.univ.expect fun (x : ι → Bool) => Finset.univ.expect fun (y : ι → Bool) => f (resample P x y)) = Finset.univ.expect fun (z : ι → Bool) => f z
theorem
Complexity.BooleanAnalysis.sum_expect_resample_internal
{ι : Type u_1}
[Fintype ι]
[DecidableEq ι]
(f : (ι → Bool) → ℝ)
(P : ι → Bool)
:
theorem
Complexity.BooleanAnalysis.guidingDensity_hits_internal
{ι : Type u_1}
[Fintype ι]
[DecidableEq ι]
(Y : Finset (ι → Bool))
(k : ℝ)
(P x : ι → Bool)
:
theorem
Complexity.BooleanAnalysis.guidedAverage_hits_internal
{ι : Type u_1}
[Fintype ι]
[DecidableEq ι]
(X Y : Finset (ι → Bool))
(hX : X.Nonempty)
{p k : ℝ}
(hp : 0 ≤ p)
(hp' : p ≤ 1)
(hlim : ∀ x ∈ X, IsDensityLimit Y p k x)
:
theorem
Complexity.BooleanAnalysis.guidedAverage_linear_internal
{ι : Type u_1}
[Fintype ι]
[DecidableEq ι]
(X Y : Finset (ι → Bool))
(p k a b : ℝ)
(f g : (ι → Bool) → ℝ)
:
(guidedAverage X Y p k fun (z : ι → Bool) => a * f z + b * g z) = a * guidedAverage X Y p k f + b * guidedAverage X Y p k g
theorem
Complexity.BooleanAnalysis.guidedAverage_bernoulli_internal
{ι : Type u_1}
[Fintype ι]
[DecidableEq ι]
(X Y : Finset (ι → Bool))
(p q k : ℝ)
(f : (ι → Bool) → (ι → Bool) → ℝ)
:
(guidedAverage X Y p k fun (z : ι → Bool) => bernoulliAverage q fun (Q : ι → Bool) => f Q z) = bernoulliAverage p fun (P : ι → Bool) =>
bernoulliAverage q fun (Q : ι → Bool) =>
X.expect fun (x : ι → Bool) =>
Finset.univ.expect fun (y : ι → Bool) => guidingDensity Y k P x y * f Q (resample P x y)
theorem
Complexity.BooleanAnalysis.guidedAverage_bad_completion_internal
{ι : Type u_1}
[Fintype ι]
[DecidableEq ι]
(X Y : Finset (ι → Bool))
(hX : X.Nonempty)
{k p q : ℝ}
(hk : 1 ≤ k)
(hdef : uniformDeficit X ≤ k)
(hp : 0 < p)
(hq : q = 32768 * k * p)
(hq' : q ≤ 1 / 2)
:
(guidedAverage X Y p k fun (z : ι → Bool) =>
bernoulliAverage q fun (Q : ι → Bool) => if coordinateDensity X Q z < 2 ^ (-194 * k) then 1 else 0) ≤ 1 / 16
theorem
Complexity.BooleanAnalysis.densityLimit_complement_internal
{ι : Type u_1}
[Fintype ι]
[DecidableEq ι]
(X : Finset (ι → Bool))
(q t : ℝ)
(z : ι → Bool)
:
(bernoulliAverage q fun (Q : ι → Bool) => if coordinateDensity X Q z < 2 ^ (-t) then 1 else 0) = 1 - bernoulliAverage q fun (Q : ι → Bool) => if 2 ^ (-t) ≤ coordinateDensity X Q z then 1 else 0
theorem
Complexity.BooleanAnalysis.guidedAverage_mirror_mass_internal
{ι : Type u_1}
[Fintype ι]
[DecidableEq ι]
(X Y : Finset (ι → Bool))
(hX : X.Nonempty)
{k p q : ℝ}
(hk : 1 ≤ k)
(hdef : uniformDeficit X ≤ k)
(hp : 0 < p)
(hq : q = 32768 * k * p)
(hq' : q ≤ 1 / 2)
(hlim : ∀ x ∈ X, IsDensityLimit Y p k x)
:
1 / 4 ≤ guidedAverage X Y p k fun (z : ι → Bool) => if z ∈ Y ∧ IsDensityLimit X q (194 * k) z then 1 else 0
theorem
Complexity.BooleanAnalysis.improved_mirror_set_internal
{ι : Type u_1}
[Fintype ι]
[DecidableEq ι]
(X Y : Finset (ι → Bool))
(hX : X.Nonempty)
{k p q : ℝ}
(hk : 1 ≤ k)
(hdef : uniformDeficit X ≤ k)
(hp : 0 < p)
(hq : q = 32768 * k * p)
(hq' : q ≤ 1 / 2)
(hlim : ∀ x ∈ X, IsDensityLimit Y p k x)
:
∃ Y' ⊆ Y, Y'.Nonempty ∧ uniformDeficit Y' ≤ 2 * k + 2 ∧ ∀ y ∈ Y', IsDensityLimit X q (194 * k) y