OAI/Analysis/TreePotential/EndpointTransfer.lean

GitHub source file

23 declarations, 0 contain sorry, 0 declared as axioms

  1. lemma OAI.BoundedTreePotentials.averagedModulusReal_lower line 15
  2. lemma OAI.BoundedTreePotentials.maximumModulusReal_lower line 20
  3. lemma OAI.BoundedTreePotentials.oneSidedModulusReal_zero line 25
  4. theorem OAI.BoundedTreePotentials.TreeCalculus.four_averaged_modulus_real line 34
  5. theorem OAI.BoundedTreePotentials.TreeCalculus.four_renorming_obstruction_real line 39
  6. theorem OAI.BoundedTreePotentials.TreeCalculus.four_no_equivalent_AUC_real line 47
  7. theorem OAI.BoundedTreePotentials.FreeRoot.freeRoot_averaged_modulus_real line 55
  8. theorem OAI.BoundedTreePotentials.FreeRoot.freeRoot_renorming_obstruction_real line 59
  9. theorem OAI.BoundedTreePotentials.FreeRoot.freeRoot_no_equivalent_AUC_real line 65
  10. theorem OAI.BoundedTreePotentials.linearOuter_renorming_obstruction_real line 73
  11. theorem OAI.BoundedTreePotentials.quadraticOuter_renorming_obstruction_real line 79
  12. theorem OAI.BoundedTreePotentials.linearOuter_no_equivalent_AUC_real line 85
  13. theorem OAI.BoundedTreePotentials.quadraticOuter_no_equivalent_AUC_real line 88
  14. theorem OAI.BoundedTreePotentials.CostHeads.linear_averaged_modulus_real line 94
  15. theorem OAI.BoundedTreePotentials.CostHeads.quadratic_averaged_modulus_real line 98
  16. theorem OAI.BoundedTreePotentials.CostHeads.quadratic_maximum_modulus_real line 102
  17. theorem OAI.BoundedTreePotentials.CostHeads.quadratic_maximum_modulus_real_positive line 106
  18. theorem OAI.BoundedTreePotentials.Segments.start_maximum_modulus_real line 116
  19. theorem OAI.BoundedTreePotentials.Segments.start_unit_sphere_bound_real line 120
  20. theorem OAI.BoundedTreePotentials.Segments.start_renorming_obstruction_real line 136
  21. theorem OAI.BoundedTreePotentials.Segments.start_no_equivalent_AUC_real line 141
  22. theorem OAI.BoundedTreePotentials.Segments.incomparable_renorming_obstruction_real line 144
  23. theorem OAI.BoundedTreePotentials.Segments.incomparable_no_equivalent_AUC_real line 150