theorem CommutingRepetition.negMulLog_rescale {W p : ℝ} (hW : 0 < W) (hp : 0 < p) : W * (p / W).negMulLog = p * Real.log (W / p)

theorem CommutingRepetition.finite_weighted_entropy_le {ι : Type u_1} (s : Finset ι) (w h : ι → ℝ) {W p : ℝ} (hw : ∀ i ∈ s, 0 ≤ w i) (hh : ∀ i ∈ s, 0 ≤ h i) (hW : 0 < W) (hp : 0 < p) (hw_sum : ∑ i ∈ s, w i = W) (hp_sum : ∑ i ∈ s, w i * h i = p) : ∑ i ∈ s, w i * (h i).negMulLog ≤ p * Real.log (W / p)

theorem CommutingRepetition.finite_weighted_entropy_le_of_weight_bound {ι : Type u_1} (s : Finset ι) (w h : ι → ℝ) {W N p : ℝ} (hw : ∀ i ∈ s, 0 ≤ w i) (hh : ∀ i ∈ s, 0 ≤ h i) (hW : 0 < W) (hp : 0 < p) (hw_sum : ∑ i ∈ s, w i = W) (hp_sum : ∑ i ∈ s, w i * h i = p) (hWN : W ≤ N) : ∑ i ∈ s, w i * (h i).negMulLog ≤ p * Real.log (N / p)

theorem CommutingRepetition.noncommutative_resolvent_identity {R : Type u_1} [Ring R] (F M S RF RM : R) (hF : RF * (F + S) = 1) (hM : (M + S) * RM = 1) : RF - RM = RF * (M - F) * RM

theorem CommutingRepetition.noncommutative_filtered_resolvent_identity {R : Type u_1} [Ring R] (F M S RF RM : R) (hF_left : (F + S) * RF = 1) (hF_right : RF * (F + S) = 1) (hM_left : (M + S) * RM = 1) : F * RF - M * RM = S * (RF * (F - M) * RM)

theorem CommutingRepetition.noncommutative_resolvent_second_order {R : Type u_1} [Ring R] (F M S RF RM : R) (hF_left : (F + S) * RF = 1) (hF_right : RF * (F + S) = 1) (hM_left : (M + S) * RM = 1) (hM_right : RM * (M + S) = 1) : RF = RM - RM * (F - M) * RM + RM * (F - M) * RF * (F - M) * RM

theorem CommutingRepetition.noncommutative_weighted_resolvent_second_order {ι : Type u_1} {R : Type u_2} [Fintype ι] [Ring R] (weight F : ι → R) (M S : R) (RF : ι → R) (RM : R) (normalized : ∑ i : ι, weight i = 1) (centered : ∑ i : ι, weight i * (F i - M) = 0) (commute_mean : ∀ (i : ι), weight i * RM = RM * weight i) (hF_left : ∀ (i : ι), (F i + S) * RF i = 1) (hF_right : ∀ (i : ι), RF i * (F i + S) = 1) (hM_left : (M + S) * RM = 1) (hM_right : RM * (M + S) = 1) : ∑ i : ι, weight i * RF i - RM = (RM * ∑ i : ι, weight i * ((F i - M) * RF i * (F i - M))) * RM

theorem CommutingRepetition.Pinsker.centered_log_lower_of_one_le {x : ℝ} (hx : 1 ≤ x) : 2 * (x - 1) / (x + 1) ≤ Real.log x

theorem CommutingRepetition.Pinsker.centered_log_upper_of_le_one {x : ℝ} (hx0 : 0 < x) (hx1 : x ≤ 1) : Real.log x ≤ 2 * (x - 1) / (x + 1)

noncomputable def CommutingRepetition.Pinsker.pinskerScalarGap (x : ℝ) : ℝ

Equations

• CommutingRepetition.Pinsker.pinskerScalarGap x = InformationTheory.klFun x - 3 * (x - 1) ^ 2 / (2 * (x + 2))

theorem CommutingRepetition.Pinsker.hasDerivAt_pinskerScalarGap {x : ℝ} (hx : 0 < x) : HasDerivAt pinskerScalarGap (Real.log x - 3 * (x - 1) * (x + 5) / (2 * (x + 2) ^ 2)) x

