noncomputable def CommutingRepetition.ClassicalInformation.distributionFloorNumerator {ι : Type u_1} (denominator : ℕ) (p : ι → ℝ) : ι → ℕ

Equations

• CommutingRepetition.ClassicalInformation.distributionFloorNumerator denominator p i = ⌊p i * ↑denominator⌋₊

noncomputable def CommutingRepetition.ClassicalInformation.distributionFloorResidual {ι : Type u_1} [Fintype ι] (denominator : ℕ) (p : ι → ℝ) : ℕ

Equations

• CommutingRepetition.ClassicalInformation.distributionFloorResidual denominator p = denominator - ∑ i : ι, CommutingRepetition.ClassicalInformation.distributionFloorNumerator denominator p i

noncomputable def CommutingRepetition.ClassicalInformation.distributionRoundedNumerator {ι : Type u_1} [Fintype ι] [DecidableEq ι] (base : ι) (denominator : ℕ) (p : ι → ℝ) : ι → ℕ

Equations

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

noncomputable def CommutingRepetition.ClassicalInformation.distributionFloorProbability {ι : Type u_1} (denominator : ℕ) (p : ι → ℝ) : ι → ℝ

Equations

• CommutingRepetition.ClassicalInformation.distributionFloorProbability denominator p i = ↑(CommutingRepetition.ClassicalInformation.distributionFloorNumerator denominator p i) / ↑denominator

noncomputable def CommutingRepetition.ClassicalInformation.distributionRoundedProbability {ι : Type u_1} [Fintype ι] [DecidableEq ι] (base : ι) (denominator : ℕ) (p : ι → ℝ) : ι → ℝ

Equations

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

theorem CommutingRepetition.ClassicalInformation.distributionFloorNumerator_cast_le {ι : Type u_1} (denominator : ℕ) (p : ι → ℝ) (hp : ∀ (i : ι), 0 ≤ p i) (i : ι) : ↑(distributionFloorNumerator denominator p i) ≤ p i * ↑denominator

theorem CommutingRepetition.ClassicalInformation.distributionFloorProbability_le {ι : Type u_1} (denominator : ℕ) (positive : 0 < denominator) (p : ι → ℝ) (hp : ∀ (i : ι), 0 ≤ p i) (i : ι) : distributionFloorProbability denominator p i ≤ p i

theorem CommutingRepetition.ClassicalInformation.distributionFloorProbability_error_lt {ι : Type u_1} (denominator : ℕ) (positive : 0 < denominator) (p : ι → ℝ) (i : ι) : p i - distributionFloorProbability denominator p i < 1 / ↑denominator

theorem CommutingRepetition.ClassicalInformation.distributionFloorNumerator_sum_le {ι : Type u_1} [Fintype ι] (denominator : ℕ) (p : ι → ℝ) (hp : ∀ (i : ι), 0 ≤ p i) (normalized : ∑ i : ι, p i = 1) : ∑ i : ι, distributionFloorNumerator denominator p i ≤ denominator

theorem CommutingRepetition.ClassicalInformation.distributionRoundedNumerator_sum {ι : Type u_1} [Fintype ι] [DecidableEq ι] (base : ι) (denominator : ℕ) (p : ι → ℝ) (hp : ∀ (i : ι), 0 ≤ p i) (normalized : ∑ i : ι, p i = 1) : ∑ i : ι, distributionRoundedNumerator base denominator p i = denominator

theorem CommutingRepetition.ClassicalInformation.distributionFloorResidual_probability_eq_sum {ι : Type u_1} [Fintype ι] (denominator : ℕ) (positive : 0 < denominator) (p : ι → ℝ) (hp : ∀ (i : ι), 0 ≤ p i) (normalized : ∑ i : ι, p i = 1) : ↑(distributionFloorResidual denominator p) / ↑denominator = ∑ i : ι, (p i - distributionFloorProbability denominator p i)

theorem CommutingRepetition.ClassicalInformation.distributionRoundedProbability_eq_floor_add {ι : Type u_1} [Fintype ι] [DecidableEq ι] (base : ι) (denominator : ℕ) (p : ι → ℝ) (i : ι) : distributionRoundedProbability base denominator p i = distributionFloorProbability denominator p i + if i = base then ↑(distributionFloorResidual denominator p) / ↑denominator else 0

