OAI/Analysis/RotationWeights/SamplingStage.lean

GitHub source file

21 declarations, 0 contain sorry, 0 declared as axioms

  1. lemma OAI.CircleSampling.exists_sampling_stage line 53
  2. theorem OAI.ContinuousCircleWeight.exists_nonzero_low_product_coefficient line 159
  3. def OAI.ContinuousCircleWeight.shiftedPolynomial line 171
  4. theorem OAI.ContinuousCircleWeight.coeff_shiftedPolynomial line 174
  5. theorem OAI.ContinuousCircleWeight.continuous_coeff_shiftedPolynomial line 181
  6. abbrev OAI.ContinuousCircleWeight.CoefficientPair line 189
  7. def OAI.ContinuousCircleWeight.lowProduct line 192
  8. theorem OAI.ContinuousCircleWeight.continuous_lowProduct line 195
  9. def OAI.ContinuousCircleWeight.centerIndex line 204
  10. theorem OAI.ContinuousCircleWeight.lowProduct_ne_zero line 206
  11. theorem OAI.ContinuousCircleWeight.finite_coefficient_bound line 220
  12. def OAI.CircleSampling.nextWindow line 265
  13. def OAI.CircleSampling.kappa line 266
  14. lemma OAI.CircleSampling.kappa_pos line 268
  15. lemma OAI.CircleSampling.kappa_le line 269
  16. lemma OAI.CircleSampling.exists_exponential_budget line 274
  17. lemma OAI.CircleSampling.exists_bridge_budget line 285
  18. lemma OAI.CircleSampling.eventually_nextWindow_superlinear line 292
  19. lemma OAI.CircleSampling.eventually_nextWindow_overlap line 300
  20. def OAI.CircleSampling.StageNumerics line 317
  21. lemma OAI.CircleSampling.eventually_StageNumerics line 324