OAI/Combinatorics/Progressions/Estimates/PreparedFiniteNestedSourceArrays.lean

GitHub source file

19 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.Erdos3.VectorPolynomial.preparedFiniteForwardInnerSourceExponent line 14
  2. theorem OAI.Erdos3.VectorPolynomial.preparedFiniteForwardInnerSourceExponent_pos line 17
  3. def OAI.Erdos3.VectorPolynomial.preparedFiniteForwardInnerSourceProfile line 41
  4. def OAI.Erdos3.VectorPolynomial.preparedFiniteForwardResourceLayerInnerSourceProfile line 164
  5. def OAI.Erdos3.VectorPolynomial.preparedFiniteForwardActualLocalMaster line 267
  6. def OAI.Erdos3.VectorPolynomial.preparedFiniteForwardActualInnerSourceProfile line 308
  7. def OAI.Erdos3.VectorPolynomial.preparedFiniteForwardActualResourceLayerInnerSourceProfile line 402
  8. def OAI.Erdos3.VectorPolynomial.preparedFiniteNestedSourceSliceExponent line 475
  9. def OAI.Erdos3.VectorPolynomial.preparedFiniteNestedSourceNativeExponent line 479
  10. def OAI.Erdos3.VectorPolynomial.preparedFiniteNestedSourceExponent line 484
  11. theorem OAI.Erdos3.VectorPolynomial.preparedFiniteNestedSourceSliceExponent_bounds line 492
  12. theorem OAI.Erdos3.VectorPolynomial.preparedFiniteNestedSourceExponent_bounds line 506
  13. def OAI.Erdos3.VectorPolynomial.preparedFiniteNestedResourceLayerSourceExponent line 541
  14. theorem OAI.Erdos3.VectorPolynomial.preparedFiniteNestedResourceLayerSourceExponent_bounds line 548
  15. theorem OAI.Erdos3.VectorPolynomial.preparedFiniteNestedResourceLayerSourceSliceExponent_bounds line 575
  16. def OAI.Erdos3.VectorPolynomial.preparedFiniteNestedSourceMaster line 592
  17. def OAI.Erdos3.VectorPolynomial.preparedFiniteNestedSourceNative line 622
  18. theorem OAI.Erdos3.VectorPolynomial.preparedFiniteNestedSourceMaster_front line 635
  19. theorem OAI.Erdos3.VectorPolynomial.preparedFiniteNestedSourceMaster_direct line 649