theorem CommutingRepetition.HistoryKL.finiteRelativeEntropy_le_log_sum {ι : Type u_1} [Fintype ι] (p q : ι → ℝ) (hp : ∀ (i : ι), 0 ≤ p i) (hq : ∀ (i : ι), 0 ≤ q i) (habs : ∀ (i : ι), q i = 0 → p i = 0) (hp1 : ∑ i : ι, p i = 1) (hq1 : ∑ i : ι, q i ≤ 1) : Pinsker.finiteRelativeEntropy p q ≤ ∑ i : ι, p i * Real.log (p i / q i)

Log-sum upper bound. Against a nonnegative, subnormalized, absolutely continuous reference, the finite relative entropy is at most the log-sum ∑ p log(p/q) (equality when the reference is normalized).

theorem CommutingRepetition.HistoryKL.sum_mul_log_le_log_of_le {ι : Type u_1} [Fintype ι] (q P : ι → ℝ) {K : ℝ} (hK : 0 < K) (hq : ∀ (i : ι), 0 ≤ q i) (hqK : ∀ (i : ι), q i ≤ K * P i) (hq1 : ∑ i : ι, q i = 1) : ∑ i : ι, q i * Real.log (q i / P i) ≤ Real.log K

Pointwise-density bound: if q ≤ K·P pointwise then ∑ q log(q/P) ≤ log K.

theorem CommutingRepetition.HistoryKL.neg_log_sum_le_sum_mul_log {ι : Type u_1} [Fintype ι] (q P : ι → ℝ) (hq : ∀ (i : ι), 0 ≤ q i) (hP : ∀ (i : ι), 0 ≤ P i) (habs : ∀ (i : ι), P i = 0 → q i = 0) (hq1 : ∑ i : ι, q i = 1) (hT : 0 < ∑ i : ι, P i) : -Real.log (∑ i : ι, P i) ≤ ∑ i : ι, q i * Real.log (q i / P i)

Gibbs lower bound against an unnormalized nonnegative reference of total mass T: ∑ q log(q/P) ≥ −log T.

theorem CommutingRepetition.HistoryKL.groupedMass_eq_sum_ite {ι : Type u_1} {κ : Type u_2} [Fintype ι] [DecidableEq κ] [DecidableEq ι] (f : ι → κ) (p : ι → ℝ) (j : κ) : ClassicalInformation.groupedMass f p j = ∑ i : ι, if f i = j then p i else 0

The grouped mass as an indicator sum.

theorem CommutingRepetition.HistoryKL.sum_groupedMass_mul {ι : Type u_1} {κ : Type u_2} [Fintype ι] [Fintype κ] [DecidableEq κ] [DecidableEq ι] (f : ι → κ) (p : ι → ℝ) (φ : κ → ℝ) : ∑ j : κ, ClassicalInformation.groupedMass f p j * φ j = ∑ i : ι, p i * φ (f i)

Pushforward identity: an expectation of a function of the grouped variable is the expectation of its composite.

theorem CommutingRepetition.HistoryKL.sum_groupedMass {ι : Type u_1} {κ : Type u_2} [Fintype ι] [Fintype κ] [DecidableEq κ] [DecidableEq ι] (f : ι → κ) (p : ι → ℝ) : ∑ j : κ, ClassicalInformation.groupedMass f p j = ∑ i : ι, p i

theorem CommutingRepetition.HistoryKL.groupedMass_nonneg {ι : Type u_1} {κ : Type u_2} [Fintype ι] [DecidableEq κ] [DecidableEq ι] (f : ι → κ) (p : ι → ℝ) (hp : ∀ (i : ι), 0 ≤ p i) (j : κ) : 0 ≤ ClassicalInformation.groupedMass f p j

theorem CommutingRepetition.HistoryKL.groupedMass_le_mul {ι : Type u_1} {κ : Type u_2} [Fintype ι] [Fintype κ] [DecidableEq κ] [DecidableEq ι] (f : ι → κ) (p P : ι → ℝ) (K : ℝ) (h : ∀ (i : ι), p i ≤ K * P i) (j : κ) : ClassicalInformation.groupedMass f p j ≤ K * ClassicalInformation.groupedMass f P j

theorem CommutingRepetition.HistoryKL.sum_mul_class_eq {ι : Type u_1} {κ : Type u_2} [Fintype ι] [Fintype κ] [DecidableEq κ] [DecidableEq ι] (c : ι → κ) (q : ι → ℝ) (ψ : κ → ℝ) : ∑ i : ι, q i * ψ (c i) = ∑ u : κ, ClassicalInformation.groupedMass c q u * ψ u

The summand of a class-function expectation depends on the class only.

