KMSBasisComparisonNeighborsRetention.lean`

2 declarations, 0 contain sorry, 0 declared as axioms

Local ordered-basis retention in the precise KMS vertex representation.

theorem OAI.UniqueGamesTheorem.Inverse.KMSBasisComparison.relativeDensity_eq_expect_subtype line 15
theorem OAI.UniqueGamesTheorem.Inverse.KMSBasisComparison.outsideNeighbor_retention line 34
Source documentation
The ordered-basis test conditioned on its good event samples every full Grassmann neighbor uniformly. The target observable is the original lifted indicator, so this identity directly feeds the matrix-test retention bound.
```
theorem outsideNeighbor_retention {n ell : ℕ} (S : Finset (KMS.Vertex n ell))
    (X : BasisMap n ell) (hX : Function.Injective X) :
    (𝔼 p : OutsideNeighborFactors X,
      liftedIndicator S (rankOneUpdate X p.1.val p.2.val)) =
        KMS.relativeDensity S (KMS.neighbors (rangeVertex X hX)) := by
…
```
Mentions: OAI.UniqueGamesTheorem.Inverse.KMS.Vertex, OAI.UniqueGamesTheorem.Inverse.KMSBasisComparison.BasisMap, OAI.UniqueGamesTheorem.Inverse.KMSBasisComparison.OutsideNeighborFactors, OAI.UniqueGamesTheorem.Inverse.KMSBasisComparison.liftedIndicator, OAI.UniqueGamesTheorem.Inverse.KMSBasisComparison.rankOneUpdate, OAI.UniqueGamesTheorem.Inverse.KMS.relativeDensity, OAI.UniqueGamesTheorem.Inverse.KMS.neighbors, OAI.UniqueGamesTheorem.Inverse.KMSBasisComparison.rangeVertex