Documentation

Complexitylib.Circuits.DepthThree.LowerBound.Internal.FiniteProbabilityBounds

Unrestricted depth-three lower bound: finite probability bounds #

Adapted from OpenAI's formalization at revision adc7f1241b42e322a6451854ab7e4b4c146bf78a. Source: https://github.com/openai/math/blob/adc7f1241b42e322a6451854ab7e4b4c146bf78a/lean/OAI/Computability/DepthThree/FiniteProbabilityBounds.lean

Imports, namespaces, module visibility, documentation, and formatting are adapted for complexitylib. The source theorem statements and mathematical proofs are retained.

source
noncomputable def Complexity.DepthThreeLowerBound.finiteProb {Ω : Type uDepth1} [Fintype Ω] (P : Ω → Prop) :
ℝ

Uniform probability of a predicate on a finite type.

Equations
Instances For
    source
    theorem Complexity.DepthThreeLowerBound.finiteProb_nonneg {Ω : Type uDepth2} [Fintype Ω] (P : Ω → Prop) :
    0 ≤ finiteProb P
    source
    theorem Complexity.DepthThreeLowerBound.finiteProb_le_one {Ω : Type uDepth2} [Fintype Ω] [Nonempty Ω] (P : Ω → Prop) :
    finiteProb P ≤ 1
    source
    theorem Complexity.DepthThreeLowerBound.finiteProb_mono {Ω : Type uDepth2} [Fintype Ω] {P Q : Ω → Prop} (h : ∀ (ω : Ω), P ω → Q ω) :
    finiteProb P ≤ finiteProb Q
    source
    theorem Complexity.DepthThreeLowerBound.finiteAvg_exists_le {Ω : Type uDepth2} [Fintype Ω] [Nonempty Ω] (f : Ω → ℝ) :
    ∃ (ω : Ω), f ω ≤ finiteAvg f
    source
    theorem Complexity.DepthThreeLowerBound.finiteAvg_exists_le_of_le {Ω : Type uDepth2} [Fintype Ω] [Nonempty Ω] (f : Ω → ℝ) (c : ℝ) (h : finiteAvg f ≤ c) :
    ∃ (ω : Ω), f ω ≤ c
    source
    theorem Complexity.DepthThreeLowerBound.finiteProb_gt_le {Ω : Type uDepth2} [Fintype Ω] {f : Ω → ℝ} (hf : ∀ (ω : Ω), 0 ≤ f ω) {a : ℝ} (ha : 0 < a) :
    (finiteProb fun (ω : Ω) => a < f ω) ≤ finiteAvg f / a
    source
    theorem Complexity.DepthThreeLowerBound.finiteProb_exists_le_sum {Ω : Type uDepth2} [Fintype Ω] {ι : Type uDepth4} (s : Finset ι) (P : ι → Ω → Prop) :
    (finiteProb fun (ω : Ω) => ∃ i ∈ s, P i ω) ≤ ∑ i ∈ s, finiteProb (P i)
    source
    theorem Complexity.DepthThreeLowerBound.finiteProb_abs_gt_le_moment {Ω : Type uDepth2} [Fintype Ω] (f : Ω → ℝ) (t : ℕ) (ht : 0 < t) (a C : ℝ) (ha : 0 < a) (hM : (finiteAvg fun (ω : Ω) => |f ω| ^ t) ≤ C) :
    (finiteProb fun (ω : Ω) => a < |f ω|) ≤ C / a ^ t
    source
    theorem Complexity.DepthThreeLowerBound.finiteAvg_restrictionAvg {Ω : Type uDepth2} [Fintype Ω] {V : Type uDepth5} [Fintype V] (p : ℝ) (F : Ω → Restriction V → ℝ) :
    (finiteAvg fun (ω : Ω) => restrictionAvg p (F ω)) = restrictionAvg p fun (σ : Restriction V) => finiteAvg fun (ω : Ω) => F ω σ