Rounding a law to a common denominator

noncomputable def CommutingRepetition.RoundedSampler.ceilNum {H : Type} (dens : ℕ) (ρ : ℝ) (q : H → ℝ) (h : H) : ℕ

Ceiling numerators ⌈dens (1−ρ) q(h)⌉.

Equations

• CommutingRepetition.RoundedSampler.ceilNum dens ρ q h = ⌈↑dens * (1 - ρ) * q h⌉₊

noncomputable def CommutingRepetition.RoundedSampler.roundedNum {H : Type} [Fintype H] [DecidableEq H] (dens : ℕ) (ρ : ℝ) (q : H → ℝ) (h₀ h : H) : ℕ

The rounded numerators: the ceilings, with the leftover on a base point.

Equations

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

theorem CommutingRepetition.RoundedSampler.sum_ceilNum_le {H : Type} [Fintype H] [DecidableEq H] (dens : ℕ) {ρ : ℝ} (hρ1 : ρ ≤ 1) (q : H → ℝ) (hq0 : ∀ (h : H), 0 ≤ q h) (hq1 : ∑ h : H, q h ≤ 1) (hcard : ↑(Fintype.card H) ≤ ↑dens * ρ) : ∑ h : H, ceilNum dens ρ q h ≤ dens

theorem CommutingRepetition.RoundedSampler.sum_roundedNum {H : Type} [Fintype H] [DecidableEq H] (dens : ℕ) {ρ : ℝ} (hρ1 : ρ ≤ 1) (q : H → ℝ) (hq0 : ∀ (h : H), 0 ≤ q h) (hq1 : ∑ h : H, q h ≤ 1) (hcard : ↑(Fintype.card H) ≤ ↑dens * ρ) (h₀ : H) : ∑ h : H, roundedNum dens ρ q h₀ h = dens

theorem CommutingRepetition.RoundedSampler.le_roundedNum {H : Type} [Fintype H] [DecidableEq H] (dens : ℕ) (ρ : ℝ) (q : H → ℝ) (h₀ h : H) : ↑dens * (1 - ρ) * q h ≤ ↑(roundedNum dens ρ q h₀ h)

theorem CommutingRepetition.RoundedSampler.roundedNum_eq_zero {H : Type} [Fintype H] [DecidableEq H] (dens : ℕ) (ρ : ℝ) (q : H → ℝ) (h₀ h : H) (hq : q h = 0) (hne : h ≠ h₀) : roundedNum dens ρ q h₀ h = 0

The shared seed and the output

theorem CommutingRepetition.RoundedSampler.rationalMarked_nonempty {H : Type} [Fintype H] [DecidableEq H] (dens : ℕ) (hdens : 0 < dens) (num : H → ℕ) (hsum : ∑ h : H, num h = dens) : (ClassicalSampling.rationalMarked dens num).Nonempty

@[reducible, inline]

abbrev CommutingRepetition.RoundedSampler.Seed (H ι : Type) (dens : ℕ) : Type

The shared seed: a live coordinate and a permutation of H × Fin dens.

Equations

• CommutingRepetition.RoundedSampler.Seed H ι dens = (ι × Equiv.Perm (H × Fin dens))

noncomputable def CommutingRepetition.RoundedSampler.ν {H ι : Type} [Fintype H] [DecidableEq H] [Fintype ι] (dens : ℕ) (_ω : Seed H ι dens) : ℝ

The uniform seed law.

Equations

• CommutingRepetition.RoundedSampler.ν dens _ω = (↑(Fintype.card ι) * ↑(Fintype.card (Equiv.Perm (H × Fin dens))))⁻¹

theorem CommutingRepetition.RoundedSampler.ν_nonneg {H ι : Type} [Fintype H] [DecidableEq H] [Fintype ι] [DecidableEq ι] (dens : ℕ) (ω : Seed H ι dens) : 0 ≤ ν dens ω

theorem CommutingRepetition.RoundedSampler.ν_sum {H ι : Type} [Fintype H] [DecidableEq H] [Fintype ι] [DecidableEq ι] [Nonempty ι] (dens : ℕ) : ∑ ω : Seed H ι dens, ν dens ω = 1

noncomputable def CommutingRepetition.RoundedSampler.output {H ι : Type} [Fintype H] [DecidableEq H] (dens : ℕ) (hdens : 0 < dens) (num : ι → H → ℕ) (hsum : ∀ (i : ι), ∑ h : H, num i h = dens) (ω : Seed H ι dens) : H