theorem CommutingRepetition.ClassicalInformation.distributionRoundedProbability_totalVariation_le {ι : Type u_1} [Fintype ι] [DecidableEq ι] (base : ι) (denominator : ℕ) (positive : 0 < denominator) (p : ι → ℝ) (hp : ∀ (i : ι), 0 ≤ p i) (normalized : ∑ i : ι, p i = 1) : Pinsker.finiteTotalVariation p (distributionRoundedProbability base denominator p) ≤ ↑(Fintype.card ι) / ↑denominator

theorem CommutingRepetition.ClassicalInformation.finite_log_sum_inequality {ι : Type u_1} (indices : Finset ι) (p q : ι → ℝ) (hp : ∀ (i : ι), 0 ≤ p i) (hq : ∀ (i : ι), 0 ≤ q i) (absolute_continuity : ∀ (i : ι), q i = 0 → p i = 0) (positive_mass : 0 < ∑ i ∈ indices, q i) : (∑ i ∈ indices, q i) * InformationTheory.klFun ((∑ i ∈ indices, p i) / ∑ i ∈ indices, q i) ≤ ∑ i ∈ indices, q i * InformationTheory.klFun (p i / q i)

def CommutingRepetition.ClassicalInformation.groupedMass {ι : Type u_1} [Fintype ι] {κ : Type u_2} [DecidableEq κ] (map : ι → κ) (p : ι → ℝ) (j : κ) : ℝ

Equations

• CommutingRepetition.ClassicalInformation.groupedMass map p j = ∑ i : ι with map i = j, p i

theorem CommutingRepetition.ClassicalInformation.finite_relative_entropy_data_processing {ι : Type u_1} [Fintype ι] {κ : Type u_2} [Fintype κ] [DecidableEq κ] (map : ι → κ) (p q : ι → ℝ) (hp : ∀ (i : ι), 0 ≤ p i) (hq : ∀ (i : ι), 0 ≤ q i) (absolute_continuity : ∀ (i : ι), q i = 0 → p i = 0) : Pinsker.finiteRelativeEntropy (groupedMass map p) (groupedMass map q) ≤ Pinsker.finiteRelativeEntropy p q

def CommutingRepetition.ClassicalInformation.jointFirstMarginal {ι : Type u_1} {κ : Type u_2} [Fintype κ] (joint : ι × κ → ℝ) : ι → ℝ

Equations

• CommutingRepetition.ClassicalInformation.jointFirstMarginal joint i = ∑ j : κ, joint (i, j)

noncomputable def CommutingRepetition.ClassicalInformation.jointConditional {ι : Type u_1} {κ : Type u_2} [Fintype κ] (joint : ι × κ → ℝ) (i : ι) : κ → ℝ

Equations

• CommutingRepetition.ClassicalInformation.jointConditional joint i j = joint (i, j) / CommutingRepetition.ClassicalInformation.jointFirstMarginal joint i

theorem CommutingRepetition.ClassicalInformation.jointFirstMarginal_nonneg {ι : Type u_1} {κ : Type u_2} [Fintype κ] (joint : ι × κ → ℝ) (nonnegative : ∀ (point : ι × κ), 0 ≤ joint point) (i : ι) : 0 ≤ jointFirstMarginal joint i

theorem CommutingRepetition.ClassicalInformation.jointFirstMarginal_sum {ι : Type u_1} [Fintype ι] {κ : Type u_2} [Fintype κ] (joint : ι × κ → ℝ) : ∑ i : ι, jointFirstMarginal joint i = ∑ point : ι × κ, joint point

theorem CommutingRepetition.ClassicalInformation.jointFirstMarginal_absolute_continuity {ι : Type u_1} {κ : Type u_2} [Fintype κ] (p q : ι × κ → ℝ) (hq : ∀ (point : ι × κ), 0 ≤ q point) (absolute_continuity : ∀ (point : ι × κ), q point = 0 → p point = 0) (i : ι) : jointFirstMarginal q i = 0 → jointFirstMarginal p i = 0

theorem CommutingRepetition.ClassicalInformation.jointConditional_sum {ι : Type u_1} {κ : Type u_2} [Fintype κ] (joint : ι × κ → ℝ) (i : ι) (nonzero : jointFirstMarginal joint i ≠ 0) : ∑ j : κ, jointConditional joint i j = 1

