OAI/Combinatorics/Progressions/Sampling/AllocatedProbabilityGrid.lean

GitHub source file

32 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.Erdos3.VectorPolynomial.allocatedGridAxisScale line 22
  2. theorem OAI.Erdos3.VectorPolynomial.allocatedGridAxisScale_bounds line 26
  3. def OAI.Erdos3.VectorPolynomial.allocatedGridNormalizedRows line 40
  4. def OAI.Erdos3.VectorPolynomial.allocatedGridJetFactorInterpolation line 53
  5. def OAI.Erdos3.VectorPolynomial.allocatedGridJetInterpolation line 62
  6. theorem OAI.Erdos3.VectorPolynomial.allocatedGridJetFactorInterpolation_grid line 65
  7. theorem OAI.Erdos3.VectorPolynomial.allocatedGridJetInterpolation_grid line 75
  8. theorem OAI.Erdos3.VectorPolynomial.allocatedGridJetFactorInterpolation_bounds line 82
  9. theorem OAI.Erdos3.VectorPolynomial.allocatedGridJetInterpolation_bounds line 95
  10. theorem OAI.Erdos3.VectorPolynomial.allocatedGridJetInterpolation_uniform_bounds line 129
  11. theorem OAI.Erdos3.VectorPolynomial.allocatedGridJetInterpolation_counting_mass line 146
  12. abbrev OAI.Erdos3.VectorPolynomial.JetAmbientIndex line 178
  13. def OAI.Erdos3.VectorPolynomial.mixedJetAmbientPoint line 189
  14. def OAI.Erdos3.VectorPolynomial.allocatedGridAmbientCoordinates line 194
  15. theorem OAI.Erdos3.VectorPolynomial.allocatedGridAmbientCoordinates_point line 201
  16. theorem OAI.Erdos3.VectorPolynomial.allocatedGridAmbientCoordinates_lipschitz line 215
  17. def OAI.Erdos3.VectorPolynomial.allocatedNormalizedGridFactor line 268
  18. def OAI.Erdos3.VectorPolynomial.allocatedNormalizedGridInterpolation line 274
  19. theorem OAI.Erdos3.VectorPolynomial.allocatedNormalizedGridFactor_bounds line 278
  20. theorem OAI.Erdos3.VectorPolynomial.allocatedNormalizedGridInterpolation_bounds line 287
  21. theorem OAI.Erdos3.VectorPolynomial.allocatedNormalizedGridInterpolation_grid line 316
  22. def OAI.Erdos3.VectorPolynomial.allocatedProbabilityGridDensity line 354
  23. theorem OAI.Erdos3.VectorPolynomial.allocatedProbabilityGridDensity_nonneg line 358
  24. theorem OAI.Erdos3.VectorPolynomial.allocatedProbabilityGridDensity_mass line 362
  25. def OAI.Erdos3.VectorPolynomial.allocatedProbabilityGridFactor line 381
  26. def OAI.Erdos3.VectorPolynomial.allocatedProbabilityGridInterpolation line 387
  27. theorem OAI.Erdos3.VectorPolynomial.allocatedProbabilityGridFactor_grid line 390
  28. theorem OAI.Erdos3.VectorPolynomial.allocatedProbabilityGridInterpolation_grid line 400
  29. theorem OAI.Erdos3.VectorPolynomial.allocatedProbabilityGridFactor_bounds line 407
  30. theorem OAI.Erdos3.VectorPolynomial.allocatedProbabilityGridInterpolation_bounds line 420
  31. theorem OAI.Erdos3.VectorPolynomial.allocatedProbabilityGridInterpolation_uniform_bounds line 454
  32. theorem OAI.Erdos3.VectorPolynomial.allocatedProbabilityGridInterpolation_counting_mass line 471