OAI/NumberTheory/Jacobsthal/Renewal/KernelPotential.lean

GitHub source file

10 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.Erdos970.NumberTheoryLean.KernelPotential.potential line 16
2. instance OAI.Erdos970.NumberTheoryLean.KernelPotential.potential_isSFiniteKernel line 19
3. theorem OAI.Erdos970.NumberTheoryLean.KernelPotential.compose_mono_left line 32
4. theorem OAI.Erdos970.NumberTheoryLean.KernelPotential.compose_finset_sum_left line 40
5. theorem OAI.Erdos970.NumberTheoryLean.KernelPotential.power_comp_succ line 47
6. theorem OAI.Erdos970.NumberTheoryLean.KernelPotential.potential_unfold line 52
7. theorem OAI.Erdos970.NumberTheoryLean.KernelPotential.potential_le_of_super line 62
8. theorem OAI.Erdos970.NumberTheoryLean.KernelPotential.potential_add line 86
9. theorem OAI.Erdos970.NumberTheoryLean.KernelPotential.potential_comp_left line 92
10. theorem OAI.Erdos970.NumberTheoryLean.KernelPotential.first_capture_decomposition line 100