OAI/Combinatorics/PerfectMatching/Covariance.lean

GitHub source file

15 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.MatchingEntropy.weightedColumns line 20
2. def OAI.MatchingEntropy.covariance line 23
3. theorem OAI.MatchingEntropy.covariance_posSemidef line 27
4. theorem OAI.MatchingEntropy.covariance_entry line 33
5. theorem OAI.MatchingEntropy.covariance_mulVec line 45
6. theorem OAI.MatchingEntropy.covariance_quadratic line 58
7. def OAI.MatchingEntropy.weightedDirectionSpace line 74
8. theorem OAI.MatchingEntropy.weightedColumns_span line 78
9. theorem OAI.MatchingEntropy.covariance_rank line 106
10. def OAI.MatchingEntropy.normalizedCentered line 110
11. theorem OAI.MatchingEntropy.normalizedCentered_mean line 114
12. theorem OAI.MatchingEntropy.normalizedCentered_variance line 121
13. theorem OAI.MatchingEntropy.normalized_covariance_trace line 141
14. theorem OAI.MatchingEntropy.covariance_rank_bound line 156

    Source documentation

    Spectral form of the second-variation step, using the full (possibly singular) covariance rather than introducing an inverse on its image.

    theorem covariance_rank_bound {ι : Type*} [Fintype ι] [DecidableEq ι]
        {C : Matrix ι ι ℝ} (hC : C.PosSemidef) {a : ℝ}
        (hsecond : ∀ u : ι → ℝ,
          (a - 1) * ((C *ᵥ u) ⬝ᵥ (C *ᵥ u)) + u ⬝ᵥ (C *ᵥ u) ≤ 0) :
        (C.rank : ℝ) ≤ (1-a) * C.trace := by
    …

15. theorem OAI.MatchingEntropy.covariance_contradiction line 196

    Source documentation

    The numerical contradiction following covariance rank and trace.

    theorem covariance_contradiction {ι : Type*} [Fintype ι] [DecidableEq ι]
        {C : Matrix ι ι ℝ} (hC : C.PosSemidef) {a m s : ℝ}
        (hm : 0 < m) (hs : 8*m < s) (hrank : s-4*m ≤ C.rank)
        (htrace : C.trace = s-m) (ha : 8*m/s ≤ a)
        (hsecond : ∀ u : ι → ℝ,
          (a-1) * ((C *ᵥ u) ⬝ᵥ (C *ᵥ u)) + u ⬝ᵥ (C *ᵥ u) ≤ 0) : False := by
    …