Finite entropy, rate estimates and ordered asymptotic limits.

noncomputable def MatrixMultiplicationAllFields.MatrixMultiplication.Foundation.entropyTerm (p : ℝ) : ℝ

The contribution of one mass to Shannon entropy, using natural logarithms.

Equations

• MatrixMultiplicationAllFields.MatrixMultiplication.Foundation.entropyTerm p = -p * Real.log p

noncomputable def MatrixMultiplicationAllFields.MatrixMultiplication.Foundation.finiteEntropy {A : Type u_1} [Fintype A] (p : A → ℝ) : ℝ

Shannon entropy of a finite mass function, using natural logarithms.

Equations

• MatrixMultiplicationAllFields.MatrixMultiplication.Foundation.finiteEntropy p = ∑ a : A, MatrixMultiplicationAllFields.MatrixMultiplication.Foundation.entropyTerm (p a)

theorem MatrixMultiplicationAllFields.MatrixMultiplication.Foundation.finiteEntropy_equiv {A : Type u_1} {B : Type u_2} [Fintype A] [Fintype B] (e : A ≃ B) (p : B → ℝ) : (finiteEntropy fun (a : A) => p (e a)) = finiteEntropy p

@[simp]

theorem MatrixMultiplicationAllFields.MatrixMultiplication.Foundation.entropyTerm_zero : entropyTerm 0 = 0

theorem MatrixMultiplicationAllFields.MatrixMultiplication.Foundation.entropyTerm_mul (p q : ℝ) : entropyTerm (p * q) = q * entropyTerm p + p * entropyTerm q

theorem MatrixMultiplicationAllFields.MatrixMultiplication.Foundation.finiteEntropy_chain {A : Type u_1} {B : Type u_2} [Fintype A] [Fintype B] (p : A → ℝ) (q : A → B → ℝ) (hq : ∀ (a : A), ∑ b : B, q a b = 1) : (finiteEntropy fun (ab : A × B) => p ab.1 * q ab.1 ab.2) = finiteEntropy p + ∑ a : A, p a * finiteEntropy (q a)

structure MatrixMultiplicationAllFields.MatrixMultiplication.Foundation.FiniteLaw (A : Type u_1) [Fintype A] : Type u_1

A nonnegative probability mass function on a finite type.

• mass : A → ℝ

  Probability mass assigned to each point.

• nonneg (a : A) : 0 ≤ self.mass a
• total : ∑ a : A, self.mass a = 1

noncomputable def MatrixMultiplicationAllFields.MatrixMultiplication.Foundation.FiniteLaw.map {A : Type u_1} {B : Type u_2} [Fintype A] [Fintype B] (p : FiniteLaw A) (f : A → B) : FiniteLaw B

Push a finite probability law forward along a map.

Equations

• p.map f = { mass := fun (b : B) => ∑ a : A, if f a = b then p.mass a else 0, nonneg := ⋯, total := ⋯ }

@[simp]

theorem MatrixMultiplicationAllFields.MatrixMultiplication.Foundation.FiniteLaw.map_mass {A : Type u_1} {B : Type u_2} [Fintype A] [Fintype B] [DecidableEq B] (p : FiniteLaw A) (f : A → B) (b : B) : (p.map f).mass b = ∑ a : A, if f a = b then p.mass a else 0

theorem MatrixMultiplicationAllFields.MatrixMultiplication.Foundation.FiniteLaw.map_mass_apply {A : Type u_1} {B : Type u_2} [Fintype A] [Fintype B] (p : FiniteLaw A) (f : A → B) (hf : Function.Injective f) (a : A) : (p.map f).mass (f a) = p.mass a

theorem MatrixMultiplicationAllFields.MatrixMultiplication.Foundation.FiniteLaw.map_entropy_of_injective {A : Type u_1} {B : Type u_2} [Fintype A] [Fintype B] (p : FiniteLaw A) (f : A → B) (hf : Function.Injective f) : finiteEntropy (p.map f).mass = finiteEntropy p.mass

def MatrixMultiplicationAllFields.MatrixMultiplication.Foundation.FiniteLaw.joint {A : Type u_1} {B : Type u_2} [Fintype A] [Fintype B] (p : FiniteLaw A) (q : A → FiniteLaw B) : FiniteLaw (A × B)

The joint law obtained by sampling a point and then its conditional law.

Equations

• p.joint q = { mass := fun (ab : A × B) => p.mass ab.1 * (q ab.1).mass ab.2, nonneg := ⋯, total := ⋯ }

theorem MatrixMultiplicationAllFields.MatrixMultiplication.Foundation.FiniteLaw.joint_entropy {A : Type u_1} {B : Type u_2} [Fintype A] [Fintype B] (p : FiniteLaw A) (q : A → FiniteLaw B) : finiteEntropy (p.joint q).mass = finiteEntropy p.mass + ∑ a : A, p.mass a * finiteEntropy (q a).mass

theorem MatrixMultiplicationAllFields.MatrixMultiplication.Foundation.FiniteLaw.mass_le_map_mass {A : Type u_1} {B : Type u_2} [Fintype A] [Fintype B] (p : FiniteLaw A) (f : A → B) (a : A) : p.mass a ≤ (p.map f).mass (f a)

noncomputable def MatrixMultiplicationAllFields.MatrixMultiplication.Foundation.FiniteLaw.conditional {A : Type u_1} {B : Type u_2} [Fintype A] [Fintype B] (p : FiniteLaw A) (f : A → B) (b : B) : FiniteLaw A

Condition on a fiber, retaining the original law when that fiber has zero mass.

Equations

• p.conditional f b = if hzero : (p.map f).mass b = 0 then p else { mass := fun (a : A) => (if f a = b then p.mass a else 0) / (p.map f).mass b, nonneg := ⋯, total := ⋯ }

theorem MatrixMultiplicationAllFields.MatrixMultiplication.Foundation.FiniteLaw.map_mass_mul_conditional {A : Type u_1} {B : Type u_2} [Fintype A] [Fintype B] [DecidableEq B] (p : FiniteLaw A) (f : A → B) (b : B) (a : A) : (p.map f).mass b * (p.conditional f b).mass a = if f a = b then p.mass a else 0

theorem MatrixMultiplicationAllFields.MatrixMultiplication.Foundation.FiniteLaw.entropy_eq_map_add_conditional {A : Type u_1} {B : Type u_2} [Fintype A] [Fintype B] (p : FiniteLaw A) (f : A → B) : finiteEntropy p.mass = finiteEntropy (p.map f).mass + ∑ b : B, (p.map f).mass b * finiteEntropy (p.conditional f b).mass