Documentation

Complexitylib.Circuits.DepthThree.LowerBound.Internal.EntropyThreshold

Unrestricted depth-three lower bound: entropy threshold #

Adapted from OpenAI's formalization at revision adc7f1241b42e322a6451854ab7e4b4c146bf78a. Source: https://github.com/openai/math/blob/adc7f1241b42e322a6451854ab7e4b4c146bf78a/lean/OAI/Computability/DepthThree/EntropyThreshold.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.binaryEntropy (x : ℝ) :
ℝ

The base-two binary entropy function.

Equations
Instances For
    source
    @[simp]
    theorem Complexity.DepthThreeLowerBound.binaryEntropy_zero :
    binaryEntropy 0 = 0
    source
    @[simp]
    theorem Complexity.DepthThreeLowerBound.binaryEntropy_one :
    binaryEntropy 1 = 0
    source
    theorem Complexity.DepthThreeLowerBound.binaryEntropy_mul_log_two (x : ℝ) :
    binaryEntropy x * Real.log 2 = -(x * Real.log x + (1 - x) * Real.log (1 - x))
    source
    theorem Complexity.DepthThreeLowerBound.binaryEntropy_nonneg {x : ℝ} (hx₀ : 0 ≤ x) (hx₁ : x ≤ 1) :
    0 ≤ binaryEntropy x
    source
    theorem Complexity.DepthThreeLowerBound.continuous_binaryEntropy :
    Continuous binaryEntropy
    source
    theorem Complexity.DepthThreeLowerBound.tendsto_binaryEntropy_reciprocal :
    Filter.Tendsto (fun (r : ℕ) => binaryEntropy (1 / ↑r)) Filter.atTop (nhds 0)
    source
    theorem Complexity.DepthThreeLowerBound.exists_integer_entropy_threshold (F : ℕ) {ε : ℝ} (hε : 0 < ε) :
    ∃ (r : ℕ), 2 ≤ r ∧ ↑F * binaryEntropy (1 / ↑r) ≤ ε