def Hex.PermGroup.randomIndexAttempts : ℕ

The number of rejection attempts randomIndex makes before it returns index zero.

Equations

• Hex.PermGroup.randomIndexAttempts = 128

def Hex.PermGroup.randomDigits {g : Type} [RandomGen g] {m : Type → Type} [Monad m] (lo width : ℕ) : ℕ → RandGT g m ℕ

Read k generator draws as the base-width digits of a number below width ^ k, least significant digit first. Each draw is shifted down by lo and reduced modulo width. The reduction changes nothing for a draw in the generator's range [lo, lo + width - 1].

Equations

• Hex.PermGroup.randomDigits lo width 0 = pure 0
• Hex.PermGroup.randomDigits lo width k.succ = do let d ← Rand.next let rest ← Hex.PermGroup.randomDigits lo width k pure ((d - lo) % width + width * rest)

def Hex.PermGroup.digitSpan (width bound fuel k span : ℕ) : ℕ × ℕ

Starting from (k, span), multiply span by width at most fuel times until it reaches bound, and return the final count and span.

Equations

• Hex.PermGroup.digitSpan width bound 0 x✝¹ x✝ = (x✝¹, x✝)
• Hex.PermGroup.digitSpan width bound fuel.succ x✝¹ x✝ = if bound ≤ x✝ then (x✝¹, x✝) else Hex.PermGroup.digitSpan width bound fuel (x✝¹ + 1) (x✝ * width)

def Hex.PermGroup.randomIndex {g : Type} [RandomGen g] {m : Type → Type} [Monad m] (bound : ℕ) (h : 0 < bound) : RandGT g m (Fin bound)

An index in Fin bound drawn by rejection sampling from the generator.

Let [lo, hi] be the generator's range and width = hi + 1 - lo. Take the least k with bound ≤ width ^ k and span = width ^ k. One attempt reads k draws as a number x < span (randomDigits) and accepts it when x is below limit, the largest multiple of bound that is at most span, returning x % bound. No modular reduction is applied to an incomplete range.

If the draws are independent and uniform on [lo, hi], then x is uniform below span, an accepted x is uniform below limit, and x % bound is exactly uniform on Fin bound. Since bound ≤ span, limit > span / 2, so each attempt accepts with probability above one half. After randomIndexAttempts = 128 rejections in a row the result is index zero. That happens with probability below 2 ^ (-128), so each index has probability within 2 ^ (-128) of 1 / bound, and exactly 1 / bound conditional on some attempt being accepted. The fixed number of attempts keeps the definition total in RandGT g m for every monad m, including for generators that are not uniform. A range with fewer than two values carries no randomness, and the result is then index zero without any draw.

Equations

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

def Hex.PermGroup.randomIndex.attempt {g : Type} [RandomGen g] {m : Type → Type} [Monad m] (bound : ℕ) (h : 0 < bound) (lo width k limit : ℕ) : ℕ → RandGT g m (Fin bound)

At most fuel attempts with acceptance threshold limit.

Equations

• One or more equations did not get rendered due to their size.
• Hex.PermGroup.randomIndex.attempt bound h lo width k limit 0 = pure ⟨0, h⟩

def Hex.PermGroup.Group.rankEquiv {n : ℕ} (G : Group n) : Element G ≃ Fin G.order

The computational rank and unrank functions form an equivalence.

Equations

• G.rankEquiv = { toFun := G.rank, invFun := G.unrank, left_inv := ⋯, right_inv := ⋯ }

def Hex.PermGroup.Group.indexEquiv {n : ℕ} (G : Group n) : Fin G.order ≃ ↥(closure G.generators)

The same indexing identifies the corresponding Mathlib subgroup.

Equations

• G.indexEquiv = G.rankEquiv.symm.trans (Hex.PermGroup.Element.equiv G).toEquiv

theorem Hex.PermGroup.Group.unrank_probability {n : ℕ} (G : Group n) (source : PMF (Fin G.order)) (p : Element G) : (PMF.map G.unrank source) p = source (G.rank p)

Each output element receives exactly the mass at its unique input index.

theorem Hex.PermGroup.Group.sample_uniform {n : ℕ} (G : Group n) (source : PMF (Fin G.order)) (h : ∀ (k : Fin G.order), source k = (↑G.order)⁻¹) (p : Element G) : (PMF.map G.unrank source) p = (↑G.order)⁻¹

Conditional uniformity: unranking preserves uniform mass supplied on the bounded indices. No assumption about a pseudorandom implementation is made.

theorem Hex.PermGroup.Group.sampleFrom_probability {n : ℕ} (draw : (bound : ℕ) → 0 < bound → PMF (Fin bound)) (G : Group n) (p : Element G) : (sampleFrom draw G) p = (draw G.order ⋯) (G.rank p)

The effect-polymorphic sampling API has the same probability contract when its index source is a probability mass function.

def Hex.PermGroup.Group.randomElement {n : ℕ} {g : Type} [RandomGen g] {m : Type → Type} [Monad m] (G : Group n) : RandGT g m (Element G)

An element of G drawn with Mathlib's random-generator interface: unrank an index from randomIndex. If the generator's draws are independent and uniform on its range, each element has probability within 2 ^ (-128) of 1 / order G, and exactly 1 / order G conditional on the index draw accepting within its attempt limit. Mathlib's randFin is not used, because it reduces a draw modulo the bound and is therefore biased.

Equations

• G.randomElement = Hex.PermGroup.Group.sampleFrom Hex.PermGroup.randomIndex G

@[instance_reducible]

instance Hex.PermGroup.Group.instRandomElementOfMonad_hexPermGroupTheory {n : ℕ} {m : Type → Type} [Monad m] (G : Group n) : Random m (Element G)

Equations

• G.instRandomElementOfMonad_hexPermGroupTheory = { random := fun {g : Type} [RandomGen g] => G.randomElement }

theorem Hex.PermGroup.Group.enumerate_spec {n : ℕ} (G : Group n) (e : Equiv.Perm (Fin n)) : e ∈ Array.map (fun (p : Element G) => (↑p).toEquiv) G.enumerate ↔ e ∈ closure G.generators

Enumerated permutation values are exactly the corresponding subgroup.