OAI/Analysis/Steinitz/Chaining.lean

GitHub source file

60 declarations, 0 contain sorry, 0 declared as axioms

Gaussian chaining, finite nets, and uniform process bounds.

  1. def OAI.GaussianChaining.radius line 13
  2. def OAI.GaussianChaining.variance line 15
  3. def OAI.GaussianChaining.exponent line 18
  4. lemma OAI.GaussianChaining.nat_add_one_le_two_pow line 20
  5. lemma OAI.GaussianChaining.exponent_le line 23
  6. lemma OAI.GaussianChaining.radius_nonneg line 32
  7. lemma OAI.GaussianChaining.tail_threshold_le line 36
  8. lemma OAI.GaussianChaining.exp_exponent_le line 81
  9. lemma OAI.GaussianChaining.edge_failure line 91
  10. lemma OAI.GaussianChaining.entropy_weight line 109
  11. lemma OAI.GaussianChaining.weight_sum line 116
  12. lemma OAI.GaussianChaining.weight_sum_all line 125
  13. lemma OAI.GaussianChaining.level_failure line 133
  14. lemma OAI.GaussianChaining.all_edges_failure line 151
  15. lemma OAI.GaussianChaining.radius_sum line 167
  16. def OAI.GridNets.cell line 192
  17. def OAI.GridNets.InSquare line 194
  18. def OAI.GridNets.cellPair line 196
  19. def OAI.GridNets.grid line 198
  20. lemma OAI.GridNets.cell_le line 200
  21. lemma OAI.GridNets.cellPair_mem line 205
  22. lemma OAI.GridNets.abs_sub_lt_width line 212
  23. lemma OAI.GridNets.eventually_cell_separates line 228
  24. def OAI.GridNets.point line 240
  25. def OAI.GridNets.rep line 243
  26. lemma OAI.GridNets.rep_cell line 245
  27. lemma OAI.GridNets.rep_distance line 251
  28. lemma OAI.GridNets.eventually_rep_eq line 258
  29. lemma OAI.GridNets.grid_card line 271
  30. lemma OAI.GridNets.grid_card_square_le line 273
  31. lemma OAI.GridNets.image_pair_card_le line 284
  32. lemma OAI.GaussianTail.matrixMap_add line 308
  33. lemma OAI.GaussianTail.matrixMap_sub line 312
  34. lemma OAI.GaussianTail.matrixMap_zero line 316
  35. lemma OAI.GaussianTail.squareMass_eq_zero line 321
  36. lemma OAI.GaussianTail.difference_operator line 328
  37. lemma OAI.GaussianChaining.width_power line 344
  38. lemma OAI.GaussianChaining.coordinate_power_bound line 351
  39. lemma OAI.GaussianChaining.width_le_quarter line 360
  40. def OAI.GaussianChaining.netEnd line 367
  41. def OAI.GaussianChaining.netEdge line 370
  42. def OAI.GaussianChaining.edgeSet line 374
  43. lemma OAI.GaussianChaining.edgeSet_card line 378
  44. lemma OAI.GaussianChaining.adjacent_distance line 387
  45. lemma OAI.GaussianChaining.netEdge_variance line 404
  46. lemma OAI.GaussianChaining.netEdge_operator line 433
  47. lemma OAI.GaussianChaining.netEdge_sum line 441
  48. lemma OAI.GaussianChaining.eventually_netEnd_eq line 448
  49. lemma OAI.GaussianChaining.radius_summable line 459
  50. lemma OAI.GaussianChaining.netEnd_norm_le line 468
  51. lemma OAI.GaussianChaining.class_failure line 483
  52. lemma OAI.GaussianTail.matrixMap_mul line 539
  53. lemma OAI.GaussianTail.inner_matrixMap line 544
  54. lemma OAI.GaussianTail.coisometry_operator line 550
  55. lemma OAI.GaussianChaining.classified_failure line 580
  56. lemma OAI.GaussianChaining.classified_survival line 620
  57. def OAI.GaussianChaining.sizeClass line 646
  58. lemma OAI.GaussianChaining.sizeClass_bounds line 649
  59. lemma OAI.GaussianChaining.sizeClass_sqrt line 662
  60. lemma OAI.GaussianAR.block_survival line 684