OAI/Combinatorics/Progressions/Sampling/AllocatedActiveGridPlateau.lean

GitHub source file

22 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.Erdos3.VectorPolynomial.allocatedGridAxisWindowVolume line 17
  2. theorem OAI.Erdos3.VectorPolynomial.allocatedGridAxisWindowVolume_nonneg line 20
  3. def OAI.Erdos3.VectorPolynomial.allocatedGridFamilyWindowVolume line 26
  4. theorem OAI.Erdos3.VectorPolynomial.allocatedGridFamilyWindowVolume_nonneg line 30
  5. theorem OAI.Erdos3.VectorPolynomial.allocatedSelectedWindowVolume_le line 37
  6. def OAI.Erdos3.VectorPolynomial.allocatedGridIntegerAxis line 82
  7. theorem OAI.Erdos3.VectorPolynomial.allocatedGridIntegerAxis_grid line 89
  8. theorem OAI.Erdos3.VectorPolynomial.allocatedGridIntegerAxis_injective line 96
  9. def OAI.Erdos3.VectorPolynomial.allocatedActiveGrid line 105
  10. def OAI.Erdos3.VectorPolynomial.allocatedGridIntegerValues line 111
  11. def OAI.Erdos3.VectorPolynomial.allocatedGridNaturalScale line 117
  12. theorem OAI.Erdos3.VectorPolynomial.allocatedGridNaturalScale_pos line 124
  13. def OAI.Erdos3.VectorPolynomial.allocatedGridNaturalWindow line 127
  14. theorem OAI.Erdos3.VectorPolynomial.allocatedGridNaturalWindow_outside line 135
  15. theorem OAI.Erdos3.VectorPolynomial.allocatedGridNaturalWindow_card_le line 146
  16. def OAI.Erdos3.VectorPolynomial.allocatedActiveNaturalVolume line 160
  17. theorem OAI.Erdos3.VectorPolynomial.allocatedActiveNaturalVolume_pos line 165
  18. theorem OAI.Erdos3.VectorPolynomial.allocatedActiveWindow_volume line 170
  19. theorem OAI.Erdos3.VectorPolynomial.allocatedSupportedGridJetPMF_integer line 205
  20. def OAI.Erdos3.VectorPolynomial.allocatedActivePlateauAxis line 219
  21. theorem OAI.Erdos3.VectorPolynomial.allocatedActivePlateauAxis_zero line 224
  22. theorem OAI.Erdos3.VectorPolynomial.allocatedActivePlateauAxis_estimates line 238