The output of the shared-permutation sampler at seed ω for the numerators of live coordinate ω.1.

Equations

• CommutingRepetition.RoundedSampler.output dens hdens num hsum ω = CommutingRepetition.ClassicalInformation.rationalPermutationOutput dens (num ω.1) ⋯ ω.2

theorem CommutingRepetition.RoundedSampler.sum_ite_eq_uniform {H : Type} [Fintype H] [DecidableEq H] (dens : ℕ) (P : Equiv.Perm (H × Fin dens) → Prop) [DecidablePred P] : (∑ π : Equiv.Perm (H × Fin dens), if P π then 1 else 0) = ClassicalSampling.uniformPermutationProbability P * ↑(Fintype.card (Equiv.Perm (H × Fin dens)))

The uniform permutation probability as an indicator sum.

theorem CommutingRepetition.RoundedSampler.sum_ite_ne_eq_uniform {H : Type} [Fintype H] [DecidableEq H] (dens : ℕ) (f g : Equiv.Perm (H × Fin dens) → H) : (∑ π : Equiv.Perm (H × Fin dens), if f π = g π then 0 else 1) = (ClassicalSampling.uniformPermutationProbability fun (π : Equiv.Perm (H × Fin dens)) => f π ≠ g π) * ↑(Fintype.card (Equiv.Perm (H × Fin dens)))

The disagreement probability as an indicator sum.

theorem CommutingRepetition.RoundedSampler.sum_ν_output {H ι : Type} [Fintype H] [DecidableEq H] [Fintype ι] [DecidableEq ι] (dens : ℕ) (hdens : 0 < dens) (num : ι → H → ℕ) (hsum : ∀ (i : ι), ∑ h : H, num i h = dens) (h : H) : (∑ ω : Seed H ι dens, ν dens ω * if output dens hdens num hsum ω = h then 1 else 0) = (↑(Fintype.card ι))⁻¹ * ∑ i : ι, ↑(num i h) / ↑dens

The output law: Pr[output = h] = (1/|ι|) ∑_i num(i, h)/dens.

theorem CommutingRepetition.RoundedSampler.sum_num_eq {H ι : Type} [Fintype H] [DecidableEq H] [Fintype ι] [DecidableEq ι] (dens : ℕ) (num : ι → H → ℕ) (lc : H → ι) (hsupp : ∀ (i : ι) (h : H), lc h ≠ i → num i h = 0) (h : H) : ∑ i : ι, ↑(num i h) / ↑dens = ↑(num (lc h) h) / ↑dens

Numerators supported on the live coordinate collapse the coordinate sum.

Relative entropy against a dominating law

theorem CommutingRepetition.RoundedSampler.finiteRelativeEntropy_le_of_dominates {κ : Type} [Fintype κ] (Q J₀ J' : κ → ℝ) (hQ0 : ∀ (u : κ), 0 ≤ Q u) (hQ1 : ∑ u : κ, Q u = 1) (hJ₀ : ∀ (u : κ), 0 ≤ J₀ u) (habs : ∀ (u : κ), J₀ u = 0 → Q u = 0) (hJ'0 : ∀ (u : κ), 0 ≤ J' u) (hJ'1 : ∑ u : κ, J' u ≤ 1) {ρ : ℝ} (hρ : ρ < 1) (hdom : ∀ (u : κ), (1 - ρ) * J₀ u ≤ J' u) : Pinsker.finiteRelativeEntropy Q J' ≤ ∑ u : κ, Q u * Real.log (Q u / J₀ u) + Real.log (1 / (1 - ρ))

If J' ≥ (1−ρ) J₀ pointwise, the relative entropy against J' is at most the log-sum against J₀ plus log(1/(1−ρ)).

Total variation

theorem CommutingRepetition.RoundedSampler.finiteTotalVariation_triangle {κ : Type} [Fintype κ] (p q r : κ → ℝ) : Pinsker.finiteTotalVariation q r ≤ Pinsker.finiteTotalVariation p q + Pinsker.finiteTotalVariation p r

theorem CommutingRepetition.RoundedSampler.sum_comm3' {α β γ : Type} [Fintype α] [Fintype β] [Fintype γ] (F : α → β → γ → ℝ) : ∑ a : α, ∑ b : β, ∑ c : γ, F a b c = ∑ b : β, ∑ c : γ, ∑ a : α, F a b c

