Finite probability calculations for adaptive stabilizer learning

These are finite counting identities and real inequalities used in the paper. They do not assert the quantum measurement laws, independence of physical samples, or stochastic domination of a history-dependent stopping time.

noncomputable def LeanPool.SingleCopyStabilizer.FiniteProbability.uniformPMF (α : Type u_1) [Fintype α] [Nonempty α] : PMF α

The uniform probability mass function on a nonempty finite type.

Equations

• LeanPool.SingleCopyStabilizer.FiniteProbability.uniformPMF α = PMF.ofFintype (fun (x : α) => (↑(Fintype.card α))⁻¹) ⋯

@[simp]

theorem LeanPool.SingleCopyStabilizer.FiniteProbability.uniformPMF_apply {α : Type u_1} [Fintype α] [Nonempty α] (a : α) : (uniformPMF α) a = (↑(Fintype.card α))⁻¹

def LeanPool.SingleCopyStabilizer.FiniteProbability.collisionMass {A : Type u_1} [Fintype A] (p : A → ℝ) : ℝ

The collision mass of a finite vector of class probabilities.

Equations

• LeanPool.SingleCopyStabilizer.FiniteProbability.collisionMass p = ∑ a : A, p a ^ 2

theorem LeanPool.SingleCopyStabilizer.FiniteProbability.independent_collision_mass {A : Type u_1} [Fintype A] (p : A → ℝ) [DecidableEq A] : (∑ a : A, ∑ b : A, if a = b then p a * p b else 0) = collisionMass p

For independent draws with weights p, the diagonal of the product weight has total mass ∑ a, p a².

theorem LeanPool.SingleCopyStabilizer.FiniteProbability.one_le_card_mul_collision {A : Type u_1} [Fintype A] (p : A → ℝ) (hp : ∑ a : A, p a = 1) : 1 ≤ ↑(Fintype.card A) * collisionMass p

Cauchy--Schwarz in the form used for the coset collision estimate.

theorem LeanPool.SingleCopyStabilizer.FiniteProbability.inv_card_le_collision {A : Type u_1} [Fintype A] [Nonempty A] (p : A → ℝ) (hp : ∑ a : A, p a = 1) : 1 / ↑(Fintype.card A) ≤ collisionMass p

Any normalized class weights have collision mass at least 1 / #A.

theorem LeanPool.SingleCopyStabilizer.FiniteProbability.inverse_two_pow_le_collision {A : Type u_1} [Fintype A] (p : A → ℝ) (hp : ∑ a : A, p a = 1) (r : ℕ) (hcard : Fintype.card A ≤ 2 ^ r) : 1 / 2 ^ r ≤ collisionMass p

At most 2^r cosets give the paper's collision lower bound 2^(-r). The expression on the left is written 1 / 2^r to use natural exponents.

