Unrestricted depth-three lower bound: marker permutation

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

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

noncomputable def Complexity.DepthThreeLowerBound.permutationRank {L : Type u} [instFintypeL : Fintype L] (π : Equiv.Perm L) (l : L) : Fin (Fintype.card L)

The position of an element in a permutation order.

Equations

• Complexity.DepthThreeLowerBound.permutationRank π l = (Fintype.equivFin L) (π l)

def Complexity.DepthThreeLowerBound.IsFirst {L : Type u} [instFintypeL : Fintype L] (S : Finset L) (π : Equiv.Perm L) (s : L) : Prop

The selected element occurs first among the specified competitors.

Equations

• Complexity.DepthThreeLowerBound.IsFirst S π s = (s ∈ S ∧ ∀ t ∈ S, Complexity.DepthThreeLowerBound.permutationRank π s ≤ Complexity.DepthThreeLowerBound.permutationRank π t)

theorem Complexity.DepthThreeLowerBound.permutationRank_injective {L : Type u} [instFintypeL : Fintype L] (π : Equiv.Perm L) : Function.Injective (permutationRank π)

theorem Complexity.DepthThreeLowerBound.exists_isFirst {L : Type u} [instFintypeL : Fintype L] (S : Finset L) (hS : S.Nonempty) (π : Equiv.Perm L) : ∃ (s : L), IsFirst S π s

theorem Complexity.DepthThreeLowerBound.isFirst_unique {L : Type u} [instFintypeL : Fintype L] {S : Finset L} {π : Equiv.Perm L} {s t : L} (hs : IsFirst S π s) (ht : IsFirst S π t) : s = t

def Complexity.DepthThreeLowerBound.permutationInputSwap {L : Type u} [instDecidableEqL : DecidableEq L] (s t : L) : Equiv.Perm (Equiv.Perm L)

Swap input labels in the permutation used for marker sampling.

Equations

• One or more equations did not get rendered due to their size.

theorem Complexity.DepthThreeLowerBound.permutation_first_ratio {L : Type u} [instFintypeL : Fintype L] [instDecidableEqL : DecidableEq L] (S M : Finset L) (hS : S.Nonempty) (hMS : M ⊆ S) : (∑ π : Equiv.Perm L, if ∃ s ∈ M, IsFirst S π s then 1 else 0) / ↑(Fintype.card (Equiv.Perm L)) = ↑M.card / ↑S.card