OAI/Combinatorics/Progressions/Linear/AllocatedCenteredMeasurableFramedBadTail.lean

GitHub source file

25 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.Erdos3.VectorPolynomial.allocatedJointFrameRead line 14
  2. theorem OAI.Erdos3.VectorPolynomial.allocatedJointFrameRead_noise line 21
  3. theorem OAI.Erdos3.VectorPolynomial.allocatedJointFrameRead_noise_some line 29
  4. theorem OAI.Erdos3.VectorPolynomial.allocatedJointFrameRead_deck line 35
  5. theorem OAI.Erdos3.VectorPolynomial.allocatedJointFrameRead_projection line 39
  6. theorem OAI.Erdos3.VectorPolynomial.allocatedJointFrameRead_reduce line 43
  7. theorem OAI.Erdos3.VectorPolynomial.allocatedOriginalCongruenceTop_congr_slopes line 56
  8. theorem OAI.Erdos3.VectorPolynomial.allocatedResidueModulusBad_congr_slopes line 81
  9. theorem OAI.Erdos3.VectorPolynomial.allocatedActualModulusBad_jointFrame line 93
  10. theorem OAI.Erdos3.VectorPolynomial.allocatedJointFrameRead_rankBad line 105
  11. theorem OAI.Erdos3.VectorPolynomial.allocatedJointFrameRead_badDepth line 130
  12. theorem OAI.Erdos3.VectorPolynomial.allocatedReplaceReadNoise_eq_jointFrame line 161
  13. theorem OAI.Erdos3.VectorPolynomial.allocatedReplaceReadNoise_modulusBad line 182
  14. theorem OAI.Erdos3.VectorPolynomial.allocatedReplaceReadNoise_primeBad line 195
  15. theorem OAI.Erdos3.VectorPolynomial.allocatedActualPrimeBad_jointFrame line 228
  16. theorem OAI.Erdos3.VectorPolynomial.allocatedActualPrimeBad_depth_jointFrame line 235
  17. theorem OAI.Erdos3.VectorPolynomial.allocatedActualPrimeBad_product_jointFrame line 243
  18. theorem OAI.Erdos3.VectorPolynomial.AllocatedCenteredRecoveredSampleReadAt.jointFrame line 278
  19. theorem OAI.Erdos3.VectorPolynomial.AllocatedCenteredRecoveredSampleReadAt.centeredJointFrame_read line 343
  20. theorem OAI.Erdos3.VectorPolynomial.AllocatedCenteredRecoveredSampleReadAt.centeredJointFrame_cover line 353
  21. theorem OAI.Erdos3.VectorPolynomial.AllocatedCenteredRecoveredSampleReadAt.centeredJointFrame_recovery line 381
  22. theorem OAI.Erdos3.VectorPolynomial.allocatedCentered_joint_weight_measurable line 471
  23. theorem OAI.Erdos3.VectorPolynomial.allocatedCentered_joint_positive_rankCertificate line 481
  24. theorem OAI.Erdos3.VectorPolynomial.exists_allocatedCentered_measurable_unframed_bad_tail line 495
  25. theorem OAI.Erdos3.VectorPolynomial.exists_allocatedCentered_measurable_framed_bad_tail line 520