Gaussian-rational unitaries and projective measurements are dense

• exists_unitary_entriesIn_norm_smul_sub_le: up to a unit phase, every unitary is within η (in operator norm) of a unitary with Gaussian-rational entries — the Cayley transform of an entrywise rounding of the skew-Hermitian Cayley preimage;
• IsPVM.exists_entriesIn_norm_sub_le: every projective measurement is within η, element by element, of a projective measurement with Gaussian-rational entries — conjugate the coordinate pattern of IsPVM.exists_unitary_pattern by the approximating unitary.

This is the density half of lem:value-lower-approx, and the point where the Lean route departs from the paper's: the paper rounds the measurement operators themselves and repairs the result into a POVM (its Claims "Stability" and "Density"); here the rounding happens at the level of the skew-Hermitian generator, so that the rounded object is an exact projective measurement and no repair is needed.

theorem MIPRE.ValueApprox.exists_unitary_entriesIn_norm_smul_sub_le {n : Type u_1} [Fintype n] [DecidableEq n] {U : Matrix n n ℂ} (hU : U ∈ Matrix.unitaryGroup n ℂ) {η : ℝ} (hη : 0 < η) : ∃ (z : ℂ), ‖z‖ = 1 ∧ ∃ V ∈ Matrix.unitaryGroup n ℂ, EntriesIn GaussianRat V ∧ ‖z • U - V‖ ≤ η

Up to a unit phase z, every unitary U is within η of a Gaussian-rational unitary.

theorem MIPRE.ValueApprox.IsPVM.exists_entriesIn_norm_sub_le {n : Type u_1} [Fintype n] [DecidableEq n] {A : Type u_2} [Fintype A] [DecidableEq A] {M : A → Matrix n n ℂ} (hM : IsPVM M) {η : ℝ} (hη : 0 < η) : ∃ (M' : A → Matrix n n ℂ), IsPVM M' ∧ (∀ (a : A), EntriesIn GaussianRat (M' a)) ∧ ∀ (a : A), ‖M a - M' a‖ ≤ η

Every projective measurement is within η, element by element, of a projective measurement with Gaussian-rational entries.