OAI/Combinatorics/KMedianRecovery/Sampling/SamplerWeights.lean

GitHub source file

33 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.MetricKMedianRecovery.BitMachine.BinarySampler.Weights.stateInput line 10
  2. def OAI.MetricKMedianRecovery.BitMachine.BinarySampler.Weights.stateInput_computes line 11
  3. lemma OAI.MetricKMedianRecovery.BitMachine.BinarySampler.Weights.stateInput_some line 13
  4. def OAI.MetricKMedianRecovery.BitMachine.BinarySampler.Weights.context line 17
  5. def OAI.MetricKMedianRecovery.BitMachine.BinarySampler.Weights.context_computes line 19
  6. def OAI.MetricKMedianRecovery.BitMachine.BinarySampler.Weights.actionField line 23
  7. def OAI.MetricKMedianRecovery.BitMachine.BinarySampler.Weights.actionField_computes line 24
  8. def OAI.MetricKMedianRecovery.BitMachine.BinarySampler.Weights.kind line 25
  9. def OAI.MetricKMedianRecovery.BitMachine.BinarySampler.Weights.kind_computes line 26
  10. def OAI.MetricKMedianRecovery.BitMachine.BinarySampler.Weights.active line 28
  11. def OAI.MetricKMedianRecovery.BitMachine.BinarySampler.Weights.active_computes line 30
  12. def OAI.MetricKMedianRecovery.BitMachine.BinarySampler.Weights.base line 32
  13. def OAI.MetricKMedianRecovery.BitMachine.BinarySampler.Weights.base_computes line 34
  14. def OAI.MetricKMedianRecovery.BitMachine.BinarySampler.Weights.weight line 37
  15. def OAI.MetricKMedianRecovery.BitMachine.BinarySampler.Weights.weight_computes line 41
  16. lemma OAI.MetricKMedianRecovery.BitMachine.BinarySampler.Weights.state_none line 50
  17. lemma OAI.MetricKMedianRecovery.BitMachine.BinarySampler.Weights.state_some_ne line 51
  18. lemma OAI.MetricKMedianRecovery.BitMachine.BinarySampler.Weights.weight_pair line 53
  19. def OAI.MetricKMedianRecovery.BitMachine.BinarySampler.Client.row line 85
  20. def OAI.MetricKMedianRecovery.BitMachine.BinarySampler.Client.row_computes line 86
  21. def OAI.MetricKMedianRecovery.BitMachine.BinarySampler.Client.distances line 87
  22. def OAI.MetricKMedianRecovery.BitMachine.BinarySampler.Client.distances_computes line 88
  23. def OAI.MetricKMedianRecovery.BitMachine.BinarySampler.Client.population line 89
  24. def OAI.MetricKMedianRecovery.BitMachine.BinarySampler.Client.population_computes line 90
  25. def OAI.MetricKMedianRecovery.BitMachine.BinarySampler.Client.near line 93
  26. def OAI.MetricKMedianRecovery.BitMachine.BinarySampler.Client.near_computes line 94
  27. def OAI.MetricKMedianRecovery.BitMachine.BinarySampler.Client.radii line 95
  28. def OAI.MetricKMedianRecovery.BitMachine.BinarySampler.Client.radii_computes line 96
  29. lemma OAI.MetricKMedianRecovery.BitMachine.BinarySampler.Client.row_pair line 98
  30. lemma OAI.MetricKMedianRecovery.BitMachine.BinarySampler.Client.distances_pair line 101
  31. lemma OAI.MetricKMedianRecovery.BitMachine.BinarySampler.Client.population_pair line 107
  32. lemma OAI.MetricKMedianRecovery.BitMachine.BinarySampler.Client.near_pair line 113
  33. lemma OAI.MetricKMedianRecovery.BitMachine.BinarySampler.Client.radii_pair line 119