OAI/Analysis/RotationWeights/Thresholds.lean

GitHub source file

30 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.CircleSampling.blockScale line 83
  2. def OAI.CircleSampling.blockRange line 84
  3. lemma OAI.CircleSampling.blockScale_pos line 85
  4. lemma OAI.CircleSampling.blockRange_ge_length line 86
  5. lemma OAI.CircleSampling.bridge_overlap line 91
  6. lemma OAI.CircleSampling.bridge_below_scale line 93
  7. lemma OAI.CircleSampling.scale_below_range line 99
  8. lemma OAI.CircleSampling.exists_large_range line 107
  9. def OAI.CircleSampling.crossingThreshold line 133
  10. def OAI.CircleSampling.stageCrossingWidth line 134
  11. def OAI.CircleSampling.stageCrossingProbability line 135
  12. lemma OAI.CircleSampling.coordinatePhase_bounds line 137
  13. lemma OAI.CircleSampling.stageCrossingProbability_eq line 141
  14. lemma OAI.CircleSampling.stageCrossingWidth_eq line 145
  15. lemma OAI.CircleSampling.stageCrossingProbability_nonneg line 149
  16. lemma OAI.CircleSampling.stageCrossingProbability_le_one line 151
  17. lemma OAI.CircleSampling.stage_range_strength line 155
  18. lemma OAI.CircleSampling.stage_bridge_strength line 170
  19. lemma OAI.CircleSampling.threshold_bounds_of_abs line 180
  20. lemma OAI.CircleSampling.bridge_thresholds line 196
  21. lemma OAI.CircleSampling.large_thresholds line 222
  22. def OAI.CircleSampling.regularSamples line 257
  23. lemma OAI.CircleSampling.ae_regularSamples line 260
  24. lemma OAI.CircleSampling.actual_Xi_tail line 265
  25. lemma OAI.CircleSampling.regular_order line 275
  26. lemma OAI.CircleSampling.crossing_decay line 279
  27. lemma OAI.CircleSampling.stage_masks line 287
  28. lemma OAI.CircleSampling.large_masks line 323
  29. lemma OAI.CircleSampling.tagged_coordinate_extreme line 342
  30. lemma OAI.CircleSampling.short_ratio line 377