OAI/Analysis/FourierLLogL/Snapshot/Representative.lean

GitHub source file

18 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.FourierLLogL.Dyadic.Procedure.Snapshot.tolerance line 14
2. def OAI.FourierLLogL.Dyadic.Procedure.Snapshot.spotLimit line 16
3. lemma OAI.FourierLLogL.Dyadic.Procedure.Snapshot.tolerance_pos line 19
4. lemma OAI.FourierLLogL.Dyadic.Procedure.Snapshot.spotLimit_pos line 21
5. def OAI.FourierLLogL.Dyadic.Procedure.Snapshot.adjacent line 24
6. lemma OAI.FourierLLogL.Dyadic.Procedure.Snapshot.adjacent_zero line 27
7. lemma OAI.FourierLLogL.Dyadic.Procedure.Snapshot.adjacent_neg line 38
8. def OAI.FourierLLogL.Dyadic.Procedure.Snapshot.net_ok line 50
9. lemma OAI.FourierLLogL.Dyadic.Procedure.Snapshot.exists_net line 54
10. def OAI.FourierLLogL.Dyadic.Procedure.Snapshot.net line 84
11. lemma OAI.FourierLLogL.Dyadic.Procedure.Snapshot.net_spec line 85
12. lemma OAI.FourierLLogL.Dyadic.Procedure.Snapshot.net_len_main line 88
13. lemma OAI.FourierLLogL.Dyadic.Procedure.Snapshot.share_pos' line 95
14. lemma OAI.FourierLLogL.Dyadic.Procedure.Snapshot.share_small line 97
15. lemma OAI.FourierLLogL.Dyadic.Procedure.Snapshot.share_child line 103
16. lemma OAI.FourierLLogL.Dyadic.Procedure.Snapshot.scalar_point line 111
17. lemma OAI.FourierLLogL.Dyadic.Procedure.Snapshot.scalar_compare line 136
18. lemma OAI.FourierLLogL.Dyadic.Procedure.Snapshot.scalar_power line 147