OAI/Analysis/JiangSu/Comparison/FiniteScalar.lean

GitHub source file

8 declarations, 0 contain sorry, 0 declared as axioms

1. lemma OAI.DirectComparison.finite_runs_exhaust line 14
2. def OAI.DirectComparison.SpectralProjectionSupply line 50
3. lemma OAI.DirectComparison.localized_projection line 55
4. theorem OAI.DirectComparison.finite_scalar_single line 72
5. lemma OAI.DirectComparison.compression_persist_real line 112
6. lemma OAI.DirectComparison.ProjectionPacking.refine_good line 122
7. theorem OAI.DirectComparison.finite_scalar_family line 132
8. theorem OAI.DirectComparison.scalar_compressions line 178