OAI/NumberTheory/Jacobsthal/Estimates/LossBounds.lean

GitHub source file

37 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.Erdos970.ErdosBoundaryLoss.loss2Kernel line 13
  2. def OAI.Erdos970.ErdosBoundaryLoss.loss3Kernel line 15
  3. def OAI.Erdos970.ErdosBoundaryLoss.L1 line 17
  4. def OAI.Erdos970.ErdosBoundaryLoss.L2 line 18
  5. def OAI.Erdos970.ErdosBoundaryLoss.L3 line 20
  6. def OAI.Erdos970.ErdosBoundaryLoss.inner2Primitive line 31
  7. theorem OAI.Erdos970.ErdosBoundaryLoss.inner2Primitive_deriv line 40
  8. def OAI.Erdos970.ErdosBoundaryLoss.middle3Kernel line 56
  9. def OAI.Erdos970.ErdosBoundaryLoss.inner3Primitive line 75
  10. theorem OAI.Erdos970.ErdosBoundaryLoss.inner3Primitive_deriv line 87
  11. def OAI.Erdos970.ErdosBoundaryLoss.middle3Primitive line 106
  12. theorem OAI.Erdos970.ErdosBoundaryLoss.middle3Primitive_deriv line 124
  13. def OAI.Erdos970.ErdosBoundaryLoss.reduced2 line 149
  14. def OAI.Erdos970.ErdosBoundaryLoss.reduced3 line 161
  15. def OAI.Erdos970.ErdosBoundaryLoss.outer2Primitive line 178
  16. theorem OAI.Erdos970.ErdosBoundaryLoss.outer2Primitive_deriv line 190
  17. def OAI.Erdos970.ErdosBoundaryLoss.outer3Primitive line 209
  18. theorem OAI.Erdos970.ErdosBoundaryLoss.outer3Primitive_deriv line 226
  19. theorem OAI.Erdos970.ErdosBoundaryLoss.loss2_inner_integrable line 259
  20. theorem OAI.Erdos970.ErdosBoundaryLoss.loss2_inner_reduction line 270
  21. theorem OAI.Erdos970.ErdosBoundaryLoss.loss3_inner_integrable line 284
  22. theorem OAI.Erdos970.ErdosBoundaryLoss.loss3_inner_reduction line 296
  23. theorem OAI.Erdos970.ErdosBoundaryLoss.loss3_middle_kernel_integrable line 312
  24. theorem OAI.Erdos970.ErdosBoundaryLoss.loss3_middle_reduction line 323
  25. theorem OAI.Erdos970.ErdosBoundaryLoss.reduced2_integrable line 352
  26. theorem OAI.Erdos970.ErdosBoundaryLoss.reduced3_integrable line 361
  27. theorem OAI.Erdos970.ErdosBoundaryLoss.loss3_middle_integrable line 370
  28. theorem OAI.Erdos970.ErdosBoundaryLoss.loss2_outer_integrable line 377
  29. theorem OAI.Erdos970.ErdosBoundaryLoss.loss3_outer_integrable line 384
  30. theorem OAI.Erdos970.ErdosBoundaryLoss.L1_integrable line 391
  31. theorem OAI.Erdos970.ErdosBoundaryLoss.L1_eq line 394
  32. theorem OAI.Erdos970.ErdosBoundaryLoss.L2_eq line 399
  33. theorem OAI.Erdos970.ErdosBoundaryLoss.L3_eq line 416
  34. theorem OAI.Erdos970.ErdosBoundaryLoss.log_two_bounds line 441
  35. theorem OAI.Erdos970.ErdosBoundaryLoss.L2_lt line 446
  36. theorem OAI.Erdos970.ErdosBoundaryLoss.L3_lt line 453
  37. theorem OAI.Erdos970.ErdosBoundaryLoss.first_three_loss_lt line 460