Documentation

Complexitylib.Algebraic.LowerBound.AC0.RandomRestriction

The finite p-random restriction distribution #

For 0 <= p <= 1, every input coordinate is independently left live with probability p, fixed to false with probability (1 - p) / 2, and fixed to true with the same probability. Parameters are nonnegative reals and event probabilities are extended nonnegative reals, matching mathlib's PMF API.

The distribution is defined by its exact finite product mass. The normalization proof factors the sum over all partial assignments into the product of the three-state coordinate sums. No sampler or empirical approximation is used.

source
noncomputable def Algebraic.AC0.RandomRestriction.fixedWeight (p : NNReal) :
NNReal

Probability of either fixed Boolean value at one coordinate.

Equations
Instances For
    source
    noncomputable def Algebraic.AC0.RandomRestriction.coordinateWeight (p : NNReal) :
    Option Bool → NNReal

    One-coordinate mass: p for a live variable and (1 - p) / 2 for either fixed value.

    Equations
    Instances For
      source
      @[simp]
      theorem Algebraic.AC0.RandomRestriction.coordinateWeight_none (p : NNReal) :
      coordinateWeight p none = p
      source
      @[simp]
      theorem Algebraic.AC0.RandomRestriction.coordinateWeight_some (p : NNReal) (value : Bool) :
      coordinateWeight p (some value) = fixedWeight p
      source
      theorem Algebraic.AC0.RandomRestriction.sum_coordinateWeight (p : NNReal) (atMostOne : p ≤ 1) :
      ∑ state : Option Bool, ↑(coordinateWeight p state) = 1

      The three one-coordinate masses sum exactly to one.

      source
      noncomputable def Algebraic.AC0.RandomRestriction.weight {n : ℕ} (p : NNReal) (rho : PartialAssignment n) :
      ENNReal

      Product mass of a particular restriction.

      Equations
      Instances For
        source
        theorem Algebraic.AC0.RandomRestriction.sum_weight (n : ℕ) (p : NNReal) (atMostOne : p ≤ 1) :
        ∑ rho : PartialAssignment n, weight p rho = 1

        The finite product masses over all restrictions sum exactly to one.

        source
        noncomputable def Algebraic.AC0.RandomRestriction.distribution (n : ℕ) (p : NNReal) (atMostOne : p ≤ 1) :
        PMF (PartialAssignment n)

        The standard independent p-random restriction on n variables.

        Equations
        Instances For
          source
          @[simp]
          theorem Algebraic.AC0.RandomRestriction.distribution_apply (n : ℕ) (p : NNReal) (atMostOne : p ≤ 1) (rho : PartialAssignment n) :
          (distribution n p atMostOne) rho = weight p rho
          source
          theorem Algebraic.AC0.RandomRestriction.weight_eq_live_fixed {n : ℕ} (p : NNReal) (rho : PartialAssignment n) :
          weight p rho = ↑p ^ rho.liveCount * ↑(fixedWeight p) ^ rho.fixedCount

          The product mass depends only on the numbers of live and fixed variables.

          source
          theorem Algebraic.AC0.RandomRestriction.distribution_apply_eq_live_fixed (n : ℕ) (p : NNReal) (atMostOne : p ≤ 1) (rho : PartialAssignment n) :
          (distribution n p atMostOne) rho = ↑p ^ rho.liveCount * ↑(fixedWeight p) ^ rho.fixedCount

          Closed form for the mass assigned to an individual restriction.

          source
          noncomputable def Algebraic.AC0.RandomRestriction.probability (n : ℕ) (p : NNReal) (atMostOne : p ≤ 1) (event : PartialAssignment n → Prop) [DecidablePred event] :
          ENNReal

          Probability of a predicate under the finite random-restriction distribution.

          Equations
          Instances For
            source
            @[simp]
            theorem Algebraic.AC0.RandomRestriction.probability_true (n : ℕ) (p : NNReal) (atMostOne : p ≤ 1) :
            (probability n p atMostOne fun (x : PartialAssignment n) => True) = 1

            The certain event has probability one.

            source
            @[simp]
            theorem Algebraic.AC0.RandomRestriction.probability_false (n : ℕ) (p : NNReal) (atMostOne : p ≤ 1) :
            (probability n p atMostOne fun (x : PartialAssignment n) => False) = 0

            The impossible event has probability zero.

            source
            theorem Algebraic.AC0.RandomRestriction.probability_add_complement (n : ℕ) (p : NNReal) (atMostOne : p ≤ 1) (event : PartialAssignment n → Prop) [DecidablePred event] :
            (probability n p atMostOne event + probability n p atMostOne fun (rho : PartialAssignment n) => ¬event rho) = 1

            An event and its complement have total probability one.

            source
            theorem Algebraic.AC0.RandomRestriction.probability_le_one (n : ℕ) (p : NNReal) (atMostOne : p ≤ 1) (event : PartialAssignment n → Prop) [DecidablePred event] :
            probability n p atMostOne event ≤ 1

            Every event has probability at most one.

            source
            theorem Algebraic.AC0.RandomRestriction.probability_congr (n : ℕ) (p : NNReal) (atMostOne : p ≤ 1) {left right : PartialAssignment n → Prop} [DecidablePred left] [DecidablePred right] (equal : ∀ (rho : PartialAssignment n), left rho ↔ right rho) :
            probability n p atMostOne left = probability n p atMostOne right

            Extensionally equal events have equal probability.

            source
            theorem Algebraic.AC0.RandomRestriction.probability_mono (n : ℕ) (p : NNReal) (atMostOne : p ≤ 1) {left right : PartialAssignment n → Prop} [DecidablePred left] [DecidablePred right] (included : ∀ (rho : PartialAssignment n), left rho → right rho) :
            probability n p atMostOne left ≤ probability n p atMostOne right

            Inclusion of finite events implies monotonicity of their exact probabilities.

            source
            theorem Algebraic.AC0.RandomRestriction.probability_or_le (n : ℕ) (p : NNReal) (atMostOne : p ≤ 1) (left right : PartialAssignment n → Prop) [DecidablePred left] [DecidablePred right] :
            (probability n p atMostOne fun (rho : PartialAssignment n) => left rho ∨ right rho) ≤ probability n p atMostOne left + probability n p atMostOne right

            The exact probability of a union of two finite events is at most the sum of their probabilities.

            source
            theorem Algebraic.AC0.RandomRestriction.probability_exists_mem_le_sum {indexType : Type u_1} (n : ℕ) (p : NNReal) (atMostOne : p ≤ 1) (indices : Finset indexType) (events : indexType → PartialAssignment n → Prop) [(index : indexType) → DecidablePred (events index)] :
            (probability n p atMostOne fun (rho : PartialAssignment n) => ∃ index ∈ indices, events index rho) ≤ ∑ index ∈ indices, probability n p atMostOne (events index)

            Finite union bound for an indexed family of exact restriction events.

            source
            theorem Algebraic.AC0.RandomRestriction.probability_singleton (n : ℕ) (p : NNReal) (atMostOne : p ≤ 1) (target : PartialAssignment n) :
            (probability n p atMostOne fun (rho : PartialAssignment n) => rho = target) = (distribution n p atMostOne) target

            A singleton event has the point mass specified by the product formula.