OAI/NumberTheory/Ostmann/Supply/ActualKernelBudget.lean

GitHub source file

4 declarations, 0 contain sorry, 0 declared as axioms

1. theorem OAI.Ostmann.Supply.actualKernelOutput_norm_sq line 14
2. theorem OAI.Ostmann.Supply.actualKernelInput_norm_sq line 23
3. theorem OAI.Ostmann.Supply.prime_mem_retainedProducts line 44
4. theorem OAI.Ostmann.Supply.eventually_actualKernel_budgets line 53