MatchingCovariance.lean`

12 declarations, 0 contain sorry, 0 declared as axioms

Normalized matching covariance: face rank, exact trace, and second variation.

def OAI.MatchingEntropy.matchingNormalized line 22
Source documentation
Normalized matching directions on exactly the positive edge support.
```
def matchingNormalized (G : LooplessGraph V E) (x : E → ℝ) :
    G.Matching → {e // 0 < x e} → ℝ :=
…
```
theorem OAI.MatchingEntropy.matchingNormalized_average line 27

theorem OAI.MatchingEntropy.midpoint_law_support line 37

Source documentation

A feasible two-sided direction has a positive-side law supported on the entropy optimizer at its midpoint.

theorem midpoint_law_support (G : LooplessGraph V E) {x v : E → ℝ} {a : ℝ}
    {p q r : G.Matching → ℝ} (hp : p ∈ G.feasibleLaws x)
    (hopt : entropy p=maxMatchingEntropy G x)
    (hq : q ∈ G.feasibleLaws (x+a • v))
    (hr : r ∈ G.feasibleLaws (x+(-a) • v)) :
    ∀ M, 0 < q M → 0 < p M := by
…

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

theorem OAI.MatchingEntropy.normalized_face_mem line 61
Source documentation
Every active-face direction belongs to the optimizer's normalized covariance span. No face support or dimension assertion is being supplied as a hypothesis.
```
theorem normalized_face_mem (G : LooplessGraph V E) {x : E → ℝ}
    (heven : Even (Fintype.card V)) {p : G.Matching → ℝ}
    (hp : p ∈ G.feasibleLaws x) (hopt : entropy p=maxMatchingEntropy G x)
    {u : {e // 0 < x e} → ℝ} (hu : u ∈ G.faceSpace x) :
    (fun e => u e/Real.sqrt (x e.val)) ∈ weightedDirectionSpace p (matchingNormalized G x) := by
…
```
Mentions: OAI.MatchingEntropy.entropy, OAI.MatchingEntropy.maxMatchingEntropy, OAI.MatchingEntropy.weightedDirectionSpace, OAI.MatchingEntropy.matchingNormalized
def OAI.MatchingEntropy.normalizeLinear line 100

theorem OAI.MatchingEntropy.matching_covariance_rank line 107

Source documentation

Face codimension gives a lower bound for the rank of the genuine covariance.

theorem matching_covariance_rank (G : LooplessGraph V E) {x : E → ℝ}
    (heven : Even (Fintype.card V)) {p : G.Matching → ℝ}
    (hp : p ∈ G.feasibleLaws x) (hopt : entropy p=maxMatchingEntropy G x) :
    Fintype.card {e // 0 < x e} ≤ 2*Fintype.card V+
      (covariance p (matchingNormalized G x)).rank := by
…

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

theorem OAI.MatchingEntropy.sum_positive_support line 136
def OAI.MatchingEntropy.matchingScoreWeights line 145
theorem OAI.MatchingEntropy.matchingNormalized_score line 149
theorem OAI.MatchingEntropy.matchingNormalized_mulVec line 164

theorem OAI.MatchingEntropy.matching_covariance_trace line 187

Source documentation

The normalized covariance has the exact trace s-m.

theorem matching_covariance_trace (G : LooplessGraph V E) {x : E → ℝ}
    {p : G.Matching → ℝ} (hp : p ∈ G.feasibleLaws x) {m : ℕ}
    (hV : Fintype.card V=2*m) :
    (covariance p (matchingNormalized G x)).trace = Fintype.card {e // 0 < x e}-(m:ℝ) := by
…

Mentions: OAI.MatchingEntropy.covariance, OAI.MatchingEntropy.matchingNormalized

theorem OAI.MatchingEntropy.matching_covariance_second_variation line 205

Source documentation

Convert the genuine second variation into the covariance spectral inequality.

theorem matching_covariance_second_variation (G : LooplessGraph V E) {x : E → ℝ}
    {p : G.Matching → ℝ} (hp : p ∈ G.feasibleLaws x)
    (hopt : entropy p=maxMatchingEntropy G x) {m : ℝ} (hm : 0 < m)
    (hmax : ∀ y ∈ G.polytope, entropyDefect G m y ≤ entropyDefect G m x)
    (u : {e // 0 < x e} → ℝ) :
    (8*Real.exp (-entropy x/m)-1)*
        ((covariance p (matchingNormalized G x) *ᵥ u) ⬝ᵥ
          (covariance p (matchingNormalized G x) *ᵥ u)) +
      u ⬝ᵥ (covariance p (matchingNormalized G x) *ᵥ u) ≤ 0 := by
…

Mentions: OAI.MatchingEntropy.entropy, OAI.MatchingEntropy.maxMatchingEntropy, OAI.MatchingEntropy.entropyDefect, OAI.MatchingEntropy.covariance, OAI.MatchingEntropy.matchingNormalized