Optimizer.lean`

10 declarations, 0 contain sorry, 0 declared as axioms

Support and first-order identities for entropy-maximizing matching laws.

theorem OAI.MatchingEntropy.entropy_mix_ge line 19

Source documentation

Concavity of actual finite-law Shannon entropy.

theorem entropy_mix_ge {ι : Type*} [Fintype ι] {p q : ι → ℝ}
    (hp : ∀ i, 0 ≤ p i) (hq : ∀ i, 0 ≤ q i)
    {t : ℝ} (ht : t ∈ Set.Icc (0 : ℝ) 1) :
    (1-t) * entropy p + t * entropy q ≤
      entropy (fun i => (1-t)*p i + t*q i) := by
…

Mentions: OAI.MatchingEntropy.entropy

theorem OAI.MatchingEntropy.entropy_mix_zero_bonus line 34

Source documentation

A zero probability gains a strict logarithmic bonus under mixing. This is the boundary argument needed to obtain a positive entropy optimizer on the entire face, not an assumed regularity of H.

theorem entropy_mix_zero_bonus {ι : Type*} [Fintype ι] {p q : ι → ℝ}
    (hp : ∀ i, 0 ≤ p i) (hq : ∀ i, 0 ≤ q i) {j : ι} (hj : p j = 0)
    {t : ℝ} (ht : t ∈ Set.Icc (0 : ℝ) 1) :
    (1-t) * entropy p + t * entropy q + q j * Real.negMulLog t ≤
      entropy (fun i => (1-t)*p i + t*q i) := by
…

Mentions: OAI.MatchingEntropy.entropy

theorem OAI.MatchingEntropy.entropy_maximizer_support line 57

Source documentation

Every entropy maximizer on a convex feasible set has maximal support.

theorem entropy_maximizer_support {ι : Type*} [Fintype ι] {p q : ι → ℝ}
    (hp : ∀ i, 0 ≤ p i) (hq : ∀ i, 0 ≤ q i)
    (hmax : ∀ t ∈ Set.Icc (0 : ℝ) 1,
      entropy (fun i => (1-t)*p i+t*q i) ≤ entropy p) {j : ι} (hjq : 0 < q j) :
    0 < p j := by
…

Mentions: OAI.MatchingEntropy.entropy

theorem OAI.MatchingEntropy.matching_optimizer_support line 81

Source documentation

The preceding support conclusion for the concrete matching-law optimizer.

theorem matching_optimizer_support (G : LooplessGraph V E) {y : E → ℝ}
    {p q : G.Matching → ℝ} (hp : p ∈ G.feasibleLaws y)
    (hq : q ∈ G.feasibleLaws y) (hopt : entropy p = maxMatchingEntropy G y)
    {M : G.Matching} (hM : 0 < q M) : 0 < p M := by
…

Mentions: OAI.MatchingEntropy.entropy, OAI.MatchingEntropy.maxMatchingEntropy

theorem OAI.MatchingEntropy.negMulLog_tangent line 101
Source documentation
Supporting-line inequality for -x log x, with no positivity assumption on the comparison probability x.
```
theorem negMulLog_tangent {x y : ℝ} (hx : 0 ≤ x) (hy : 0 < y) :
    Real.negMulLog x ≤ -x * Real.log y + y-x := by
…
```

theorem OAI.MatchingEntropy.entropy_le_crossEntropy line 116

Source documentation

Gibbs' inequality on a finite set, with the exact support condition needed on boundary faces.

theorem entropy_le_crossEntropy {ι : Type*} [Fintype ι] {p q : ι → ℝ}
    (hp : p ∈ probabilitySimplex ι) (hq : q ∈ probabilitySimplex ι)
    (hsupp : ∀ i, p i = 0 → q i = 0) :
    entropy q ≤ -∑ i, q i * Real.log (p i) := by
…

Mentions: OAI.MatchingEntropy.probabilitySimplex, OAI.MatchingEntropy.entropy

theorem OAI.MatchingEntropy.entropy_line_hasDerivAt line 132

Source documentation

Derivative of entropy along a line supported on the positive probabilities.

theorem entropy_line_hasDerivAt {ι : Type*} [Fintype ι] (p v : ι → ℝ)
    (hsupp : ∀ i, p i = 0 → v i = 0) :
    HasDerivAt (fun t : ℝ => entropy (fun i => p i+t*v i))
      (-∑ i, v i * Real.log (p i) - ∑ i, v i) 0 := by
…

Mentions: OAI.MatchingEntropy.entropy

theorem OAI.MatchingEntropy.matching_optimizer_log_annihilates line 156

Source documentation

The log probabilities of the actual optimizer annihilate every feasible mass/mean-preserving linear variation. No exponential representation assumed.

theorem matching_optimizer_log_annihilates (G : LooplessGraph V E) {y : E → ℝ}
    {p : G.Matching → ℝ} (hp : p ∈ G.feasibleLaws y)
    (hopt : entropy p = maxMatchingEntropy G y) (v : G.Matching → ℝ)
    (hvsum : ∑ M, v M = 0) (hvmean : G.mean v = 0)
    (hsupp : ∀ M, p M = 0 → v M = 0) :
    ∑ M, v M * Real.log (p M) = 0 := by
…

Mentions: OAI.MatchingEntropy.entropy, OAI.MatchingEntropy.maxMatchingEntropy

theorem OAI.MatchingEntropy.exists_pos_nonneg_perturb line 190
Source documentation
A finite nonnegative vector permits small positive motion in any direction which does not point outwards at its zero coordinates.
```
theorem exists_pos_nonneg_perturb {ι : Type*} [Fintype ι] (p v : ι → ℝ)
    (hp : ∀ i, 0 ≤ p i) (hz : ∀ i, p i = 0 → 0 ≤ v i) :
    ∃ t : ℝ, 0 < t ∧ ∀ i, 0 ≤ p i+t*v i := by
…
```

theorem OAI.MatchingEntropy.matching_optimizer_face_support line 216

Source documentation

The support of an optimizing law is a face: every law at a mean generated by that support is itself supported there. This avoids assuming a face representation of the marginal polytope in the entropy-optimization step.

theorem matching_optimizer_face_support (G : LooplessGraph V E) {y : E → ℝ}
    {p : G.Matching → ℝ} (hp : p ∈ G.feasibleLaws y)
    (hopt : entropy p = maxMatchingEntropy G y)
    {q r : G.Matching → ℝ} (hq : q ∈ probabilitySimplex G.Matching)
    (hr : r ∈ probabilitySimplex G.Matching) (hmean : G.mean q = G.mean r)
    (hrsupport : ∀ M, p M = 0 → r M = 0) :
    ∀ M, p M = 0 → q M = 0 := by
…

Mentions: OAI.MatchingEntropy.entropy, OAI.MatchingEntropy.maxMatchingEntropy, OAI.MatchingEntropy.probabilitySimplex