Entropy optimization for finitely many sectors

The normalized weights q = A / (A + B) and 1 - q = B / (A + B) make the entropy-weighted geometric mean equal to A + B. This is the scalar identity used in Section 5.1 of the auxiliary-separation argument. The same calculation also applies to an arbitrary nonempty finite family.

theorem MatrixMultiplicationAllFields.MatrixMultiplication.AuxiliarySeparation.binary_entropy_log_partition {A B : ℝ} (hA : 0 < A) (hB : 0 < B) : Real.binEntropy (A / (A + B)) + Real.log A * (A / (A + B)) + Real.log B * (1 - A / (A + B)) = Real.log (A + B)

The logarithmic form of the entropy identity at the normalized weights.

theorem MatrixMultiplicationAllFields.MatrixMultiplication.AuxiliarySeparation.binary_entropy_variational_identity {A B : ℝ} (hA : 0 < A) (hB : 0 < B) : Real.exp (Real.binEntropy (A / (A + B))) * A ^ (A / (A + B)) * B ^ (1 - A / (A + B)) = A + B

Entropy compensates the weighted geometric mean at the normalized weights.

theorem MatrixMultiplicationAllFields.MatrixMultiplication.AuxiliarySeparation.binary_entropy_variational_identity_of_ratio {A B q : ℝ} (hA : 0 < A) (hB : 0 < B) (hq : q = A / (A + B)) : Real.exp (-q * Real.log q - (1 - q) * Real.log (1 - q)) * A ^ q * B ^ (1 - q) = A + B

The identity with an explicitly named optimizing proportion.

theorem MatrixMultiplicationAllFields.MatrixMultiplication.AuxiliarySeparation.finite_entropy_log_partition {ι : Type u_1} (s : Finset ι) (A : ι → ℝ) (hs : s.Nonempty) (hA : ∀ i ∈ s, 0 < A i) : -∑ i ∈ s, (A i / ∑ j ∈ s, A j) * Real.log (A i / ∑ j ∈ s, A j) + ∑ i ∈ s, Real.log (A i) * (A i / ∑ j ∈ s, A j) = Real.log (∑ j ∈ s, A j)

The logarithmic entropy identity for positive weights on a finite set.

theorem MatrixMultiplicationAllFields.MatrixMultiplication.AuxiliarySeparation.finite_entropy_variational_identity {ι : Type u_1} (s : Finset ι) (A : ι → ℝ) (hs : s.Nonempty) (hA : ∀ i ∈ s, 0 < A i) : Real.exp (-∑ i ∈ s, (A i / ∑ j ∈ s, A j) * Real.log (A i / ∑ j ∈ s, A j)) * ∏ i ∈ s, A i ^ (A i / ∑ j ∈ s, A j) = ∑ j ∈ s, A j

Normalizing any positive finite family attains its sum in the entropy formula.