OAI/Combinatorics/Progressions/Estimates/AllocatedSlicedCoveredComparison.lean

GitHub source file

16 declarations, 0 contain sorry, 0 declared as axioms

  1. theorem OAI.Erdos3.VectorPolynomial.allocatedFixedKernel_refined_principal_comparison line 36
  2. theorem OAI.Erdos3.VectorPolynomial.measurable_dependent_row_product line 100
  3. theorem OAI.Erdos3.VectorPolynomial.allocatedLongJetTarget_row_measurable line 126
  4. def OAI.Erdos3.VectorPolynomial.allocatedLongJetProxy line 151
  5. theorem OAI.Erdos3.VectorPolynomial.allocatedLongJetProxy_measurable line 157
  6. def OAI.Erdos3.VectorPolynomial.allocatedLongJetRealCoordinates line 204
  7. theorem OAI.Erdos3.VectorPolynomial.allocatedLongJetTarget_normalized line 209
  8. theorem OAI.Erdos3.VectorPolynomial.allocatedLongJetProxy_continuous line 217
  9. theorem OAI.Erdos3.VectorPolynomial.allocatedLongJet_l1_comparison line 286
  10. theorem OAI.Erdos3.VectorPolynomial.allocatedLongJet_test_comparison line 319
  11. theorem OAI.Erdos3.VectorPolynomial.allocatedLongJetMask_eq_of_periods line 357
  12. theorem OAI.Erdos3.VectorPolynomial.allocatedLongJetProxy_eq_of_periods line 378
  13. theorem OAI.Erdos3.VectorPolynomial.allocatedFixedKernel_refined_pointwise line 428
  14. theorem OAI.Erdos3.VectorPolynomial.allocatedPhysicalCovered_test_comparison_of_l1 line 529
  15. theorem OAI.Erdos3.VectorPolynomial.allocatedPhysicalCovered_test_comparison line 552
  16. theorem OAI.Erdos3.VectorPolynomial.allocatedSlicedPhysicalCovered_test_comparison_of_l1 line 631