OAI/Probability/CoordinateSweeps/Perturbation.lean

GitHub source file

24 declarations, 0 contain sorry, 0 declared as axioms

All definitions are finite and use the source's ordinary probability and trace normalizations.

  1. structure OAI.CoordinateSweeps.SparseScalar.SizeReady line 63

    Also declared: ComparatorChallenges/CoordinateSweeps.lean:272 (same declaration text).

  2. lemma OAI.CoordinateSweeps.SparseScalar.eventually_sizeReady line 73
  3. structure OAI.CoordinateSweeps.SparseScalar.ScaleReady line 81

    Also declared: ComparatorChallenges/CoordinateSweeps.lean:283 (same declaration text).

  4. lemma OAI.CoordinateSweeps.SparseScalar.eventually_scaleReady line 86
  5. def OAI.CoordinateSweeps.SparseScalar.slack line 100

    Source comment

    Positive slack used by the uniform finite real perturbation.

    Also declared: ComparatorChallenges/CoordinateSweeps.lean:289 (same declaration text).

    def slack (s : ℝ) : ℝ :=
…
  6. lemma OAI.CoordinateSweeps.SparseScalar.slack_pos line 102
  7. lemma OAI.CoordinateSweeps.SparseScalar.slack_le_gap line 108
  8. lemma OAI.CoordinateSweeps.Grid.pow_r_le_size line 124
  9. lemma OAI.CoordinateSweeps.Grid.sizeReady line 129
  10. lemma OAI.CoordinateSweeps.Grid.sparse_uniform_room line 131
  11. lemma OAI.CoordinateSweeps.Grid.sparse_many_room line 149
  12. lemma OAI.CoordinateSweeps.Grid.Holes.lineLaw_zero line 169
  13. lemma OAI.CoordinateSweeps.Grid.Holes.sparse_uniform_norm line 172
  14. lemma OAI.CoordinateSweeps.Grid.Holes.sparse_many_norm line 192
  15. structure OAI.CoordinateSweeps.SparseDimension.Level line 217
  16. lemma OAI.CoordinateSweeps.SparseDimension.exists_level line 227
  17. lemma OAI.CoordinateSweeps.SparseDimension.level_log_bounds line 243
  18. lemma OAI.CoordinateSweeps.Grid.Holes.level_uniform_norm line 266
  19. lemma OAI.CoordinateSweeps.Grid.Holes.level_many_norm line 280
  20. lemma OAI.CoordinateSweeps.baseZeta_le_inv_card line 301
  21. lemma OAI.CoordinateSweeps.lineLaw_base_bounds line 309
  22. def OAI.CoordinateSweeps.SparsePerturb line 316

    Also declared: ComparatorChallenges/CoordinateSweeps.lean:294 (same declaration text).

  23. lemma OAI.CoordinateSweeps.exists_sparsePerturb line 320
  24. lemma OAI.CoordinateSweeps.Grid.Holes.level_sparse_norm line 331