OAI/Combinatorics/Progressions/Linear/ActualCandidateSlowProjectionMass.lean

GitHub source file

33 declarations, 0 contain sorry, 0 declared as axioms

  1. theorem OAI.Erdos3.VectorPolynomial.fullTaggedRealMatrixProjection_single line 17
  2. theorem OAI.Erdos3.VectorPolynomial.fullTaggedRealMatrixProjection_rowSum_le line 22
  3. theorem OAI.Erdos3.VectorPolynomial.fullTaggedRealMatrixProjection_slow_mass_row_le line 36
  4. theorem OAI.Erdos3.VectorPolynomial.fullTaggedRealMatrixProjection_slow_mass_row_le_exp line 48
  5. def OAI.Erdos3.VectorPolynomial.fullTaggedCenteredCoordinates line 89
  6. def OAI.Erdos3.VectorPolynomial.fullTaggedSlowProjectionChart line 95
  7. theorem OAI.Erdos3.VectorPolynomial.fullTaggedSlowProjectionChart_inl line 102
  8. theorem OAI.Erdos3.VectorPolynomial.fullTaggedSlowProjectionChart_inr line 109
  9. theorem OAI.Erdos3.VectorPolynomial.fullTaggedCenteredCoordinates_support line 121
  10. theorem OAI.Erdos3.VectorPolynomial.fullTaggedCenteredCoordinates_top line 134
  11. theorem OAI.Erdos3.VectorPolynomial.fullTaggedSlowProjectionChart_support line 145
  12. theorem OAI.Erdos3.VectorPolynomial.fullTaggedSlowProjectionChart_top line 164
  13. theorem OAI.Erdos3.VectorPolynomial.allocatedRecoveredIntegerFullChart_slowProjection_spatial line 210
  14. theorem OAI.Erdos3.VectorPolynomial.AllocatedCenteredFramedRecoveredSampleAt.integerFullChart_slowProjection_tag line 227
  15. theorem OAI.Erdos3.normalizedMass_neg_linearCombination_le line 260
  16. theorem OAI.Erdos3.VectorPolynomial.allocatedRecoveredIntegerFullChart_slowProjection_spatial_mass line 294
  17. theorem OAI.Erdos3.VectorPolynomial.allocatedRecoveredIntegerFullChart_slowProjection_spatial_mass_of_support line 311
  18. theorem OAI.Erdos3.VectorPolynomial.AllocatedCenteredFramedRecoveredSampleAt.integerFullChart_slowProjection_tag_mass line 344
  19. theorem OAI.Erdos3.VectorPolynomial.AllocatedCenteredFramedRecoveredSampleAt.integerFullChart_slowProjection_mass line 371
  20. theorem OAI.Erdos3.VectorPolynomial.AllocatedCenteredFramedRecoveredSampleAt.integerFullChart_frozen_slowProjection_mass line 432
  21. theorem OAI.Erdos3.VectorPolynomial.fullTaggedSlowProjectionChart_physical_spatial line 485
  22. theorem OAI.Erdos3.VectorPolynomial.fullTaggedSlowProjectionChart_physical_spatial_abs_le_one line 494
  23. theorem OAI.Erdos3.VectorPolynomial.fullTaggedCenteredCoordinates_eval line 523
  24. theorem OAI.Erdos3.VectorPolynomial.fullTaggedSlowProjectionChart_physical_tag line 533
  25. theorem OAI.Erdos3.VectorPolynomial.fullTaggedSlowProjectionChart_physical_tag_abs_le line 557
  26. theorem OAI.Erdos3.VectorPolynomial.fullTaggedSlowProjectionChart_physical_abs_le line 578
  27. theorem OAI.Erdos3.VectorPolynomial.fullTaggedSlowProjectionChart_physical_abs_le_rational line 600
  28. def OAI.Erdos3.actualCandidateSlowProjectionMassBudget line 628
  29. theorem OAI.Erdos3.actualCandidateSlowProjectionMassBudget_two_le line 631
  30. theorem OAI.Erdos3.actualCandidateSlowProjectionMassBudget_one_le line 636
  31. theorem OAI.Erdos3.actualCandidateSlowProjectionMassBudget_max_le line 641
  32. theorem OAI.Erdos3.VectorPolynomial.AllocatedExternalLocalChart.slowProjection_mass line 683
  33. theorem OAI.Erdos3.VectorPolynomial.AllocatedExternalLocalChart.slowProjection_mass_sides line 722