SecondVariation.lean`

4 declarations, 0 contain sorry, 0 declared as axioms

The second-variation inequality at a maximum of the actual entropy defect.

def OAI.MatchingEntropy.entropyDefect line 18
theorem OAI.MatchingEntropy.score_law_eventually_simplex line 21
theorem OAI.MatchingEntropy.mean_score_support line 38

theorem OAI.MatchingEntropy.matching_defect_second_variation line 55

Source documentation

A maximum of the actual entropy defect satisfies the second-variation inequality. The comparison uses optimizing probability laws rather than a replacement for H.

theorem matching_defect_second_variation (G : LooplessGraph V E) {x : E → ℝ}
    {p : G.Matching → ℝ} (hp : p ∈ G.feasibleLaws x)
    (hopt : entropy p = maxMatchingEntropy G x) {m : ℝ} (hm : m ≠ 0)
    (hmax : ∀ y ∈ G.polytope, entropyDefect G m y ≤ entropyDefect G m x)
    (u : E → ℝ) (c : ℝ) (hcenter : ∑ M, p M*linearScore G u c M = 0) :
    (8*Real.exp (-entropy x/m)-1)*
        (∑ e, (G.mean (fun M => p M*linearScore G u c M) e)^2/x e) +
      (8*Real.exp (-entropy x/m)/m)*
        (entropyLineD x (G.mean (fun M => p M*linearScore G u c M)) 0)^2 +
      (∑ M, p M*(linearScore G u c M)^2) ≤ 0 := by
…

Mentions: OAI.MatchingEntropy.entropy, OAI.MatchingEntropy.maxMatchingEntropy, OAI.MatchingEntropy.entropyDefect, OAI.MatchingEntropy.linearScore, OAI.MatchingEntropy.entropyLineD