theorem CommutingRepetition.ClassicalInformation.finite_relative_entropy_joint_chain_rule {ι : Type u_1} [Fintype ι] {κ : Type u_2} [Fintype κ] (p q : ι × κ → ℝ) (hp : ∀ (point : ι × κ), 0 ≤ p point) (hq : ∀ (point : ι × κ), 0 ≤ q point) (absolute_continuity : ∀ (point : ι × κ), q point = 0 → p point = 0) (hp_normalized : ∑ point : ι × κ, p point = 1) (hq_normalized : ∑ point : ι × κ, q point = 1) : Pinsker.finiteRelativeEntropy p q = Pinsker.finiteRelativeEntropy (jointFirstMarginal p) (jointFirstMarginal q) + ∑ i : ι, jointFirstMarginal p i * Pinsker.finiteRelativeEntropy (jointConditional p i) (jointConditional q i)

noncomputable def CommutingRepetition.ClassicalInformation.rationalPermutationOutput {ι : Type u_1} [Fintype ι] (denominator : ℕ) (numerator : ι → ℕ) (nonempty : (ClassicalSampling.rationalMarked denominator numerator).Nonempty) (permutation : Equiv.Perm (ι × Fin denominator)) : ι

Equations

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

theorem CommutingRepetition.ClassicalInformation.rationalPermutationOutput_probability {ι : Type u_1} [Fintype ι] [DecidableEq ι] (denominator : ℕ) (numerator : ι → ℕ) (normalized : ∑ i : ι, numerator i = denominator) (nonempty : (ClassicalSampling.rationalMarked denominator numerator).Nonempty) (letter : ι) : (ClassicalSampling.uniformPermutationProbability fun (permutation : Equiv.Perm (ι × Fin denominator)) => rationalPermutationOutput denominator numerator nonempty permutation = letter) = ↑(numerator letter) / ↑denominator

theorem CommutingRepetition.ClassicalInformation.rationalMarked_inter {ι : Type u_1} [Fintype ι] [DecidableEq ι] (denominator : ℕ) (left right : ι → ℕ) : ClassicalSampling.rationalMarked denominator left ∩ ClassicalSampling.rationalMarked denominator right = ClassicalSampling.rationalMarked denominator fun (i : ι) => min (left i) (right i)

theorem CommutingRepetition.ClassicalInformation.rationalMarked_inter_card {ι : Type u_1} [Fintype ι] [DecidableEq ι] (denominator : ℕ) (left right : ι → ℕ) (hleft : ∑ i : ι, left i = denominator) (_hright : ∑ i : ι, right i = denominator) : (ClassicalSampling.rationalMarked denominator left ∩ ClassicalSampling.rationalMarked denominator right).card = ∑ i : ι, min (left i) (right i)

theorem CommutingRepetition.ClassicalInformation.rationalMarked_markedTotalVariation_eq {ι : Type u_1} [Fintype ι] [DecidableEq ι] (denominator : ℕ) (positive : 0 < denominator) (left right : ι → ℕ) (hleft : ∑ i : ι, left i = denominator) (hright : ∑ i : ι, right i = denominator) : ClassicalSampling.markedTotalVariation (ClassicalSampling.rationalMarked denominator left) (ClassicalSampling.rationalMarked denominator right) = Pinsker.finiteTotalVariation (fun (i : ι) => ↑(left i) / ↑denominator) fun (i : ι) => ↑(right i) / ↑denominator

theorem CommutingRepetition.ClassicalInformation.uniformPermutationProbability_mono {α : Type u_2} [Fintype α] [DecidableEq α] (small large : Equiv.Perm α → Prop) (hinclusion : ∀ (permutation : Equiv.Perm α), small permutation → large permutation) : ClassicalSampling.uniformPermutationProbability small ≤ ClassicalSampling.uniformPermutationProbability large

theorem CommutingRepetition.ClassicalInformation.rationalPermutationOutput_disagreement_le_two_mul_tv {ι : Type u_1} [Fintype ι] [DecidableEq ι] (denominator : ℕ) (left right : ι → ℕ) (hleft : ∑ i : ι, left i = denominator) (hright : ∑ i : ι, right i = denominator) (nonempty_left : (ClassicalSampling.rationalMarked denominator left).Nonempty) (nonempty_right : (ClassicalSampling.rationalMarked denominator right).Nonempty) : (ClassicalSampling.uniformPermutationProbability fun (permutation : Equiv.Perm (ι × Fin denominator)) => rationalPermutationOutput denominator left nonempty_left permutation ≠ rationalPermutationOutput denominator right nonempty_right permutation) ≤ 2 * ClassicalSampling.markedTotalVariation (ClassicalSampling.rationalMarked denominator left) (ClassicalSampling.rationalMarked denominator right)

