KMSAnalyticHybridCoordinatesConditions.lean`

2 declarations, 0 contain sorry, 0 declared as axioms

The actual hybrid selector in compressed-fiber coordinates

When the prescribed compression is onto W, the hybrid image and preimage conditions are equivalent to injectivity of the complementary target map and surjectivity of the remaining coordinate map. These are conditions on the actual assembled linear map, with no rank or analytic hypothesis.

theorem OAI.UniqueGamesTheorem.Inverse.KMSAnalyticHybridCoordinates.psi_split line 26
theorem OAI.UniqueGamesTheorem.Inverse.KMSAnalyticHybridCoordinates.hybrid_assemble_iff line 39
Source documentation
The genuine hybrid selector is exactly the two independent coordinate conditions. In particular the full-rank coordinate condition does not depend on the chosen injective map into the complementary target.
```
theorem hybrid_assemble_iff {z : B →ₗ[R] W}
    (p : Coordinates (A := A) (D := D) (C := C) z)
…
```
Mentions: OAI.UniqueGamesTheorem.Inverse.KMSAnalyticHybridCoordinates.Coordinates