OAI/Probability/SKFluctuations/ComparisonCapTravel.lean

GitHub source file

27 declarations, 0 contain sorry, 0 declared as axioms

Comparison Cap Travel.

  1. theorem OAI.SKFluctuations.Hierarchy.cap_travel_identity line 15
  2. theorem OAI.SKFluctuations.Hierarchy.comparisonCap_first_term line 32
  3. theorem OAI.SKFluctuations.Hierarchy.comparisonCap_log_travel line 49
  4. theorem OAI.SKFluctuations.Hierarchy.comparisonCap_band_travel line 68
  5. def OAI.SKFluctuations.comparisonBracket line 103
  6. theorem OAI.SKFluctuations.comparisonBracket_antitone line 105
  7. theorem OAI.SKFluctuations.comparisonBracket_nonneg_geometry line 116
  8. theorem OAI.SKFluctuations.comparisonBracket_increment line 134
  9. theorem OAI.SKFluctuations.comparisonBracket_endpoint_increment line 163
  10. theorem OAI.SKFluctuations.Hierarchy.potential_integral_eq_sub line 183
  11. theorem OAI.SKFluctuations.Hierarchy.potential_negative_left_witness line 193
  12. theorem OAI.SKFluctuations.Hierarchy.potential_positive_right_witness line 209
  13. theorem OAI.SKFluctuations.Hierarchy.potential_cap_witnesses line 226
  14. theorem OAI.SKFluctuations.comparisonBracket_mono_moments line 255
  15. theorem OAI.SKFluctuations.comparisonBracket_left_mismatch line 263
  16. theorem OAI.SKFluctuations.comparisonBracket_endpoint_increment_uniform line 295
  17. theorem OAI.SKFluctuations.cap_S_le_right line 315
  18. theorem OAI.SKFluctuations.cap_interior_increment line 335
  19. theorem OAI.SKFluctuations.cap_interior_mismatch line 357
  20. theorem OAI.SKFluctuations.comparisonBracket_nonpos_of_radius_le line 393
  21. theorem OAI.SKFluctuations.cap_travel_le_total line 404
  22. theorem OAI.SKFluctuations.potential_negative_center_bound line 422
  23. theorem OAI.SKFluctuations.potential_future_center_bound line 474
  24. theorem OAI.SKFluctuations.Hierarchy.comparisonFloor_antiderivative line 539
  25. theorem OAI.SKFluctuations.Hierarchy.comparisonFloor_integral line 547
  26. theorem OAI.SKFluctuations.Hierarchy.comparisonFloor_total_mass line 559
  27. theorem OAI.SKFluctuations.Hierarchy.comparisonFloor_region_mass line 568