Duality.lean`

10 declarations, 0 contain sorry, 0 declared as axioms

Finite exponential tilts, partition functions, and entropy duality on a face.

def OAI.MatchingEntropy.partition line 19
Source documentation
Finite exponential partition function, based on a probability law p.
```
def partition {ι : Type*} [Fintype ι] (p a : ι → ℝ) (t : ℝ) : ℝ :=
…
```
def OAI.MatchingEntropy.tiltedLaw line 22
theorem OAI.MatchingEntropy.partition_pos line 25
theorem OAI.MatchingEntropy.partition_zero line 32
theorem OAI.MatchingEntropy.tiltedLaw_mem_simplex line 36

theorem OAI.MatchingEntropy.entropy_partition_bound line 46

Source documentation

Gibbs' variational inequality for the explicit finite partition function, including all boundary laws supported on p.

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

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

def OAI.MatchingEntropy.linearScore line 78
Source documentation
A score affine in the matching vector; the constant permits centering without changing the duality calculation.
```
def linearScore (G : LooplessGraph V E) (u : E → ℝ) (c : ℝ) (M : G.Matching) : ℝ :=
…
```
theorem OAI.MatchingEntropy.sum_mean_assoc line 82
theorem OAI.MatchingEntropy.linearScore_expectation line 93

theorem OAI.MatchingEntropy.matching_entropy_dual_bound line 105

Source documentation

A genuine upper bound on the actual maximum entropy at every mean in the optimizer's face. This is proved from Gibbs' inequality, not assumed as a replacement definition of H.

theorem matching_entropy_dual_bound (G : LooplessGraph V E) {y : E → ℝ}
    {p : G.Matching → ℝ} (hp : p ∈ G.feasibleLaws y)
    (hopt : entropy p = maxMatchingEntropy G y)
    {r : G.Matching → ℝ} (hr : r ∈ probabilitySimplex G.Matching)
    (hrsupport : ∀ M, p M = 0 → r M = 0)
    (u : E → ℝ) (c t : ℝ) :
    maxMatchingEntropy G (G.mean r) ≤
      Real.log (partition p (linearScore G u c) t) - ∑ M, r M * Real.log (p M) -
        t * ∑ M, r M * linearScore G u c M := by
…

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