OAI/Probability/SKBarriers/Hierarchy/HierarchyPrefix.lean

GitHub source file

10 declarations, 0 contain sorry, 0 declared as axioms

1. theorem OAI.SK.Analytic.TailZero.zero line 27
2. theorem OAI.SK.Analytic.PrefixZero.zero line 36
3. theorem OAI.SK.Analytic.TailZero.add line 44
4. theorem OAI.SK.Analytic.TailZero.smul line 54
5. theorem OAI.SK.Analytic.PrefixZero.add line 64
6. theorem OAI.SK.Analytic.PrefixZero.smul line 76
7. theorem OAI.SK.Analytic.tailZero_coordinateAxis line 88
8. theorem OAI.SK.Analytic.prefixZero_coordinateAxis line 101
9. theorem OAI.SK.Analytic.coordinateLinear_coordinateAxis line 114
10. theorem OAI.SK.Analytic.hierarchyLevel_pair_invariance line 118