OAI/Probability/LatticeSurface/Dynamics/ClusterShift.lean

GitHub source file

75 declarations, 0 contain sorry, 0 declared as axioms

  1. theorem OAI.FeasibleShift.mem_component line 12
  2. theorem OAI.FeasibleShift.self_mem_component line 15
  3. theorem OAI.FeasibleShift.component_nonempty line 18
  4. theorem OAI.FeasibleShift.component_eq_of_reachable line 21
  5. theorem OAI.FeasibleShift.component_mono line 27
  6. theorem OAI.FeasibleShift.contactGraph_le line 34
  7. theorem OAI.FeasibleShift.contactGraph_mono line 38
  8. theorem OAI.FeasibleShift.walk_oscillation line 43
  9. theorem OAI.FeasibleShift.walk_support_subset_component line 55
  10. theorem OAI.FeasibleShift.component_oscillation line 66
  11. theorem OAI.FeasibleShift.prescription_ground line 82
  12. theorem OAI.FeasibleShift.prescription_eq_of_reachable line 90
  13. theorem OAI.FeasibleShift.prescription_bound line 95
  14. theorem OAI.FeasibleShift.prescription_approximation line 111
  15. theorem OAI.FeasibleShift.measurableSet_contactGraph_fiber line 139
  16. theorem OAI.FeasibleShift.measurable_prescription line 160
  17. theorem OAI.FeasibleShift.intervalIntegrable_prescription line 174
  18. theorem OAI.FeasibleShift.averagedShift_sub line 187
  19. theorem OAI.FeasibleShift.averagedShift_approximation line 197
  20. theorem OAI.FeasibleShift.averagedShift_bound line 222
  21. theorem OAI.FeasibleShift.averagedShift_ground line 237
  22. theorem OAI.FeasibleShift.averagedShift_tangent line 241
  23. theorem OAI.FeasibleShift.averaged_shift_approximation line 253
  24. def OAI.FeasibleShift.betweenIndicator line 271
  25. theorem OAI.FeasibleShift.betweenIndicator_nonneg line 274
  26. theorem OAI.FeasibleShift.integrable_betweenIndicator line 278
  27. theorem OAI.FeasibleShift.integral_betweenIndicator_le line 282
  28. theorem OAI.FeasibleShift.integral_edge_change_bound line 293
  29. theorem OAI.FeasibleShift.le_iff_of_not_mem_uIcc line 324
  30. def OAI.FeasibleShift.edgeThreshold line 333
  31. theorem OAI.FeasibleShift.edgeThreshold_difference line 337
  32. theorem OAI.FeasibleShift.averagedShift_difference line 350
  33. theorem OAI.FeasibleShift.averagedShift_global_difference line 360
  34. theorem OAI.FeasibleShift.averagedShift_lipschitz line 393
  35. theorem OAI.FeasibleShift.reachable_of_agree_on_component line 408
  36. theorem OAI.FeasibleShift.component_eq_of_agree line 419
  37. def OAI.FeasibleShift.componentEdges line 429
  38. theorem OAI.FeasibleShift.mem_componentEdges line 433
  39. theorem OAI.FeasibleShift.averagedShift_component_difference line 438
  40. theorem OAI.FeasibleShift.mem_neighbors line 476
  41. theorem OAI.FeasibleShift.componentEdges_card_le line 480
  42. theorem OAI.FeasibleShift.averagedShift_component_lipschitz_bound line 493
  43. theorem OAI.FeasibleShift.contactGraph_le_of_distance line 522
  44. theorem OAI.FeasibleShift.averagedShift_feasible line 530
  45. theorem OAI.FeasibleShift.averagedShift_injective_good line 563
  46. def OAI.FeasibleShift.incidentEdges line 612
  47. theorem OAI.FeasibleShift.mem_incidentEdges line 615
  48. theorem OAI.FeasibleShift.incidentEdges_card_le line 628
  49. theorem OAI.FeasibleShift.edgeThreshold_same_off_coordinate line 639
  50. theorem OAI.FeasibleShift.edgeThreshold_coordinate_bound line 645
  51. theorem OAI.FeasibleShift.component_threshold_sum_coordinate line 661
  52. theorem OAI.FeasibleShift.averagedShift_coordinate_bound line 689
  53. theorem OAI.FeasibleShift.averagedShift_coordinate_zero line 708
  54. theorem OAI.FeasibleShift.hasDerivAt_coordinate line 725
  55. theorem OAI.FeasibleShift.coordinate_small_contact line 735
  56. theorem OAI.FeasibleShift.averagedShift_derivative_entry line 745
  57. theorem OAI.FeasibleShift.averagedShift_derivative_entry_zero line 769
  58. def OAI.FeasibleShift.derivativeMatrix line 789
  59. theorem OAI.FeasibleShift.averagedShift_derivative_HS line 792
  60. theorem OAI.FeasibleShift.identity_add_bijective line 825
  61. theorem OAI.FeasibleShift.averagedShift_small_preserves_edge_iff line 862
  62. theorem OAI.FeasibleShift.abs_trace_square_le_HS line 890
  63. theorem OAI.FeasibleShift.extendHeight_pin line 908
  64. theorem OAI.FeasibleShift.extendHeight_free line 913
  65. theorem OAI.FeasibleShift.extendHeight_lipschitz line 917
  66. theorem OAI.FeasibleShift.freeShift_lipschitz line 929
  67. theorem OAI.FeasibleShift.extendHeight_shift line 952
  68. theorem OAI.FeasibleShift.freeShift_small_polytope_preimage line 963
  69. theorem OAI.FeasibleShift.freeShift_small_polytope_onto line 994
  70. theorem OAI.FeasibleShift.extendHeight_coordinate line 1009
  71. theorem OAI.FeasibleShift.freeShift_derivative_entry line 1022
  72. theorem OAI.FeasibleShift.freeShift_derivative_entry_zero line 1048
  73. theorem OAI.FeasibleShift.freeShift_derivative_ground line 1071
  74. theorem OAI.FeasibleShift.freeShift_derivative_HS line 1084
  75. theorem OAI.FeasibleShift.freeShift_ae_differentiable line 1134