theorem CommutingRepetition.HistoryKL.sum_mul_log_class_le {ι : Type u_1} {κ : Type u_2} [Fintype ι] [Fintype κ] [DecidableEq κ] [DecidableEq ι] (c : ι → κ) (q P : ι → ℝ) {K : ℝ} (hK : 0 < K) (hq : ∀ (i : ι), 0 ≤ q i) (hqK : ∀ (i : ι), q i ≤ K * P i) (hq1 : ∑ i : ι, q i = 1) : ∑ i : ι, q i * Real.log ((∑ i' : ι, if c i' = c i then q i' else 0) / ∑ i' : ι, if c i' = c i then P i' else 0) ≤ Real.log K

Pointwise-density bound, class form: the expected log-ratio of the class masses of q and P is at most log K when q ≤ K·P.

theorem CommutingRepetition.HistoryKL.neg_log_le_sum_mul_log_class {ι : Type u_1} {κ : Type u_2} [Fintype ι] [Fintype κ] [DecidableEq κ] [DecidableEq ι] (c : ι → κ) (q P : ι → ℝ) (hq : ∀ (i : ι), 0 ≤ q i) (hP : ∀ (i : ι), 0 ≤ P i) (habs : ∀ (i : ι), P i = 0 → q i = 0) (hq1 : ∑ i : ι, q i = 1) (hT : 0 < ∑ i : ι, P i) : -Real.log (∑ i : ι, P i) ≤ ∑ i : ι, q i * Real.log ((∑ i' : ι, if c i' = c i then q i' else 0) / ∑ i' : ι, if c i' = c i then P i' else 0)

Gibbs lower bound, class form.

noncomputable def CommutingRepetition.HistoryKL.coordMarginal {ι : Type u_1} [Fintype ι] {α : Type u_3} [Fintype α] [DecidableEq α] [DecidableEq ι] (q : (ι → α) → ℝ) (j : ι) (x : α) : ℝ

The j-th coordinate marginal of a law on words.

Equations

• CommutingRepetition.HistoryKL.coordMarginal q j x = ∑ w : ι → α, if w j = x then q w else 0

theorem CommutingRepetition.HistoryKL.coordMarginal_nonneg {ι : Type u_1} [Fintype ι] {α : Type u_3} [Fintype α] [DecidableEq α] [DecidableEq ι] (q : (ι → α) → ℝ) (hq : ∀ (w : ι → α), 0 ≤ q w) (j : ι) (x : α) : 0 ≤ coordMarginal q j x

theorem CommutingRepetition.HistoryKL.le_coordMarginal {ι : Type u_1} [Fintype ι] {α : Type u_3} [Fintype α] [DecidableEq α] [DecidableEq ι] (q : (ι → α) → ℝ) (hq : ∀ (w : ι → α), 0 ≤ q w) (j : ι) (w : ι → α) : q w ≤ coordMarginal q j (w j)

theorem CommutingRepetition.HistoryKL.sum_coordMarginal {ι : Type u_1} [Fintype ι] {α : Type u_3} [Fintype α] [DecidableEq α] [DecidableEq ι] (q : (ι → α) → ℝ) (j : ι) : ∑ x : α, coordMarginal q j x = ∑ w : ι → α, q w

theorem CommutingRepetition.HistoryKL.sum_prod_coordMarginal {ι : Type u_1} [Fintype ι] {α : Type u_3} [Fintype α] [DecidableEq α] [DecidableEq ι] (q : (ι → α) → ℝ) (hq1 : ∑ w : ι → α, q w = 1) : ∑ w : ι → α, ∏ j : ι, coordMarginal q j (w j) = 1

The product of the coordinate marginals is a probability law.

theorem CommutingRepetition.HistoryKL.sum_coordMarginal_log_le {ι : Type u_1} [Fintype ι] {α : Type u_3} [Fintype α] [DecidableEq α] [DecidableEq ι] (q : (ι → α) → ℝ) (ν : α → ℝ) {K : ℝ} (hK : 0 < K) (hq : ∀ (w : ι → α), 0 ≤ q w) (hq1 : ∑ w : ι → α, q w = 1) (hν : ∀ (x : α), 0 ≤ ν x) (hqK : ∀ (w : ι → α), q w ≤ K * ∏ j : ι, ν (w j)) : ∑ j : ι, ∑ x : α, coordMarginal q j x * Real.log (coordMarginal q j x / ν x) ≤ Real.log K

Tensorization: for a law on words dominated by K times a product reference, the coordinate marginals' log-sums against the factor total at most log K — ∑_j D(q_j ‖ ν) ≤ D(q ‖ ν^{⊗}) ≤ log K (eq first-history-chain-term).