Documentation

Complexitylib.Circuits.DepthThree.LowerBound.Internal.AlgebraFiniteFibers

Unrestricted depth-three lower bound: algebra finite fibers #

Adapted from OpenAI's formalization at revision adc7f1241b42e322a6451854ab7e4b4c146bf78a. Source: https://github.com/openai/math/blob/adc7f1241b42e322a6451854ab7e4b4c146bf78a/lean/OAI/Computability/DepthThree/AlgebraFiniteFibers.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.AlgebraFiniteFibers.fiberEquivKernel {A : Type uDepth1} {B : Type uDepth2} [AddCommGroup A] [AddCommGroup B] (L : A →+ B) (hL : Function.Surjective ⇑L) (b : B) :
{ a : A // L a = b } ≃ { a : A // L a = 0 }

Identify a nonempty fiber of a linear map with its kernel by translation.

Equations
  • One or more equations did not get rendered due to their size.
Instances For
    source
    theorem Complexity.DepthThreeLowerBound.AlgebraFiniteFibers.card_fiber_eq {A : Type uDepth1} {B : Type uDepth2} [AddCommGroup A] [AddCommGroup B] [Fintype A] [DecidableEq B] (L : A →+ B) (hL : Function.Surjective ⇑L) (b : B) :
    Fintype.card { a : A // L a = b } = Fintype.card { a : A // L a = 0 }
    source
    theorem Complexity.DepthThreeLowerBound.AlgebraFiniteFibers.card_filter_fiber_eq {A : Type uDepth1} {B : Type uDepth2} [AddCommGroup A] [AddCommGroup B] [Fintype A] [DecidableEq B] (L : A →+ B) (hL : Function.Surjective ⇑L) (b : B) :
    {a : A | L a = b}.card = {a : A | L a = 0}.card
    source
    theorem Complexity.DepthThreeLowerBound.AlgebraFiniteFibers.card_eq_mul_card_kernel {A : Type uDepth1} {B : Type uDepth2} [AddCommGroup A] [AddCommGroup B] [Fintype A] [instFintypeB : Fintype B] [DecidableEq B] (L : A →+ B) (hL : Function.Surjective ⇑L) :
    Fintype.card A = Fintype.card B * Fintype.card { a : A // L a = 0 }
    source
    theorem Complexity.DepthThreeLowerBound.AlgebraFiniteFibers.sum_comp {A : Type uDepth1} {B : Type uDepth2} [AddCommGroup A] [AddCommGroup B] [Fintype A] [instFintypeB : Fintype B] [DecidableEq B] (L : A →+ B) (hL : Function.Surjective ⇑L) (f : B → ℝ) :
    ∑ a : A, f (L a) = ↑(Fintype.card { a : A // L a = 0 }) * ∑ b : B, f b
    source
    theorem Complexity.DepthThreeLowerBound.AlgebraFiniteFibers.finiteAvg_comp {A : Type uDepth1} {B : Type uDepth2} [AddCommGroup A] [AddCommGroup B] [Fintype A] [instFintypeB : Fintype B] [DecidableEq B] (L : A →+ B) (hL : Function.Surjective ⇑L) (f : B → ℝ) :
    (finiteAvg fun (a : A) => f (L a)) = finiteAvg f