OAI/NumberTheory/Jacobsthal/Estimates/ScalarTailRecurrence.lean

GitHub source file

25 declarations, 0 contain sorry, 0 declared as axioms

  1. theorem OAI.Erdos970.ErdosOmissionBindings.quadratic_window_integral line 14
  2. theorem OAI.Erdos970.ErdosOmissionBindings.integrated_force_window line 23
  3. theorem OAI.Erdos970.ErdosOmissionBindings.Audit.literal_shifted_force line 73
  4. theorem OAI.Erdos970.ErdosOmissionBindings.Audit.literal_shifted_high_support line 79
  5. theorem OAI.Erdos970.ErdosOmissionTail.terminalBlock_high line 94
  6. theorem OAI.Erdos970.ErdosOmissionTail.scalarFreeIterate_nonnegative line 97
  7. theorem OAI.Erdos970.ErdosOmissionTail.scalarFreeIterate_high line 107
  8. def OAI.Erdos970.ErdosOmissionTail.scalarTailIntegrand line 123
  9. def OAI.Erdos970.ErdosOmissionTail.scalarTailMass line 125
  10. theorem OAI.Erdos970.ErdosOmissionTail.scalarTailIntegrand_continuous line 128
  11. theorem OAI.Erdos970.ErdosOmissionTail.scalarTailIntegrand_nonnegative line 135
  12. theorem OAI.Erdos970.ErdosOmissionTail.scalarTailIntegrand_integrable line 139
  13. theorem OAI.Erdos970.ErdosOmissionTail.scalarTailMass_nonnegative line 157
  14. theorem OAI.Erdos970.ErdosOmissionTail.evenDensity_indicator_integrable line 170
  15. theorem OAI.Erdos970.ErdosOmissionTail.combinedDensity_integrable line 178
  16. theorem OAI.Erdos970.ErdosOmissionTail.combinedDensity_integral line 181
  17. theorem OAI.Erdos970.ErdosOmissionTail.actual_loss_le_scalarTailMass line 192
  18. theorem OAI.Erdos970.ErdosOmissionTail.omissionForce_le_one line 208
  19. theorem OAI.Erdos970.ErdosOmissionTail.freeGate_le_one line 219
  20. theorem OAI.Erdos970.ErdosOmissionTail.gateIterate_force_le_one line 230
  21. theorem OAI.Erdos970.ErdosOmissionTail.terminalBlock_le_one line 238
  22. theorem OAI.Erdos970.ErdosOmissionTail.scalarFreeIterate_le_one line 240
  23. theorem OAI.Erdos970.ErdosOmissionTail.scalar_weighted_bound line 247
  24. theorem OAI.Erdos970.ErdosOmissionTail.scalarTailMass_bounded line 265
  25. theorem OAI.Erdos970.ErdosOmissionTail.scalarTailMass_succ line 278