def LeanPool.SingleCopyStabilizer.FiniteProbability.differenceFiberEquiv {G : Type u_1} [AddCommGroup G] (u : G) : { xy : G × G // xy.1 - xy.2 = u } ≃ G

Fixing a difference leaves precisely one free outcome: (x,y) ↦ y, with inverse y ↦ (u+y,y).

Equations

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

theorem LeanPool.SingleCopyStabilizer.FiniteProbability.affine_difference {G : Type u_1} [AddCommGroup G] (z x y : G) : z + x - (z + y) = x - y

Translating both samples by the same affine offset leaves their additive difference unchanged.

theorem LeanPool.SingleCopyStabilizer.FiniteProbability.difference_fiber_card {G : Type u_1} [AddCommGroup G] [Fintype G] [DecidableEq G] (u : G) : Fintype.card { xy : G × G // xy.1 - xy.2 = u } = Fintype.card G

Every difference has exactly #G ordered representations in G × G.

theorem LeanPool.SingleCopyStabilizer.FiniteProbability.uniform_difference_probability {G : Type u_1} [AddCommGroup G] [Fintype G] [DecidableEq G] (u : G) : ↑(Fintype.card { xy : G × G // xy.1 - xy.2 = u }) / ↑(Fintype.card (G × G)) = 1 / ↑(Fintype.card G)

Thus the difference of two independent uniform samples is uniform, expressed as the ratio of favorable ordered pairs to all ordered pairs.

theorem LeanPool.SingleCopyStabilizer.FiniteProbability.uniform_difference_pmf {G : Type u_1} [AddCommGroup G] [Fintype G] : PMF.map (fun (xy : G × G) => xy.1 - xy.2) (uniformPMF (G × G)) = uniformPMF G

The probability-mass-function pushforward of the uniform ordered-pair distribution under subtraction is exactly the uniform distribution on G.

noncomputable def LeanPool.SingleCopyStabilizer.FiniteProbability.sameClassDifferenceMass {G : Type u_1} [AddCommGroup G] [Fintype G] [DecidableEq G] {A : Type u_2} [Fintype A] (p : A → ℝ) (u : G) : ℝ

The mass of one specified within-class difference when each class is uniform internally and class a has mass p a.

Equations

• LeanPool.SingleCopyStabilizer.FiniteProbability.sameClassDifferenceMass p u = ∑ a : A, ∑ _xy : { xy : G × G // xy.1 - xy.2 = u }, p a / ↑(Fintype.card G) * (p a / ↑(Fintype.card G))

theorem LeanPool.SingleCopyStabilizer.FiniteProbability.same_class_difference_mass {G : Type u_1} [AddCommGroup G] [Fintype G] [DecidableEq G] {A : Type u_2} [Fintype A] (p : A → ℝ) (u : G) : sameClassDifferenceMass p u = collisionMass p / ↑(Fintype.card G)

Within-class differences all have the same mass, namely collision mass divided by the size of the common translation group.

theorem LeanPool.SingleCopyStabilizer.FiniteProbability.nonzero_same_class_difference_mass {G : Type u_1} [AddCommGroup G] [Fintype G] [DecidableEq G] {A : Type u_2} [Fintype A] (p : A → ℝ) : ∑ u ∈ Finset.univ.erase 0, sameClassDifferenceMass p u = collisionMass p * (1 - 1 / ↑(Fintype.card G))

Summing the nonzero within-class differences gives exactly the factor collisionMass p * (1 - 1 / #G) used in the nullity argument.

theorem LeanPool.SingleCopyStabilizer.FiniteProbability.low_nullity_nonzero_mass_lower_bound {G : Type u_1} [AddCommGroup G] [Fintype G] [DecidableEq G] {A : Type u_2} [Fintype A] (p : A → ℝ) (hp : ∑ a : A, p a = 1) (r j : ℕ) (hclasses : Fintype.card A ≤ 2 ^ r) (hgroup : Fintype.card G = 2 ^ j) : 1 / 2 ^ r * (1 - 1 / 2 ^ j) ≤ ∑ u ∈ Finset.univ.erase 0, sameClassDifferenceMass p u

The low-nullity nonzero collision estimate, with the class and translation-space cardinality assumptions displayed explicitly.

theorem LeanPool.SingleCopyStabilizer.FiniteProbability.survival_le_geometric (s : ℕ → ℝ) (p : ℝ) (hp : p ≤ 1) (hzero : s 0 ≤ 1) (hstep : ∀ (k : ℕ), s (k + 1) ≤ (1 - p) * s k) (k : ℕ) : s k ≤ (1 - p) ^ k

A numerical survival recurrence gives the usual geometric tail. The recurrence is an explicit hypothesis, not a proved law of the algorithm.

theorem LeanPool.SingleCopyStabilizer.FiniteProbability.finite_survival_sum_le (s : ℕ → ℝ) (p : ℝ) (hp0 : 0 < p) (hp1 : p ≤ 1) (hzero : s 0 ≤ 1) (hstep : ∀ (k : ℕ), s (k + 1) ≤ (1 - p) * s k) (n : ℕ) : ∑ k ∈ Finset.range n, s k ≤ (1 - (1 - p) ^ n) / p

A finite sum of survival terms is bounded by the corresponding finite geometric sum, written in closed form.

theorem LeanPool.SingleCopyStabilizer.FiniteProbability.finite_survival_sum_le_inverse (s : ℕ → ℝ) (p : ℝ) (hp0 : 0 < p) (hp1 : p ≤ 1) (hzero : s 0 ≤ 1) (hstep : ∀ (k : ℕ), s (k + 1) ≤ (1 - p) * s k) (n : ℕ) : ∑ k ∈ Finset.range n, s k ≤ 1 / p

Thus every finite truncation of the tail sum is at most 1/p. Connecting this to a random variable's expectation is a separate step.

noncomputable def LeanPool.SingleCopyStabilizer.FiniteProbability.progressProbability (j : ℕ) : ℝ

The success parameter for a positive codimension j.

Equations

• LeanPool.SingleCopyStabilizer.FiniteProbability.progressProbability j = (1 - (1 / 2) ^ j) / 2

theorem LeanPool.SingleCopyStabilizer.FiniteProbability.progress_probability_ge_quarter (j : ℕ) (hj : 0 < j) : 1 / 4 ≤ progressProbability j

Every positive level has progress parameter at least one quarter.

theorem LeanPool.SingleCopyStabilizer.FiniteProbability.reciprocal_sum_le (n : ℕ) : ∑ k ∈ Finset.range n, 2 / (1 - (1 / 2) ^ (k + 1)) ≤ 2 * ↑n + 4 - 4 * (1 / 2) ^ n

A strengthened finite reciprocal-sum estimate. This is an arithmetic bound, not an expectation or stopping-time theorem.

theorem LeanPool.SingleCopyStabilizer.FiniteProbability.reciprocal_sum_lt_two_n_add_four (n : ℕ) : ∑ k ∈ Finset.range n, 2 / (1 - (1 / 2) ^ (k + 1)) < 2 * ↑n + 4

The paper's strict numerical bound on the sum of reciprocal progress parameters. The connection to expected waiting times is not assumed here.

theorem LeanPool.SingleCopyStabilizer.FiniteProbability.scaled_reciprocal_sum_lt (r n : ℕ) : 2 ^ r * ∑ k ∈ Finset.range n, 2 / (1 - (1 / 2) ^ (k + 1)) < 2 ^ r * (2 * ↑n + 4)

Scaling the same finite bound gives the low-nullity arithmetic bound.