OAI/Analysis/IrrationalRotation/Model/ScalarSamplingEstimates.lean

GitHub source file

11 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.Invariant233.ScalarSampling.samplingHorizon line 12
  2. def OAI.Invariant233.ScalarSampling.bvSize line 14
  3. def OAI.Invariant233.ScalarSampling.SeparatedPowers line 18
  4. structure OAI.Invariant233.ScalarSampling.SamplingPair line 23
  5. def OAI.Invariant233.ScalarSampling.rectangleProbability line 34
  6. def OAI.Invariant233.ScalarSampling.RectangleEstimate line 39
  7. def OAI.Invariant233.ScalarSampling.BVEstimate line 45
  8. def OAI.Invariant233.ScalarSampling.AllKernelEstimates line 54
  9. def OAI.Invariant233.ScalarSampling.AllMarginalEstimates line 59
  10. def OAI.Invariant233.ScalarSampling.AllSeparatedEstimates line 69
  11. structure OAI.Invariant233.ScalarSampling.ScalarSamplingEstimates line 75