OAI/Probability/SpanningForest/DyadicGaussianBound.lean

GitHub source file

9 declarations, 0 contain sorry, 0 declared as axioms

  1. theorem OAI.Problem336.DyadicGaussianBound.ae_time_consistent line 15
  2. theorem OAI.Problem336.DyadicGaussianBound.ae_zero_coordinates line 29
  3. def OAI.Problem336.DyadicGaussianBound.sample line 41
  4. theorem OAI.Problem336.DyadicGaussianBound.measurable_sample line 46
  5. theorem OAI.Problem336.DyadicGaussianBound.sample_time_eq line 54
  6. lemma OAI.Problem336.DyadicGaussianBound.nndist_adjacent_grid line 64
  7. theorem OAI.Problem336.DyadicGaussianBound.hasLaw_grid_increment line 74
  8. theorem OAI.Problem336.DyadicGaussianBound.ae_all_grid_increment_bound line 83
  9. theorem OAI.Problem336.DyadicGaussianBound.ae_all_sample_increment_bound line 96