OAI/Combinatorics/Progressions/Estimates/PreparedFiniteScheduleLocalScalarConstruction.lean

GitHub source file

21 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.Erdos3.VectorPolynomial.PreparedFiniteScheduleGeometryPrescribedScaleStatement line 12
  2. theorem OAI.Erdos3.VectorPolynomial.exists_preparedFiniteScheduleGeometryPrescribedScale line 54
  3. def OAI.Erdos3.VectorPolynomial.preparedFiniteScheduleDirectMaster line 127
  4. def OAI.Erdos3.VectorPolynomial.preparedFiniteScheduleDirectCoarse line 134
  5. theorem OAI.Erdos3.VectorPolynomial.preparedFiniteScheduleDirectScalarBounds_explicit line 138
  6. theorem OAI.Erdos3.VectorPolynomial.preparedFiniteScheduleDirectCoarse_requested line 287
  7. theorem OAI.Erdos3.VectorPolynomial.exists_preparedEmptyLayerFiniteScheduleDirectSource line 302
  8. abbrev OAI.Erdos3.VectorPolynomial.PreparedFiniteForwardSlot line 467
  9. def OAI.Erdos3.VectorPolynomial.preparedFiniteForwardSlotDegree line 469
  10. def OAI.Erdos3.VectorPolynomial.preparedFiniteForwardModelSlot line 472
  11. def OAI.Erdos3.VectorPolynomial.preparedFiniteForwardDetectionSlot line 475
  12. theorem OAI.Erdos3.VectorPolynomial.preparedFiniteForwardModelSlot_degree line 478
  13. theorem OAI.Erdos3.VectorPolynomial.preparedFiniteForwardDetectionSlot_degree line 481
  14. theorem OAI.Erdos3.VectorPolynomial.preparedFiniteForwardSlot_degree_le line 484
  15. theorem OAI.Erdos3.VectorPolynomial.preparedFiniteForwardSlot_card line 491
  16. theorem OAI.Erdos3.VectorPolynomial.preparedFiniteForwardSourceSlots_inputs line 495
  17. theorem OAI.Erdos3.VectorPolynomial.exists_preparedFiniteForwardSourceSlots_budget line 524
  18. def OAI.Erdos3.VectorPolynomial.preparedFiniteScheduleLocalPhysical line 549
  19. def OAI.Erdos3.VectorPolynomial.preparedFiniteScheduleLocalMaster line 553
  20. theorem OAI.Erdos3.VectorPolynomial.PreparedUniformDegreeDirectScalarBounds.late_mono line 558
  21. theorem OAI.Erdos3.VectorPolynomial.preparedFiniteScheduleLocalScalarBounds_explicit line 575