OAI/Geometry/Cannon/Flows/State.lean

GitHub source file

38 declarations, 0 contain sorry, 0 declared as axioms

  1. lemma OAI.CannonPairCost.sum_measure_le_multiplicity line 22
  2. theorem OAI.CannonPairCost.finite_pair_bound line 45
  3. lemma OAI.CannonPairCost.cost_comparison line 70
  4. theorem OAI.CannonPairCost.not_frequently_exp_le_quadratic line 88
  5. theorem OAI.CannonPairCost.separated_level_energy line 121
  6. abbrev OAI.CannonNode.SourceConstruction.state line 164
  7. abbrev OAI.CannonNode.SourceConstruction.good line 166
  8. def OAI.CannonNode.SourceConstruction.flow line 169
  9. abbrev OAI.CannonNode.SourceConstruction.center line 171
  10. abbrev OAI.CannonNode.SourceConstruction.len line 173
  11. abbrev OAI.CannonNode.SourceConstruction.scale line 175
  12. abbrev OAI.CannonNode.SourceConstruction.step line 177
  13. lemma OAI.CannonNode.SourceConstruction.state_depth line 179
  14. lemma OAI.CannonNode.SourceConstruction.scale_succ line 184
  15. lemma OAI.CannonNode.SourceConstruction.len_pos line 187
  16. lemma OAI.CannonNode.SourceConstruction.root_length line 189
  17. lemma OAI.CannonNode.SourceConstruction.step_pos line 191
  18. lemma OAI.CannonNode.SourceConstruction.weight_step line 193
  19. lemma OAI.CannonNode.SourceConstruction.step_linear line 196
  20. lemma OAI.CannonNode.SourceConstruction.step_nested line 200
  21. lemma OAI.CannonNode.SourceConstruction.weight_linear line 203
  22. lemma OAI.CannonNode.SourceConstruction.weight_conditional line 208
  23. lemma OAI.CannonNode.SourceConstruction.center_step line 220
  24. lemma OAI.CannonNode.SourceConstruction.centers_separated line 228
  25. lemma OAI.CannonNode.SourceConstruction.descendant_displacement line 248
  26. lemma OAI.CannonNode.SourceConstruction.step_quadratic line 257
  27. lemma OAI.CannonNode.SourceConstruction.weight_bound line 303
  28. lemma OAI.CannonNode.SourceConstruction.len_lt_one line 313
  29. lemma OAI.CannonNode.SourceConstruction.center_mem line 318
  30. lemma OAI.CannonNode.SourceConstruction.level_energy line 321
  31. theorem OAI.CannonNode.SourceConstruction.arbitrarily_late_good line 355
  32. theorem OAI.CannonMagnification.preimage_distance_bound line 378
  33. theorem OAI.CannonMagnification.inverse_lipschitz_on_preimages line 404
  34. theorem OAI.CannonMagnification.image_ball_avoids_puncture line 427
  35. def OAI.CannonMagnification.denominator line 459
  36. lemma OAI.CannonMagnification.denominator_triangle line 462
  37. theorem OAI.CannonMagnification.puncture_bounds line 468
  38. theorem OAI.CannonMagnification.cost_ball_geometry line 502