OAI/NumberTheory/Jacobsthal/Analysis/CorrectedCompactTransfer.lean

GitHub source file

33 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.Erdos970.NumberTheoryLean.SignedCompactTransfer.primeExpectation line 22
  2. def OAI.Erdos970.NumberTheoryLean.SignedCompactTransfer.continuousExpectation line 25
  3. theorem OAI.Erdos970.NumberTheoryLean.SignedCompactTransfer.actual_signed_difference line 33
  4. theorem OAI.Erdos970.NumberTheoryLean.SignedCompactTransfer.source_signed_compact_transfer line 68
  5. def OAI.Erdos970.NumberTheoryLean.CompactInverseTest.lowerRatio line 113
  6. theorem OAI.Erdos970.NumberTheoryLean.CompactInverseTest.valid_lower line 115
  7. def OAI.Erdos970.NumberTheoryLean.CompactInverseTest.safeWeight line 117
  8. theorem OAI.Erdos970.NumberTheoryLean.CompactInverseTest.safeWeight_pos line 119
  9. theorem OAI.Erdos970.NumberTheoryLean.CompactInverseTest.safeWeight_eq line 122
  10. theorem OAI.Erdos970.NumberTheoryLean.CompactInverseTest.safeWeight_continuous line 126
  11. def OAI.Erdos970.NumberTheoryLean.CompactInverseTest.inverseTest line 135
  12. theorem OAI.Erdos970.NumberTheoryLean.CompactInverseTest.inverseTest_continuous line 138
  13. theorem OAI.Erdos970.NumberTheoryLean.CompactInverseTest.inverseTest_compact line 143
  14. theorem OAI.Erdos970.NumberTheoryLean.CompactInverseTest.inverseTest_uniform line 152
  15. theorem OAI.Erdos970.NumberTheoryLean.CompactInverseTest.inverseTest_bounded line 157
  16. theorem OAI.Erdos970.NumberTheoryLean.CompactInverseTest.inverseTest_gap_support line 172
  17. theorem OAI.Erdos970.NumberTheoryLean.CompactInverseTest.inverseTest_eq line 178
  18. theorem OAI.Erdos970.NumberTheoryLean.CompactInverseTest.prime_inverseTest_eq line 182
  19. def OAI.Erdos970.NumberTheoryLean.CompactNormalizationCorrection.correctedTest line 203
  20. def OAI.Erdos970.NumberTheoryLean.CompactNormalizationCorrection.correctedExpectation line 207
  21. theorem OAI.Erdos970.NumberTheoryLean.CompactNormalizationCorrection.correctedTest_measurable line 210
  22. theorem OAI.Erdos970.NumberTheoryLean.CompactNormalizationCorrection.correction_difference_bound line 213
  23. theorem OAI.Erdos970.NumberTheoryLean.CompactNormalizationCorrection.correctedTest_bound line 235
  24. theorem OAI.Erdos970.NumberTheoryLean.CompactNormalizationCorrection.actual_compact_correction line 253
  25. def OAI.Erdos970.NumberTheoryLean.ContinuousCompactHighError.baseReward line 309
  26. def OAI.Erdos970.NumberTheoryLean.ContinuousCompactHighError.inverseReward line 312
  27. theorem OAI.Erdos970.NumberTheoryLean.ContinuousCompactHighError.baseReward_measurable line 315
  28. theorem OAI.Erdos970.NumberTheoryLean.ContinuousCompactHighError.inverseReward_measurable line 319
  29. theorem OAI.Erdos970.NumberTheoryLean.ContinuousCompactHighError.inverseReward_abs line 323
  30. theorem OAI.Erdos970.NumberTheoryLean.ContinuousCompactHighError.phase_compact_bound line 334
  31. theorem OAI.Erdos970.NumberTheoryLean.ContinuousCompactHighError.compact_high_error_bound line 349
  32. theorem OAI.Erdos970.NumberTheoryLean.CorrectedCompactTransfer.source_corrected_compact_transfer line 391
  33. theorem OAI.Erdos970.NumberTheoryLean.CorrectedCompactTransfer.source_inverse_compact_transfer line 425