OAI/NumberTheory/Jacobsthal/Probability/HighPrefixKernel.lean

GitHub source file

11 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.Erdos970.ErdosPrimeInputs.HighPrefixKernel.kernel line 16
2. instance OAI.Erdos970.ErdosPrimeInputs.HighPrefixKernel.kernel_isSFinite line 21
3. lemma OAI.Erdos970.ErdosPrimeInputs.HighPrefixKernel.update_at_measurable line 25
4. theorem OAI.Erdos970.ErdosPrimeInputs.HighPrefixKernel.kernel_eq_map line 28
5. lemma OAI.Erdos970.ErdosPrimeInputs.HighPrefixKernel.harmonic_ae_interval line 39
6. theorem OAI.Erdos970.ErdosPrimeInputs.HighPrefixKernel.ae_update line 47
7. lemma OAI.Erdos970.ErdosPrimeInputs.HighPrefixKernel.state_schur_one line 54
8. lemma OAI.Erdos970.ErdosPrimeInputs.HighPrefixKernel.state_schur_two line 61
9. theorem OAI.Erdos970.ErdosPrimeInputs.HighPrefixKernel.total_mass line 68
10. theorem OAI.Erdos970.ErdosPrimeInputs.HighPrefixKernel.weighted_mass line 74
11. theorem OAI.Erdos970.ErdosPrimeInputs.HighPrefixKernel.ae_invariant line 80