theorem CommutingRepetition.ClassicalInformation.rationalPermutationOutput_disagreement_le_two_mul_finiteTotalVariation {ι : Type u_1} [Fintype ι] [DecidableEq ι] (denominator : ℕ) (positive : 0 < denominator) (left right : ι → ℕ) (hleft : ∑ i : ι, left i = denominator) (hright : ∑ i : ι, right i = denominator) (nonempty_left : (ClassicalSampling.rationalMarked denominator left).Nonempty) (nonempty_right : (ClassicalSampling.rationalMarked denominator right).Nonempty) : (ClassicalSampling.uniformPermutationProbability fun (permutation : Equiv.Perm (ι × Fin denominator)) => rationalPermutationOutput denominator left nonempty_left permutation ≠ rationalPermutationOutput denominator right nonempty_right permutation) ≤ 2 * Pinsker.finiteTotalVariation (fun (i : ι) => ↑(left i) / ↑denominator) fun (i : ι) => ↑(right i) / ↑denominator

noncomputable def CommutingRepetition.ClassicalInformation.finiteHellingerSq {ι : Type u_1} [Fintype ι] (p q : ι → ℝ) : ℝ

Squared Hellinger distance between two finitely supported densities, H²(P, Q) = ∑ ω, (√(P ω) − √(Q ω))² (manuscript, Preliminaries).

Equations

• CommutingRepetition.ClassicalInformation.finiteHellingerSq p q = ∑ i : ι, (√(p i) - √(q i)) ^ 2

theorem CommutingRepetition.ClassicalInformation.finiteHellingerSq_nonneg {ι : Type u_1} [Fintype ι] (p q : ι → ℝ) : 0 ≤ finiteHellingerSq p q

theorem CommutingRepetition.ClassicalInformation.sub_one_le_mul_log {u : ℝ} (hu : 0 ≤ u) : u - 1 ≤ u * Real.log u

theorem CommutingRepetition.ClassicalInformation.sqrt_sub_one_sq_le_klFun {t : ℝ} (ht : 0 ≤ t) : (√t - 1) ^ 2 ≤ InformationTheory.klFun t

theorem CommutingRepetition.ClassicalInformation.hellinger_density_le_weighted_kl {p q : ℝ} (hp : 0 ≤ p) (hq : 0 < q) : (√p - √q) ^ 2 ≤ q * InformationTheory.klFun (p / q)

theorem CommutingRepetition.ClassicalInformation.finiteHellingerSq_le_relative_entropy {ι : Type u_1} [Fintype ι] (p q : ι → ℝ) (hp : ∀ (i : ι), 0 ≤ p i) (hq : ∀ (i : ι), 0 ≤ q i) (absolute_continuity : ∀ (i : ι), q i = 0 → p i = 0) : finiteHellingerSq p q ≤ ∑ i : ι, q i * InformationTheory.klFun (p i / q i)

Hellinger–relative-entropy bound H²(P, Q) ≤ D(P ‖ Q) (manuscript, Preliminaries), with the relative entropy in mass-weighted klFun form.

theorem CommutingRepetition.ClassicalInformation.finiteTotalVariation_le_hellinger {ι : Type u_1} [Fintype ι] (p q : ι → ℝ) (hp : ∀ (i : ι), 0 ≤ p i) (hq : ∀ (i : ι), 0 ≤ q i) (hp_normalized : ∑ i : ι, p i = 1) (hq_normalized : ∑ i : ι, q i = 1) : Pinsker.finiteTotalVariation p q ≤ √(finiteHellingerSq p q)

Total-variation–Hellinger bound: the manuscript display is ‖P − Q‖₁ ≤ 2 H(P, Q); since finiteTotalVariation is the halved ℓ¹ distance (∑ i, |p i − q i|) / 2, the exact-constant form is finiteTotalVariation p q ≤ √(finiteHellingerSq p q).