Finite entropy, rate estimates and ordered asymptotic limits.

theorem MatrixMultiplicationAllFields.MatrixMultiplication.Foundation.entropyTerm_eq_negMulLog (p : ℝ) : entropyTerm p = p.negMulLog

@[simp]

theorem MatrixMultiplicationAllFields.MatrixMultiplication.Foundation.entropyTerm_one : entropyTerm 1 = 0

theorem MatrixMultiplicationAllFields.MatrixMultiplication.Foundation.mul_entropyTerm_inv (x : ℝ) : x * entropyTerm x⁻¹ = Real.log x

theorem MatrixMultiplicationAllFields.MatrixMultiplication.Foundation.finiteEntropy_uniform {A : Type u_1} [Fintype A] : (finiteEntropy fun (_a : A) => (↑(Fintype.card A))⁻¹) = Real.log ↑(Fintype.card A)

theorem MatrixMultiplicationAllFields.MatrixMultiplication.Foundation.finiteEntropy_deterministic {A : Type u_1} [Fintype A] [DecidableEq A] (a : A) : (finiteEntropy fun (b : A) => if b = a then 1 else 0) = 0

theorem MatrixMultiplicationAllFields.MatrixMultiplication.Foundation.continuous_entropyTerm : Continuous entropyTerm

theorem MatrixMultiplicationAllFields.MatrixMultiplication.Foundation.entropyTerm_nonneg {p : ℝ} (hp₀ : 0 ≤ p) (hp₁ : p ≤ 1) : 0 ≤ entropyTerm p

theorem MatrixMultiplicationAllFields.MatrixMultiplication.Foundation.concaveOn_entropyTerm : ConcaveOn ℝ (Set.Ici 0) entropyTerm

theorem MatrixMultiplicationAllFields.MatrixMultiplication.Foundation.continuous_finiteEntropy {A : Type u_1} [Fintype A] : Continuous finiteEntropy

theorem MatrixMultiplicationAllFields.MatrixMultiplication.Foundation.tendsto_entropyTerm {I : Type u_1} {l : Filter I} {p : I → ℝ} {q : ℝ} (h : Filter.Tendsto p l (nhds q)) : Filter.Tendsto (fun (i : I) => entropyTerm (p i)) l (nhds (entropyTerm q))

theorem MatrixMultiplicationAllFields.MatrixMultiplication.Foundation.tendsto_entropyTerm_zero {I : Type u_1} {l : Filter I} {p : I → ℝ} (h : Filter.Tendsto p l (nhds 0)) : Filter.Tendsto (fun (i : I) => entropyTerm (p i)) l (nhds 0)

theorem MatrixMultiplicationAllFields.MatrixMultiplication.Foundation.tendsto_finiteEntropy_of_tendsto {I : Type u_1} {A : Type u_2} [Fintype A] {l : Filter I} {p : I → A → ℝ} {q : A → ℝ} (h : ∀ (a : A), Filter.Tendsto (fun (i : I) => p i a) l (nhds (q a))) : Filter.Tendsto (fun (i : I) => finiteEntropy (p i)) l (nhds (finiteEntropy q))

theorem MatrixMultiplicationAllFields.MatrixMultiplication.Foundation.finiteEntropy_nonneg {A : Type u_1} [Fintype A] (p : A → ℝ) (hp₀ : ∀ (a : A), 0 ≤ p a) (hp₁ : ∀ (a : A), p a ≤ 1) : 0 ≤ finiteEntropy p

theorem MatrixMultiplicationAllFields.MatrixMultiplication.Foundation.finiteEntropy_mix_le {A : Type u_1} [Fintype A] (p q : A → ℝ) (hp : ∀ (i : A), 0 ≤ p i) (hq : ∀ (i : A), 0 ≤ q i) {a b : ℝ} (ha : 0 ≤ a) (hb : 0 ≤ b) (hab : a + b = 1) : a * finiteEntropy p + b * finiteEntropy q ≤ finiteEntropy fun (i : A) => a * p i + b * q i

theorem MatrixMultiplicationAllFields.MatrixMultiplication.Foundation.finiteEntropy_le_log_card {A : Type u_1} [Fintype A] (p : A → ℝ) (hp : ∀ (a : A), 0 ≤ p a) (htotal : ∑ a : A, p a = 1) : finiteEntropy p ≤ Real.log ↑(Fintype.card A)

noncomputable def MatrixMultiplicationAllFields.MatrixMultiplication.Foundation.FiniteLaw.uniform (A : Type u_2) [Fintype A] [Nonempty A] : FiniteLaw A

The probability law assigning equal mass to every point of a nonempty finite type.

Equations

• MatrixMultiplicationAllFields.MatrixMultiplication.Foundation.FiniteLaw.uniform A = { mass := fun (_a : A) => (↑(Fintype.card A))⁻¹, nonneg := ⋯, total := ⋯ }

@[simp]

theorem MatrixMultiplicationAllFields.MatrixMultiplication.Foundation.FiniteLaw.uniform_mass {A : Type u_1} [Fintype A] [Nonempty A] (a : A) : (uniform A).mass a = (↑(Fintype.card A))⁻¹

@[simp]

theorem MatrixMultiplicationAllFields.MatrixMultiplication.Foundation.FiniteLaw.uniform_entropy {A : Type u_1} [Fintype A] [Nonempty A] : finiteEntropy (uniform A).mass = Real.log ↑(Fintype.card A)

noncomputable def MatrixMultiplicationAllFields.MatrixMultiplication.Foundation.FiniteLaw.pure {A : Type u_1} [Fintype A] (a : A) : FiniteLaw A

The probability law concentrated at one point.

Equations

• MatrixMultiplicationAllFields.MatrixMultiplication.Foundation.FiniteLaw.pure a = { mass := fun (b : A) => if b = a then 1 else 0, nonneg := ⋯, total := ⋯ }

@[simp]

theorem MatrixMultiplicationAllFields.MatrixMultiplication.Foundation.FiniteLaw.pure_entropy {A : Type u_1} [Fintype A] (a : A) : finiteEntropy (pure a).mass = 0

theorem MatrixMultiplicationAllFields.MatrixMultiplication.Foundation.FiniteLaw.mass_le_one {A : Type u_1} [Fintype A] (p : FiniteLaw A) (a : A) : p.mass a ≤ 1

theorem MatrixMultiplicationAllFields.MatrixMultiplication.Foundation.FiniteLaw.entropy_nonneg {A : Type u_1} [Fintype A] (p : FiniteLaw A) : 0 ≤ finiteEntropy p.mass

theorem MatrixMultiplicationAllFields.MatrixMultiplication.Foundation.FiniteLaw.entropy_le_log_card {A : Type u_1} [Fintype A] (p : FiniteLaw A) : finiteEntropy p.mass ≤ Real.log ↑(Fintype.card A)

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

theorem MatrixMultiplicationAllFields.MatrixMultiplication.Foundation.FiniteLaw.entropy_tendsto {A : Type u_1} [Fintype A] {I : Type u_2} {l : Filter I} {p : I → FiniteLaw A} {q : FiniteLaw A} (h : ∀ (a : A), Filter.Tendsto (fun (i : I) => (p i).mass a) l (nhds (q.mass a))) : Filter.Tendsto (fun (i : I) => finiteEntropy (p i).mass) l (nhds (finiteEntropy q.mass))