OAI/Combinatorics/KMedian/Compression/GaussianInputBounds.lean

GitHub source file

13 declarations, 0 contain sorry, 0 declared as axioms

  1. structure OAI.MetricKMedian.Gaussian.ListOperation.Input line 13
  2. def OAI.MetricKMedian.Gaussian.ListOperation.Input.raw line 19
  3. abbrev OAI.MetricKMedian.Gaussian.ListOperation.Input.encode line 21
  4. theorem OAI.MetricKMedian.Gaussian.ListOperation.input_bounds line 23
  5. theorem OAI.MetricKMedian.Gaussian.ListOperation.residualHeight_mono line 42
  6. theorem OAI.MetricKMedian.Gaussian.ListOperation.returnHeight_mono line 47
  7. theorem OAI.MetricKMedian.Gaussian.ListOperation.input_audit line 53
  8. def OAI.MetricKMedian.Gaussian.ListOperation.residualPolynomial line 73
  9. def OAI.MetricKMedian.Gaussian.ListOperation.returnPolynomial line 74
  10. def OAI.MetricKMedian.Gaussian.ListOperation.statePolynomial line 75
  11. theorem OAI.MetricKMedian.Gaussian.ListOperation.residualPolynomial_eval line 83
  12. theorem OAI.MetricKMedian.Gaussian.ListOperation.returnPolynomial_eval line 85
  13. theorem OAI.MetricKMedian.Gaussian.ListOperation.statePolynomial_eval line 87