theorem CommutingRepetition.Pinsker.pinsker_rational_coefficient_le {x : ℝ} (hx : 0 < x) : 3 * (x + 5) / (2 * (x + 2) ^ 2) ≤ 2 / (x + 1)

theorem CommutingRepetition.Pinsker.pinskerScalarGap_derivative_nonneg {x : ℝ} (hx : 1 ≤ x) : 0 ≤ Real.log x - 3 * (x - 1) * (x + 5) / (2 * (x + 2) ^ 2)

theorem CommutingRepetition.Pinsker.pinskerScalarGap_derivative_nonpos {x : ℝ} (hx0 : 0 < x) (hx1 : x ≤ 1) : Real.log x - 3 * (x - 1) * (x + 5) / (2 * (x + 2) ^ 2) ≤ 0

theorem CommutingRepetition.Pinsker.pinskerScalarGap_nonneg {x : ℝ} (hx : 0 ≤ x) : 0 ≤ pinskerScalarGap x

theorem CommutingRepetition.Pinsker.quadratic_le_klFun {x : ℝ} (hx : 0 ≤ x) : 3 * (x - 1) ^ 2 / (2 * (x + 2)) ≤ InformationTheory.klFun x

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

Equations

• CommutingRepetition.Pinsker.finiteRelativeEntropy p q = ∑ i : ι, q i * InformationTheory.klFun (p i / q i)

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

Equations

• CommutingRepetition.Pinsker.finiteTotalVariation p q = (∑ i : ι, |p i - q i|) / 2

theorem CommutingRepetition.Pinsker.quadratic_density_le_weighted_kl {p q : ℝ} (hp : 0 ≤ p) (hq : 0 < q) : 3 * (p - q) ^ 2 / (2 * (p + 2 * q)) ≤ q * InformationTheory.klFun (p / q)

theorem CommutingRepetition.Pinsker.finiteRelativeEntropy_eq_log_sum {ι : Type u_1} [Fintype ι] (p q : ι → ℝ) (hq : ∀ (i : ι), 0 < q i) (hp_normalized : ∑ i : ι, p i = 1) (hq_normalized : ∑ i : ι, q i = 1) : finiteRelativeEntropy p q = ∑ i : ι, p i * Real.log (p i / q i)

theorem CommutingRepetition.Pinsker.finite_pinsker {ι : 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) : 2 * finiteTotalVariation p q ^ 2 ≤ finiteRelativeEntropy p q

theorem CommutingRepetition.Pinsker.sum_over_positive_reference_support {ι : Type u_1} [Fintype ι] (q f : ι → ℝ) (hq : ∀ (i : ι), 0 ≤ q i) (hzero : ∀ (i : ι), q i = 0 → f i = 0) : ∑ i : { i : ι // 0 < q i }, f ↑i = ∑ i : ι, f i

theorem CommutingRepetition.Pinsker.finite_pinsker_of_absolute_continuity {ι : 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) (hp_normalized : ∑ i : ι, p i = 1) (hq_normalized : ∑ i : ι, q i = 1) : 2 * finiteTotalVariation p q ^ 2 ≤ finiteRelativeEntropy p q

theorem CommutingRepetition.Pinsker.finiteRelativeEntropy_eq_log_sum_of_absolute_continuity {ι : Type u_1} [Fintype ι] (p q : ι → ℝ) (hq : ∀ (i : ι), 0 ≤ q i) (absolute_continuity : ∀ (i : ι), q i = 0 → p i = 0) (hp_normalized : ∑ i : ι, p i = 1) (hq_normalized : ∑ i : ι, q i = 1) : finiteRelativeEntropy p q = ∑ i : ι, p i * Real.log (p i / q i)

theorem CommutingRepetition.Pinsker.finite_pinsker_sqrt_of_absolute_continuity {ι : 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) (hp_normalized : ∑ i : ι, p i = 1) (hq_normalized : ∑ i : ι, q i = 1) : finiteTotalVariation p q ≤ √(finiteRelativeEntropy p q / 2)