OAI/Analysis/LipschitzFree/Parameters.lean

GitHub source file

25 declarations, 0 contain sorry, 0 declared as axioms

Quantitative block parameters and strict variation bounds

  1. def OAI.DiscreteFree.BlockParameters.L line 15
  2. def OAI.DiscreteFree.BlockParameters.R line 16
  3. def OAI.DiscreteFree.BlockParameters.K line 17
  4. def OAI.DiscreteFree.BlockParameters.D line 18
  5. def OAI.DiscreteFree.BlockParameters.B line 19
  6. def OAI.DiscreteFree.BlockParameters.V line 20
  7. def OAI.DiscreteFree.BlockParameters.generators line 22
  8. def OAI.DiscreteFree.BlockParameters.degree line 23
  9. def OAI.DiscreteFree.BlockParameters.Q line 24
  10. def OAI.DiscreteFree.BlockParameters.H line 25
  11. def OAI.DiscreteFree.BlockParameters.colors line 26
  12. theorem OAI.DiscreteFree.BlockParameters.L_pos line 28
  13. theorem OAI.DiscreteFree.BlockParameters.R_pos line 30
  14. theorem OAI.DiscreteFree.BlockParameters.K_pos line 32
  15. theorem OAI.DiscreteFree.BlockParameters.small_radius line 34
  16. theorem OAI.DiscreteFree.BlockParameters.L_le_K line 36
  17. theorem OAI.DiscreteFree.BlockParameters.compatibility_cap line 41
  18. theorem OAI.DiscreteFree.BlockParameters.B_formula line 43
  19. theorem OAI.DiscreteFree.BlockParameters.degree_ge line 47
  20. theorem OAI.DiscreteFree.BlockParameters.degree_variation line 49
  21. theorem OAI.DiscreteFree.BlockParameters.Q_pos line 51
  22. theorem OAI.DiscreteFree.BlockParameters.H_pos line 53
  23. theorem OAI.DiscreteFree.BlockParameters.colors_pos line 55
  24. theorem OAI.DiscreteFree.BlockParameters.colors_large line 57
  25. theorem OAI.DiscreteFree.BlockParameters.bump_loss line 59