Moving the first of three finite sums to the back.

theorem CommutingRepetition.RoundedSampler.sum_ν_disagree_le {H ι X Y : Type} [Fintype H] [DecidableEq H] [Fintype ι] [DecidableEq ι] [Fintype X] [Fintype Y] (dens : ℕ) (hdens : 0 < dens) (numA : ι → X → H → ℕ) (numB : ι → Y → H → ℕ) (hA : ∀ (i : ι) (x : X), ∑ h : H, numA i x h = dens) (hB : ∀ (i : ι) (y : Y), ∑ h : H, numB i y h = dens) (lc : H → ι) (hsA : ∀ (i : ι) (x : X) (h : H), lc h ≠ i → numA i x h = 0) (hsB : ∀ (i : ι) (y : Y) (h : H), lc h ≠ i → numB i y h = 0) (μ : X → Y → ℝ) (hμ : ∀ (x : X) (y : Y), 0 ≤ μ x y) : (∑ ω : Seed H ι dens, ∑ x : X, ∑ y : Y, ν dens ω * μ x y * if output dens hdens (fun (i : ι) => numA i x) ⋯ ω = output dens hdens (fun (i : ι) => numB i y) ⋯ ω then 0 else 1) ≤ 2 * Pinsker.finiteTotalVariation (fun (u : H × X × Y) => (↑(Fintype.card ι))⁻¹ * μ u.2.1 u.2.2 * (↑(numA (lc u.1) u.2.1 u.1) / ↑dens)) fun (u : H × X × Y) => (↑(Fintype.card ι))⁻¹ * μ u.2.1 u.2.2 * (↑(numB (lc u.1) u.2.2 u.1) / ↑dens)

The mismatch bound: the shared seed makes the two outputs disagree with probability at most twice the total variation of the two output tuple laws.

Sum reorderings and the normalization of the output tuple laws

theorem CommutingRepetition.RoundedSampler.sum_triple {H X Y : Type} [Fintype H] [Fintype X] [Fintype Y] (F : H × X × Y → ℝ) : ∑ u : H × X × Y, F u = ∑ h : H, ∑ x : X, ∑ y : Y, F (h, x, y)

theorem CommutingRepetition.RoundedSampler.sum_comm_hxyω {H X Y S : Type} [Fintype H] [Fintype X] [Fintype Y] [Fintype S] (F : H → X → Y → S → ℝ) : ∑ h : H, ∑ x : X, ∑ y : Y, ∑ ω : S, F h x y ω = ∑ ω : S, ∑ x : X, ∑ y : Y, ∑ h : H, F h x y ω

theorem CommutingRepetition.RoundedSampler.sum_law_A {H ι X Y : Type} [Fintype H] [DecidableEq H] [Fintype ι] [DecidableEq ι] [Fintype X] [Fintype Y] [Nonempty ι] (dens : ℕ) (hdens : 0 < dens) (num : X → ι → H → ℕ) (hsum : ∀ (x : X) (i : ι), ∑ h : H, num x i h = dens) (μ : X → Y → ℝ) (hμsum : ∑ x : X, ∑ y : Y, μ x y = 1) : ∑ u : H × X × Y, (∑ ω : Seed H ι dens, ν dens ω * if output dens hdens (num u.2.1) ⋯ ω = u.1 then 1 else 0) * μ u.2.1 u.2.2 = 1

The Alice-side output tuple law (∑_ω ν(ω) [r_A(ω,x) = h]) μ(x,y) is a probability law.

theorem CommutingRepetition.RoundedSampler.sum_law_B {H ι X Y : Type} [Fintype H] [DecidableEq H] [Fintype ι] [DecidableEq ι] [Fintype X] [Fintype Y] [Nonempty ι] (dens : ℕ) (hdens : 0 < dens) (num : Y → ι → H → ℕ) (hsum : ∀ (y : Y) (i : ι), ∑ h : H, num y i h = dens) (μ : X → Y → ℝ) (hμsum : ∑ x : X, ∑ y : Y, μ x y = 1) : ∑ u : H × X × Y, (∑ ω : Seed H ι dens, ν dens ω * if output dens hdens (num u.2.2) ⋯ ω = u.1 then 1 else 0) * μ u.2.1 u.2.2 = 1

The Bob-side output tuple law is a probability law.