OAI/Combinatorics/Progressions/Sampling/PreparedActualForecastSetup.lean

GitHub source file

35 declarations, 0 contain sorry, 0 declared as axioms

  1. theorem OAI.Erdos3.VectorPolynomial.enlargedPreparedCommonSamplerBlock_single_uniform line 14
  2. theorem OAI.Erdos3.VectorPolynomial.enlargedPreparedCommonSamplerBlock_four line 29
  3. theorem OAI.Erdos3.VectorPolynomial.enlargedPreparedCommonSamplerBlock_transverse_uniform line 38
  4. theorem OAI.Erdos3.principalTupleIndex_block_sum_le_card line 54
  5. theorem OAI.Erdos3.VectorPolynomial.layerSampler_block_sum_le_principal_card line 65
  6. theorem OAI.Erdos3.VectorPolynomial.enlargedPreparedCommonSampler_block_sum_le_principal_card line 73
  7. abbrev OAI.Erdos3.VectorPolynomial.PreparedActualForecastShortIndex line 103
  8. def OAI.Erdos3.VectorPolynomial.preparedActualForecastShortSelection line 105
  9. theorem OAI.Erdos3.VectorPolynomial.preparedActualForecastShortSelection_injective line 109
  10. theorem OAI.Erdos3.VectorPolynomial.preparedActualForecastShortSelection_small line 113
  11. theorem OAI.Erdos3.VectorPolynomial.preparedActualForecastShortSelection_exhaustive line 120
  12. def OAI.Erdos3.VectorPolynomial.preparedActualForecastShortAxisEmbedding line 131
  13. theorem OAI.Erdos3.VectorPolynomial.preparedActualForecastShortIndex_card_le_axes line 139
  14. theorem OAI.Erdos3.VectorPolynomial.preparedActualForecastShortIndex_card_le_sum line 144
  15. theorem OAI.Erdos3.VectorPolynomial.preparedActualForecastShortIndex_card_le line 148
  16. theorem OAI.Erdos3.VectorPolynomial.preparedActualForecastShortSelection_inverse_bound line 153
  17. theorem OAI.Erdos3.VectorPolynomial.enlargedPreparedActualForecastShortSelection_nonempty line 172
  18. def OAI.Erdos3.VectorPolynomial.preparedActualForecastGridVolume line 203
  19. theorem OAI.Erdos3.VectorPolynomial.preparedActualForecastGridVolume_one_le line 208
  20. theorem OAI.Erdos3.VectorPolynomial.preparedActualForecastGridVolume_pos line 217
  21. theorem OAI.Erdos3.VectorPolynomial.preparedActualForecastJacobian_budget line 223
  22. abbrev OAI.Erdos3.VectorPolynomial.preparedForecastGridVolume line 262
  23. theorem OAI.Erdos3.VectorPolynomial.preparedForecastGridVolume_one_le line 265
  24. theorem OAI.Erdos3.VectorPolynomial.preparedForecastGridVolume_pos line 270
  25. theorem OAI.Erdos3.VectorPolynomial.preparedForecastGridJacobian_budget line 278
  26. theorem OAI.Erdos3.VectorPolynomial.preparedActualForecastGridVolume_mul_active_heights line 316
  27. theorem OAI.Erdos3.VectorPolynomial.preparedActualForecastGridVolume_eq_allocated_product line 355
  28. theorem OAI.Erdos3.VectorPolynomial.preparedActualForecastJacobian_eq_ratio line 382
  29. theorem OAI.Erdos3.VectorPolynomial.ratioJacobian_product_le_exp line 426
  30. theorem OAI.Erdos3.VectorPolynomial.preparedActualForecastJacobian_ratio_le_exp line 433
  31. theorem OAI.Erdos3.VectorPolynomial.preparedActualForecastJacobian_ratio_uniform_le_exp line 485
  32. theorem OAI.Erdos3.VectorPolynomial.preparedActualForecastJacobian_ratio_budget line 518
  33. theorem OAI.Erdos3.VectorPolynomial.forecastRows_one_le line 597
  34. theorem OAI.Erdos3.VectorPolynomial.preparedActualForecast_radius_bounds line 602
  35. def OAI.Erdos3.VectorPolynomial.preparedActualForecastSetup line 647