OAI/NumberTheory/Jacobsthal/Estimates/ScalarFreeGate.lean

GitHub source file

48 declarations, 0 contain sorry, 0 declared as axioms

  1. theorem OAI.Erdos970.ErdosContinuousOmission.omission_integral_hasSum line 17
  2. def OAI.Erdos970.ErdosContinuousOmission.omissionLossTerm line 31
  3. theorem OAI.Erdos970.ErdosContinuousOmission.omissionLossTerm_nonnegative line 35
  4. theorem OAI.Erdos970.ErdosContinuousOmission.actual_signed_loss_hasSum line 45
  5. theorem OAI.Erdos970.ErdosContinuousOmission.actual_signed_loss_series line 50
  6. theorem OAI.Erdos970.ErdosContinuousOmission.actual_loss_summable line 56
  7. theorem OAI.Erdos970.ErdosContinuousOmission.actual_coefficient_le_standard line 58
  8. theorem OAI.Erdos970.ErdosContinuousOmission.gate_zero_of_side line 73
  9. theorem OAI.Erdos970.ErdosContinuousOmission.omission_wrong_parity_zero line 77
  10. theorem OAI.Erdos970.ErdosContinuousOmission.omissionDensity_integrable line 107
  11. theorem OAI.Erdos970.ErdosContinuousOmission.first_odd_density_low line 117
  12. theorem OAI.Erdos970.ErdosContinuousOmission.first_odd_density_middle line 122
  13. theorem OAI.Erdos970.ErdosContinuousOmission.first_odd_density_high line 132
  14. theorem OAI.Erdos970.ErdosContinuousOmission.actual_first_loss_eq_one line 139
  15. def OAI.Erdos970.ErdosOmissionTail.freeGate line 189
  16. theorem OAI.Erdos970.ErdosOmissionTail.freeGate_continuous line 192
  17. theorem OAI.Erdos970.ErdosOmissionTail.freeGate_nonnegative line 204
  18. theorem OAI.Erdos970.ErdosOmissionTail.gate_le_freeGate line 210
  19. theorem OAI.Erdos970.ErdosOmissionTail.gate_mono line 223
  20. def OAI.Erdos970.ErdosOmissionTail.freeGateIterate line 231
  21. theorem OAI.Erdos970.ErdosOmissionTail.freeGateIterate_continuous line 235
  22. theorem OAI.Erdos970.ErdosOmissionTail.freeGateIterate_nonnegative line 241
  23. theorem OAI.Erdos970.ErdosOmissionTail.gateIterate_prefix_le line 247
  24. theorem OAI.Erdos970.ErdosOmissionTail.actual_omission_prefix_le line 261
  25. def OAI.Erdos970.ErdosOmissionTail.lastWindowCoefficient line 275
  26. theorem OAI.Erdos970.ErdosOmissionTail.last_window_integral line 278
  27. theorem OAI.Erdos970.ErdosOmissionTail.last_window_width line 285
  28. theorem OAI.Erdos970.ErdosOmissionTail.last_window_square_bound line 289
  29. theorem OAI.Erdos970.ErdosOmissionTail.last_window_mean_bound line 305
  30. def OAI.Erdos970.ErdosOmissionTail.orderedMass line 353
  31. theorem OAI.Erdos970.ErdosOmissionTail.orderedMass_continuous line 357
  32. theorem OAI.Erdos970.ErdosOmissionTail.orderedMass_nonnegative line 366
  33. theorem OAI.Erdos970.ErdosOmissionTail.log_power_primitive line 374
  34. theorem OAI.Erdos970.ErdosOmissionTail.orderedMass_eq line 384
  35. abbrev OAI.Erdos970.ErdosOmissionTail.ScalarProfile line 425
  36. def OAI.Erdos970.ErdosOmissionTail.ScalarContinuous line 426
  37. def OAI.Erdos970.ErdosOmissionTail.scalarFreeGate line 427
  38. def OAI.Erdos970.ErdosOmissionTail.scalarFreeIterate line 430
  39. theorem OAI.Erdos970.ErdosOmissionTail.scalarFreeGate_continuous line 434
  40. theorem OAI.Erdos970.ErdosOmissionTail.scalarFreeIterate_continuous line 438
  41. theorem OAI.Erdos970.ErdosOmissionTail.freeGate_total line 444
  42. theorem OAI.Erdos970.ErdosOmissionTail.freeGateIterate_total line 456
  43. def OAI.Erdos970.ErdosOmissionTail.terminalBlock line 468
  44. theorem OAI.Erdos970.ErdosOmissionTail.terminalBlock_continuous line 470
  45. theorem OAI.Erdos970.ErdosOmissionTail.terminalBlock_nonnegative line 473
  46. theorem OAI.Erdos970.ErdosOmissionTail.actual_free_total line 476
  47. def OAI.Erdos970.ErdosOmissionTail.combinedDensity line 489
  48. theorem OAI.Erdos970.ErdosOmissionTail.actual_combined_density_le line 492