OAI/Geometry/Cannon/Flows/Oscillation.lean

GitHub source file

18 declarations, 0 contain sorry, 0 declared as axioms

  1. theorem OAI.CannonNode.good_candidate_pattern line 19
  2. lemma OAI.CannonNode.clip_difference_le line 111
  3. theorem OAI.CannonNode.SourceConstruction.node_pattern line 126
  4. theorem OAI.CannonNode.exists_flow_constants line 218
  5. theorem OAI.CannonCrossEnergy.weighted_interval_cover line 276
  6. def OAI.CannonCrossEnergy.oscillation line 305
  7. def OAI.CannonCrossEnergy.rangeInterval line 308
  8. lemma OAI.CannonCrossEnergy.mem_rangeInterval line 311
  9. lemma OAI.CannonCrossEnergy.oscillation_nonneg line 317
  10. lemma OAI.CannonCrossEnergy.rangeInterval_eq_image line 322
  11. theorem OAI.CannonCrossEnergy.level_continuum_cover line 331
  12. theorem OAI.CannonCrossEnergy.finite_cell_level_comparison line 377
  13. theorem OAI.CannonCrossEnergy.no_vanishing_cross_energy line 407
  14. lemma OAI.CannonCrossEnergyLocal.mem_rangeInterval line 441
  15. lemma OAI.CannonCrossEnergyLocal.oscillation_nonneg line 447
  16. lemma OAI.CannonCrossEnergyLocal.rangeInterval_eq_image line 452
  17. theorem OAI.CannonCrossEnergyLocal.level_continuum_cover line 461
  18. theorem OAI.CannonCrossEnergyLocal.finite_cell_level_comparison line 508