Documentation

Complexitylib.Algebraic.LowerBound.AC0.ParityParameters

Concrete switching parameters for parity depth reduction #

This module records a simple source-faithful choice of parameters. For target tree depth t >= 1, use

In every round the switching base 5 * p_i * t_i is exactly 1/2, while the retained ratio is half of p_i. Hence every charged failure bound is

S * (1/2)^(t+1),

and the single sufficient smallness condition is that this be below the minimum ratio 1/(20t). Constants are intentionally conservative so exact first-moment slack remains visible; optimizing them is not mathematically important for the lower-bound exponent.

source
def Algebraic.AC0.ParityParameters.treeBound (t : ℕ) :
ℕ → ℕ

Width one before any switching step, then the common target depth t.

Equations
Instances For
    source
    noncomputable def Algebraic.AC0.ParityParameters.probability (t : ℕ) :
    ℕ → NNReal

    Constant first-round restriction probability, followed by probability inversely proportional to the common tree depth.

    Equations
    Instances For
      source
      noncomputable def Algebraic.AC0.ParityParameters.retentionRatio (t : ℕ) :
      ℕ → NNReal

      Keep half of the expected live fraction available as failure slack.

      Equations
      Instances For
        source
        noncomputable def Algebraic.AC0.ParityParameters.minimumRatio (t : ℕ) :
        NNReal

        The smallest retained ratio occurring in the schedule.

        Equations
        Instances For
          source
          @[simp]
          theorem Algebraic.AC0.ParityParameters.treeBound_zero (t : ℕ) :
          treeBound t 0 = 1
          source
          @[simp]
          theorem Algebraic.AC0.ParityParameters.treeBound_succ (t level : ℕ) :
          treeBound t (level + 1) = t
          source
          theorem Algebraic.AC0.ParityParameters.probability_le_one (t : ℕ) (oneLe : 1 ≤ t) (level : ℕ) :
          probability t level ≤ 1

          Every scheduled restriction parameter is a probability.

          source
          theorem Algebraic.AC0.ParityParameters.treeBound_mono (t : ℕ) (oneLe : 1 ≤ t) (level : ℕ) :
          treeBound t level ≤ treeBound t (level + 1)

          The scheduled tree allowance is monotone.

          source
          theorem Algebraic.AC0.ParityParameters.five_mul_probability_mul_treeBound_nnreal (t : ℕ) (oneLe : 1 ≤ t) (level : ℕ) :
          5 * probability t level * ↑(treeBound t level) = 1 / 2

          Exact switching base, first proved in the finite nonnegative reals.

          source
          theorem Algebraic.AC0.ParityParameters.five_mul_probability_mul_treeBound (t : ℕ) (oneLe : 1 ≤ t) (level : ℕ) :
          5 * ↑(probability t level) * ↑(treeBound t level) = 1 / 2

          Exact switching base in the extended nonnegative reals used by finite probabilities.

          source
          theorem Algebraic.AC0.ParityParameters.retention_twice_eq_probability_nnreal (t : ℕ) (oneLe : 1 ≤ t) (level : ℕ) :
          retentionRatio t level + retentionRatio t level = probability t level

          The retention ratio is exactly half the restriction probability.

          source
          theorem Algebraic.AC0.ParityParameters.retention_twice_eq_probability (t : ℕ) (oneLe : 1 ≤ t) (level : ℕ) :
          ↑(retentionRatio t level) + ↑(retentionRatio t level) = ↑(probability t level)

          The half-probability identity after coercion to exact finite probabilities.

          source
          theorem Algebraic.AC0.ParityParameters.minimumRatio_le (t : ℕ) (oneLe : 1 ≤ t) (level : ℕ) :
          minimumRatio t ≤ retentionRatio t level

          The later-round ratio is no larger than the first-round ratio.

          source
          noncomputable def Algebraic.AC0.ParityParameters.switchingFailure {n g : ℕ} (program : Program signature n g) (t : ℕ) :
          ENNReal

          Common charged switching failure bound for every round.

          Equations
          Instances For
            source
            theorem Algebraic.AC0.ParityParameters.layerFailure_eq {n g : ℕ} (program : Program signature n g) (t : ℕ) (oneLe : 1 ≤ t) (level : ℕ) :
            Program.layerFailureBoundOfBounds program (probability t level) (treeBound t level) (treeBound t (level + 1)) = switchingFailure program t

            Every concrete round has the same charged failure bound.

            source
            theorem Algebraic.AC0.ParityParameters.layer_slack {n g : ℕ} (program : Program signature n g) (t : ℕ) (oneLe : 1 ≤ t) (level : ℕ) (small : switchingFailure program t < ↑(minimumRatio t)) :
            Program.layerFailureBoundOfBounds program (probability t level) (treeBound t level) (treeBound t (level + 1)) + ↑(retentionRatio t level) < ↑(probability t level)

            One uniform small-failure hypothesis supplies the probability slack for every concrete round.