OAI/NumberTheory/Jacobsthal/Analysis/ActualLossDensity.lean

GitHub source file

13 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.Erdos970.ErdosContinuousOmission.sourceWeight line 18
  2. def OAI.Erdos970.ErdosContinuousOmission.sourceDomain line 22
  3. def OAI.Erdos970.ErdosContinuousOmission.lossDensity line 26
  4. def OAI.Erdos970.ErdosContinuousOmission.omissionDensity line 28
  5. theorem OAI.Erdos970.ErdosContinuousOmission.sourceWeight_nonnegative line 31
  6. theorem OAI.Erdos970.ErdosContinuousOmission.omissionDensity_continuous line 37
  7. theorem OAI.Erdos970.ErdosContinuousOmission.omissionDensity_nonnegative line 44
  8. theorem OAI.Erdos970.ErdosContinuousOmission.lossDensity_nonnegative line 49
  9. theorem OAI.Erdos970.ErdosContinuousOmission.lossDensity_hasSum line 53
  10. theorem OAI.Erdos970.ErdosContinuousOmission.lossDensity_even line 57
  11. theorem OAI.Erdos970.ErdosContinuousOmission.lossDensity_odd line 62
  12. theorem OAI.Erdos970.ErdosContinuousOmission.lossDensity_integrable line 67
  13. theorem OAI.Erdos970.ErdosContinuousOmission.actual_loss_integral line 80