OAI/Combinatorics/Progressions/Sampling/ForecastJointScaleNormalization.lean

GitHub source file

25 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.Erdos3.VectorPolynomial.forecastJointGridScale line 16
  2. def OAI.Erdos3.VectorPolynomial.forecastJointGridCenter line 20
  3. theorem OAI.Erdos3.VectorPolynomial.forecastJointGridScale_pos line 25
  4. theorem OAI.Erdos3.VectorPolynomial.forecastJointGridScale_mesh line 37
  5. theorem OAI.Erdos3.VectorPolynomial.forecastJointGridScale_prod line 56
  6. theorem OAI.Erdos3.VectorPolynomial.forecastJointGridScale_prod_eq_card line 68
  7. theorem OAI.Erdos3.VectorPolynomial.forecastJointGridScale_prod_div_card line 75
  8. theorem OAI.Erdos3.VectorPolynomial.forecastJointGrid_normalized_join line 87
  9. def OAI.Erdos3.forecastJointGridSamplerLog line 105
  10. def OAI.Erdos3.forecastJointGridAmbientLog line 108
  11. def OAI.Erdos3.forecastJointGridSamplerFloor line 111
  12. theorem OAI.Erdos3.forecastJointGridSamplerFloor_lower line 114
  13. theorem OAI.Erdos3.forecastJointGridSamplerFloor_pos line 118
  14. theorem OAI.Erdos3.forecastJointGridSamplerFloor_le_exp line 122
  15. theorem OAI.Erdos3.forecastGrid_exp_div_le line 136
  16. theorem OAI.Erdos3.VectorPolynomial.forecastJointGridScale_mesh_of_exp_bounds line 160
  17. theorem OAI.Erdos3.VectorPolynomial.forecastJointGridScale_mesh_of_floor line 206
  18. theorem OAI.Erdos3.VectorPolynomial.forecastJacobian_product_le_exp line 232
  19. def OAI.Erdos3.VectorPolynomial.forecastGeometricJacobian line 244
  20. theorem OAI.Erdos3.VectorPolynomial.forecastGeometricJacobian_pos line 253
  21. theorem OAI.Erdos3.VectorPolynomial.forecastGeometricJacobian_cancel line 263
  22. theorem OAI.Erdos3.VectorPolynomial.forecastGeometricJacobian_le_exp line 273
  23. theorem OAI.Erdos3.VectorPolynomial.forecastGeometricJacobian_uniform_le_exp line 335
  24. theorem OAI.Erdos3.VectorPolynomial.forecastJointScale_normalization line 376
  25. theorem OAI.Erdos3.VectorPolynomial.forecastJointScale_complex_normalization line 387