Main.lean`

5 declarations, 0 contain sorry, 0 declared as axioms

The nonlinear entropy defect bound F - H ≤ 8m (1 - exp (-F/m)) for finite loopless multigraphs on 2m vertices, and the perfect matching count bound [k exp (-8 (1 - 1/k))]^m, with its coarse bound (exp (-8) k)^m, when the entire edge set is partitioned into k ≥ 1 perfect matchings.

theorem OAI.MatchingEntropy.entropy_barrier_ge_id line 25
Source documentation
The small-entropy regime of the nonlinear barrier function.
```
theorem entropy_barrier_ge_id {t : ℝ} (ht : 0 ≤ t) (h8 : t ≤ Real.log 8) :
    t ≤ 8 * (1-Real.exp (-t)) := by
…
```

theorem OAI.MatchingEntropy.marginal_entropy_support_bound line 50

Source documentation

Entropy on s positive edge coordinates of total mass m is at most m log(s/m).

theorem marginal_entropy_support_bound (G : LooplessGraph V E) {m : ℕ}
    (hm : 0 < m) (hV : Fintype.card V=2*m) {x : E → ℝ} (hx : x ∈ G.polytope) :
    0 ≤ entropy x ∧ 0 < Fintype.card {e // 0 < x e} ∧
      entropy x ≤ (m:ℝ)*Real.log ((Fintype.card {e // 0 < x e}:ℝ)/(m:ℝ)) := by
…

Mentions: OAI.MatchingEntropy.entropy

theorem OAI.MatchingEntropy.entropy_main line 85
Source documentation
Main entropy comparison, for every marginal in the actual matching polytope.
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Fintype, DecidableEq, OAI.MatchingEntropy.LooplessGraph, Nat, LT.lt, OfNat.ofNat, Eq, Fintype.card, HMul.hMul, Nonempty, OAI.MatchingEntropy.LooplessGraph.Matching, Real, Membership.mem, Set, OAI.MatchingEntropy.LooplessGraph.polytope, LE.le, HSub.hSub, OAI.MatchingEntropy.marginalEntropy, OAI.MatchingEntropy.maxMatchingEntropy, Real.exp and 2 more
Proof uses: cast, Eq.symm, Eq.trans, congrFun', congrArg, Nat.cast_zero, Even, Eq.mpr, id, even_two_mul, And, OAI.MatchingEntropy.entropyDefect, Exists, OAI.MatchingEntropy.entropyDefect_attains_max, Decidable.byContradiction, Not, lt_of_not_ge, OAI.MatchingEntropy.entropy, Mathlib.Tactic.Linarith.lt_irrefl, Eq.mp and 103 more
158 instances, coercions and auxiliary constants left out.
Distinct definitions of this name: ComparatorChallenges/MatchingEntropy.lean:58 (same statement text; different proof or body). Qualify references as OAI.MatchingEntropy.entropy_main@path.
Tactic trace: 47 steps
Open to load the checked before-and-after goal states.
```
theorem entropy_main (G : LooplessGraph V E) (m : ℕ)
    (hm : 0 < m) (hV : Fintype.card V = 2 * m)
    (hPM : Nonempty G.Matching) (y : E → ℝ) (hy : y ∈ G.polytope) :
    marginalEntropy y - maxMatchingEntropy G y ≤
      8 * (m : ℝ) * (1 - Real.exp (-marginalEntropy y / (m : ℝ))) := by
…
```
Mentions: OAI.MatchingEntropy.marginalEntropy, OAI.MatchingEntropy.maxMatchingEntropy

theorem OAI.MatchingEntropy.uniform_decomposition_mem line 135

Source documentation

An edge partition into k matchings places the exact uniform edge vector in P.

theorem uniform_decomposition_mem (G : LooplessGraph V E) {k : ℕ} (hk : 1 ≤ k)
    (M : Fin k → G.Matching)
    (hpartition : ∀ e : E, ∃! i : Fin k, e ∈ (M i).val) :
    (fun _ : E => 1/(k:ℝ)) ∈ G.polytope := by
…

theorem OAI.MatchingEntropy.count_main line 163

Source documentation

The exact decomposable-graph count theorem, including its coarser bound.

theorem count_main (G : LooplessGraph V E) (m k : ℕ)
    (hm : 0 < m) (hV : Fintype.card V = 2 * m) (hk : 1 ≤ k)
    (M : Fin k → G.Matching)
    (hpartition : ∀ e : E, ∃! i : Fin k, e ∈ (M i).val) :
    ((k : ℝ) * Real.exp (-8 * (1 - 1 / (k : ℝ)))) ^ m ≤
        (Fintype.card G.Matching : ℝ) ∧
      (Real.exp (-8) * (k : ℝ)) ^ m ≤
        ((k : ℝ) * Real.exp (-8 * (1 - 1 / (k : ℝ)))) ^ m := by
…