OAI/MathematicalPhysics/RapidForcing/Support.lean

GitHub source file

11 declarations, 0 contain sorry, 0 declared as axioms

1. lemma OAI.RapidForcing.K_closed line 9
2. lemma OAI.RapidForcing.norm_le_three_of_mem_K line 20
3. lemma OAI.RapidForcing.K_compact line 29
4. lemma OAI.RapidForcing.supported_iff_zero_off line 38
5. lemma OAI.RapidForcing.Supported.zero_off line 51
6. lemma OAI.RapidForcing.Supported.spatialD line 55
7. lemma OAI.RapidForcing.Supported.timeD line 59
8. lemma OAI.RapidForcing.Supported.spatialIter line 68
9. lemma OAI.RapidForcing.Supported.spatialMulti line 75
10. lemma OAI.RapidForcing.Supported.mixedD line 79
11. theorem OAI.RapidForcing.rapidSpaceTime_of_supported_rapid line 86