def CommutingRepetition.ClassicalSampling.markedFirst {α : Type u_1} [Fintype α] (rank : α ≃ Fin (Fintype.card α)) (marked : Finset α) (nonempty : marked.Nonempty) (permutation : Equiv.Perm α) : α

Equations

• CommutingRepetition.ClassicalSampling.markedFirst rank marked nonempty permutation = (Equiv.symm permutation) (rank.symm ((Finset.image (fun (a : α) => rank (permutation a)) marked).min' ⋯))

theorem CommutingRepetition.ClassicalSampling.markedFirst_mem {α : Type u_1} [Fintype α] (rank : α ≃ Fin (Fintype.card α)) (marked : Finset α) (nonempty : marked.Nonempty) (permutation : Equiv.Perm α) : markedFirst rank marked nonempty permutation ∈ marked

theorem CommutingRepetition.ClassicalSampling.markedFirst_rank {α : Type u_1} [Fintype α] (rank : α ≃ Fin (Fintype.card α)) (marked : Finset α) (nonempty : marked.Nonempty) (permutation : Equiv.Perm α) : rank (permutation (markedFirst rank marked nonempty permutation)) = (Finset.image (fun (a : α) => rank (permutation a)) marked).min' ⋯

theorem CommutingRepetition.ClassicalSampling.markedFirst_rank_le {α : Type u_1} [Fintype α] (rank : α ≃ Fin (Fintype.card α)) (marked : Finset α) (nonempty : marked.Nonempty) (permutation : Equiv.Perm α) {a : α} (ha : a ∈ marked) : rank (permutation (markedFirst rank marked nonempty permutation)) ≤ rank (permutation a)

theorem CommutingRepetition.ClassicalSampling.markedFirst_eq_of_mem_of_rank_le {α : Type u_1} [Fintype α] (rank : α ≃ Fin (Fintype.card α)) (marked : Finset α) (nonempty : marked.Nonempty) (permutation : Equiv.Perm α) {a : α} (ha : a ∈ marked) (hle : ∀ b ∈ marked, rank (permutation a) ≤ rank (permutation b)) : markedFirst rank marked nonempty permutation = a

theorem CommutingRepetition.ClassicalSampling.markedFirst_subset_eq_of_mem {α : Type u_1} [Fintype α] (rank : α ≃ Fin (Fintype.card α)) {small large : Finset α} (hsmall : small.Nonempty) (hlarge : large.Nonempty) (permutation : Equiv.Perm α) (hsub : small ⊆ large) (hmem : markedFirst rank large hlarge permutation ∈ small) : markedFirst rank small hsmall permutation = markedFirst rank large hlarge permutation

theorem CommutingRepetition.ClassicalSampling.markedFirst_eq_iff_union_first_mem_inter {α : Type u_1} [Fintype α] [DecidableEq α] (rank : α ≃ Fin (Fintype.card α)) (left right : Finset α) (hleft : left.Nonempty) (hright : right.Nonempty) (permutation : Equiv.Perm α) : markedFirst rank left hleft permutation = markedFirst rank right hright permutation ↔ markedFirst rank (left ∪ right) ⋯ permutation ∈ left ∩ right

theorem CommutingRepetition.ClassicalSampling.markedFirst_ne_iff_union_first_mem_symmDiff {α : Type u_1} [Fintype α] [DecidableEq α] (rank : α ≃ Fin (Fintype.card α)) (left right : Finset α) (hleft : left.Nonempty) (hright : right.Nonempty) (permutation : Equiv.Perm α) : markedFirst rank left hleft permutation ≠ markedFirst rank right hright permutation ↔ markedFirst rank (left ∪ right) ⋯ permutation ∈ left \ right ∪ right \ left

theorem CommutingRepetition.ClassicalSampling.swap_mem_iff_of_mem {α : Type u_1} [DecidableEq α] {marked : Finset α} {x y : α} (hx : x ∈ marked) (hy : y ∈ marked) (a : α) : (Equiv.swap x y) a ∈ marked ↔ a ∈ marked

theorem CommutingRepetition.ClassicalSampling.markedFirst_swap_trans {α : Type u_1} [Fintype α] [DecidableEq α] (rank : α ≃ Fin (Fintype.card α)) (marked : Finset α) (nonempty : marked.Nonempty) {x y : α} (hx : x ∈ marked) (hy : y ∈ marked) (permutation : Equiv.Perm α) : markedFirst rank marked nonempty (Equiv.trans (Equiv.swap x y) permutation) = (Equiv.swap x y) (markedFirst rank marked nonempty permutation)

def CommutingRepetition.ClassicalSampling.firstFiber {α : Type u_1} [Fintype α] [DecidableEq α] (rank : α ≃ Fin (Fintype.card α)) (marked : Finset α) (nonempty : marked.Nonempty) (a : α) : Finset (Equiv.Perm α)

Equations

• CommutingRepetition.ClassicalSampling.firstFiber rank marked nonempty a = {permutation : Equiv.Perm α | CommutingRepetition.ClassicalSampling.markedFirst rank marked nonempty permutation = a}

theorem CommutingRepetition.ClassicalSampling.firstFiber_card_eq {α : Type u_1} [Fintype α] [DecidableEq α] (rank : α ≃ Fin (Fintype.card α)) (marked : Finset α) (nonempty : marked.Nonempty) {x y : α} (hx : x ∈ marked) (hy : y ∈ marked) : (firstFiber rank marked nonempty x).card = (firstFiber rank marked nonempty y).card

theorem CommutingRepetition.ClassicalSampling.markedFirst_event_card_mul {α : Type u_1} [Fintype α] [DecidableEq α] (rank : α ≃ Fin (Fintype.card α)) (marked : Finset α) (nonempty : marked.Nonempty) (event : Finset α) (hevent : event ⊆ marked) : {permutation : Equiv.Perm α | markedFirst rank marked nonempty permutation ∈ event}.card * marked.card = event.card * Fintype.card (Equiv.Perm α)

theorem CommutingRepetition.ClassicalSampling.sharedPermutation_disagreement_card_mul {α : Type u_1} [Fintype α] [DecidableEq α] (rank : α ≃ Fin (Fintype.card α)) (left right : Finset α) (hleft : left.Nonempty) (hright : right.Nonempty) : {permutation : Equiv.Perm α | markedFirst rank left hleft permutation ≠ markedFirst rank right hright permutation}.card * (left ∪ right).card = (left \ right ∪ right \ left).card * Fintype.card (Equiv.Perm α)

noncomputable def CommutingRepetition.ClassicalSampling.uniformPermutationProbability {α : Type u_1} [Fintype α] [DecidableEq α] (event : Equiv.Perm α → Prop) : ℝ

Equations

• CommutingRepetition.ClassicalSampling.uniformPermutationProbability event = ↑{permutation : Equiv.Perm α | event permutation}.card / ↑(Fintype.card (Equiv.Perm α))

theorem CommutingRepetition.ClassicalSampling.markedFirst_event_probability {α : Type u_1} [Fintype α] [DecidableEq α] (rank : α ≃ Fin (Fintype.card α)) (marked : Finset α) (nonempty : marked.Nonempty) (event : Finset α) (hevent : event ⊆ marked) : (uniformPermutationProbability fun (permutation : Equiv.Perm α) => markedFirst rank marked nonempty permutation ∈ event) = ↑event.card / ↑marked.card

theorem CommutingRepetition.ClassicalSampling.sharedPermutation_disagreement_probability {α : Type u_1} [Fintype α] [DecidableEq α] (rank : α ≃ Fin (Fintype.card α)) (left right : Finset α) (hleft : left.Nonempty) (hright : right.Nonempty) : (uniformPermutationProbability fun (permutation : Equiv.Perm α) => markedFirst rank left hleft permutation ≠ markedFirst rank right hright permutation) = ↑(left \ right ∪ right \ left).card / ↑(left ∪ right).card

theorem CommutingRepetition.ClassicalSampling.sharedPermutation_disagreement_probability_le {α : Type u_1} [Fintype α] [DecidableEq α] (rank : α ≃ Fin (Fintype.card α)) (left right : Finset α) (hleft : left.Nonempty) (hright : right.Nonempty) : (uniformPermutationProbability fun (permutation : Equiv.Perm α) => markedFirst rank left hleft permutation ≠ markedFirst rank right hright permutation) ≤ ↑(left \ right ∪ right \ left).card / ↑left.card

noncomputable def CommutingRepetition.ClassicalSampling.markedTotalVariation {α : Type u_1} [DecidableEq α] (left right : Finset α) : ℝ

Equations

• CommutingRepetition.ClassicalSampling.markedTotalVariation left right = ↑(left \ right ∪ right \ left).card / (2 * ↑left.card)

theorem CommutingRepetition.ClassicalSampling.sharedPermutation_disagreement_probability_le_two_mul_tv {α : Type u_1} [Fintype α] [DecidableEq α] (rank : α ≃ Fin (Fintype.card α)) (left right : Finset α) (hleft : left.Nonempty) (hright : right.Nonempty) (_equal_card : left.card = right.card) : (uniformPermutationProbability fun (permutation : Equiv.Perm α) => markedFirst rank left hleft permutation ≠ markedFirst rank right hright permutation) ≤ 2 * markedTotalVariation left right

def CommutingRepetition.ClassicalSampling.rationalMarked {β : Type u_2} [Fintype β] (denominator : ℕ) (numerator : β → ℕ) : Finset (β × Fin denominator)

Equations

• CommutingRepetition.ClassicalSampling.rationalMarked denominator numerator = {point : β × Fin denominator | ↑point.2 < numerator point.1}

theorem CommutingRepetition.ClassicalSampling.rationalMarked_fiber_card {β : Type u_2} [Fintype β] [DecidableEq β] (denominator : ℕ) (numerator : β → ℕ) (letter : β) : {point ∈ rationalMarked denominator numerator | point.1 = letter}.card = min denominator (numerator letter)

theorem CommutingRepetition.ClassicalSampling.rationalNumerator_le_denominator {β : Type u_2} [Fintype β] (denominator : ℕ) (numerator : β → ℕ) (normalized : ∑ letter : β, numerator letter = denominator) (letter : β) : numerator letter ≤ denominator

theorem CommutingRepetition.ClassicalSampling.rationalMarked_card {β : Type u_2} [Fintype β] [DecidableEq β] (denominator : ℕ) (numerator : β → ℕ) (normalized : ∑ letter : β, numerator letter = denominator) : (rationalMarked denominator numerator).card = denominator

theorem CommutingRepetition.ClassicalSampling.rationalMarked_nonempty {β : Type u_2} [Fintype β] [DecidableEq β] (denominator : ℕ) (numerator : β → ℕ) (normalized : ∑ letter : β, numerator letter = denominator) (positive : 0 < denominator) : (rationalMarked denominator numerator).Nonempty

theorem CommutingRepetition.ClassicalSampling.rationalMarked_letter_probability {β : Type u_2} [Fintype β] [DecidableEq β] (denominator : ℕ) (numerator : β → ℕ) (normalized : ∑ letter : β, numerator letter = denominator) (nonempty : (rationalMarked denominator numerator).Nonempty) (rank : β × Fin denominator ≃ Fin (Fintype.card (β × Fin denominator))) (letter : β) : (uniformPermutationProbability fun (permutation : Equiv.Perm (β × Fin denominator)) => (markedFirst rank (rationalMarked denominator numerator) nonempty permutation).1 = letter) = ↑(numerator letter) / ↑denominator