Optimization.lean`

5 declarations, 0 contain sorry, 0 declared as axioms

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 OAI.MatrixMultiplication.AuxiliarySeparation.binary_entropy_log_partition line 23

Source documentation

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

theorem 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) := by
…

theorem OAI.MatrixMultiplication.AuxiliarySeparation.binary_entropy_variational_identity line 37

Source documentation

Entropy compensates the weighted geometric mean at the normalized weights.

theorem 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 := by
…

theorem OAI.MatrixMultiplication.AuxiliarySeparation.binary_entropy_variational_identity_of_ratio line 45

Source documentation

The identity with an explicitly named optimizing proportion.

theorem 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 := by
…

theorem OAI.MatrixMultiplication.AuxiliarySeparation.finite_entropy_log_partition line 60

Source documentation

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

theorem finite_entropy_log_partition {ι : Type*} (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) := by
…

theorem OAI.MatrixMultiplication.AuxiliarySeparation.finite_entropy_variational_identity line 78

Source documentation

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

theorem finite_entropy_variational_identity {ι : Type*} (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 := by
…