OAI/NumberTheory/Jacobsthal/Paths/HighPrefixState.lean

GitHub source file

22 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.Erdos970.ErdosPrimeInputs.HarmonicPrefixTilt.squareBoundE line 17
2. lemma OAI.Erdos970.ErdosPrimeInputs.HarmonicPrefixTilt.squareBoundE_measurable line 19
3. lemma OAI.Erdos970.ErdosPrimeInputs.HarmonicPrefixTilt.linear_lintegral line 23
4. lemma OAI.Erdos970.ErdosPrimeInputs.HarmonicPrefixTilt.harmonic_square_integral line 35
5. theorem OAI.Erdos970.ErdosPrimeInputs.HarmonicPrefixTilt.schur_two line 51
6. theorem OAI.Erdos970.ErdosPrimeInputs.HarmonicPrefixTilt.weighted_prefix_mass line 73
7. def OAI.Erdos970.ErdosPrimeInputs.HarmonicLongPrefixes.tailMass line 89
8. lemma OAI.Erdos970.ErdosPrimeInputs.HarmonicLongPrefixes.half_power_antitone line 92
9. lemma OAI.Erdos970.ErdosPrimeInputs.HarmonicLongPrefixes.unweight_two line 101
10. theorem OAI.Erdos970.ErdosPrimeInputs.HarmonicLongPrefixes.weighted_tail_bound line 109
11. def OAI.Erdos970.ErdosPrimeInputs.HarmonicLongPrefixes.longPrefixMass line 124
12. theorem OAI.Erdos970.ErdosPrimeInputs.HarmonicLongPrefixes.long_prefix_mass line 127
13. abbrev OAI.Erdos970.ErdosPrimeInputs.HighPrefixState.State line 141
14. def OAI.Erdos970.ErdosPrimeInputs.HighPrefixState.initial line 143
15. def OAI.Erdos970.ErdosPrimeInputs.HighPrefixState.update line 146
16. lemma OAI.Erdos970.ErdosPrimeInputs.HighPrefixState.update_measurable line 149
17. lemma OAI.Erdos970.ErdosPrimeInputs.HighPrefixState.update_flag line 157
18. def OAI.Erdos970.ErdosPrimeInputs.HighPrefixState.Invariant line 161
19. lemma OAI.Erdos970.ErdosPrimeInputs.HighPrefixState.invariant_measurable line 164
20. lemma OAI.Erdos970.ErdosPrimeInputs.HighPrefixState.initial_invariant line 173
21. lemma OAI.Erdos970.ErdosPrimeInputs.HighPrefixState.update_invariant line 184
22. theorem OAI.Erdos970.ErdosPrimeInputs.HighPrefixState.short_high_gap line 201