OAI/NumberTheory/Jacobsthal/Harmonic/CompactAnomalyTest.lean

GitHub source file

19 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.Erdos970.ErdosContinuousAnomaly.continuousBoundaryCorrection line 19
  2. theorem OAI.Erdos970.ErdosContinuousAnomaly.boundaryCorrection_difference line 23
  3. theorem OAI.Erdos970.ErdosContinuousAnomaly.actual_anomaly_replacement line 30
  4. def OAI.Erdos970.ErdosContinuousAnomaly.sideSign line 77
  5. theorem OAI.Erdos970.ErdosContinuousAnomaly.terminal_side_sign line 79
  6. theorem OAI.Erdos970.ErdosContinuousAnomaly.source_parity_sign line 90
  7. def OAI.Erdos970.ErdosContinuousAnomaly.signedAnomaly line 94
  8. theorem OAI.Erdos970.ErdosContinuousAnomaly.continuousBoundaryCorrection_eq_state_reward line 96
  9. def OAI.Erdos970.ErdosCorrectionOccupation.extendedSignedAnomaly line 117
  10. theorem OAI.Erdos970.ErdosCorrectionOccupation.extendedSignedAnomaly_continuous line 120
  11. theorem OAI.Erdos970.ErdosCorrectionOccupation.extendedSignedAnomaly_eq line 125
  12. def OAI.Erdos970.ErdosCorrectionOccupation.compactCutoff line 129
  13. theorem OAI.Erdos970.ErdosCorrectionOccupation.compactCutoff_spec line 132
  14. def OAI.Erdos970.ErdosCorrectionOccupation.compactAnomalyTest line 138
  15. theorem OAI.Erdos970.ErdosCorrectionOccupation.compactAnomalyTest_continuous line 141
  16. theorem OAI.Erdos970.ErdosCorrectionOccupation.compactAnomalyTest_compact line 144
  17. theorem OAI.Erdos970.ErdosCorrectionOccupation.compactAnomalyTest_support line 147
  18. theorem OAI.Erdos970.ErdosCorrectionOccupation.compactAnomalyTest_eq line 152
  19. theorem OAI.Erdos970.ErdosCorrectionOccupation.compactAnomalyTest_error line 158