OAI/Analysis/LipschitzEquivalence/WeightedGraph.lean

GitHub source file

35 declarations, 0 contain sorry, 0 declared as axioms

  1. abbrev OAI.LipschitzCounterexample.WeightedGraph.L1 line 17
  2. abbrev OAI.LipschitzCounterexample.WeightedGraph.C0 line 18
  3. def OAI.LipschitzCounterexample.WeightedGraph.weight line 20
  4. theorem OAI.LipschitzCounterexample.WeightedGraph.weight_pos line 22
  5. theorem OAI.LipschitzCounterexample.WeightedGraph.weight_ne_zero line 23
  6. theorem OAI.LipschitzCounterexample.WeightedGraph.weight_nonneg line 24
  7. theorem OAI.LipschitzCounterexample.WeightedGraph.hasSum_weight line 26
  8. theorem OAI.LipschitzCounterexample.WeightedGraph.norm_l1 line 32
  9. instance OAI.LipschitzCounterexample.WeightedGraph.(instance at line 35) line 35
  10. def OAI.LipschitzCounterexample.WeightedGraph.graphSubmodule line 52
  11. theorem OAI.LipschitzCounterexample.WeightedGraph.isClosed_graphSubmodule line 64
  12. def OAI.LipschitzCounterexample.WeightedGraph.Space line 74
  13. instance OAI.LipschitzCounterexample.WeightedGraph.(instance at line 76) line 76
  14. instance OAI.LipschitzCounterexample.WeightedGraph.(instance at line 78) line 78
  15. instance OAI.LipschitzCounterexample.WeightedGraph.(instance at line 80) line 80
  16. instance OAI.LipschitzCounterexample.WeightedGraph.(instance at line 83) line 83
  17. def OAI.LipschitzCounterexample.WeightedGraph.inclusion line 89
  18. def OAI.LipschitzCounterexample.WeightedGraph.coord line 95
  19. def OAI.LipschitzCounterexample.WeightedGraph.output line 97
  20. theorem OAI.LipschitzCounterexample.WeightedGraph.output_apply line 100
  21. theorem OAI.LipschitzCounterexample.WeightedGraph.map_coord line 102
  22. theorem OAI.LipschitzCounterexample.WeightedGraph.weight_smul_coord line 106
  23. theorem OAI.LipschitzCounterexample.WeightedGraph.norm_output_le line 109
  24. theorem OAI.LipschitzCounterexample.WeightedGraph.norm_coord_le line 112
  25. def OAI.LipschitzCounterexample.WeightedGraph.coordCLM line 117
  26. theorem OAI.LipschitzCounterexample.WeightedGraph.norm_eq line 129
  27. theorem OAI.LipschitzCounterexample.WeightedGraph.summable_weighted_norm line 138
  28. def OAI.LipschitzCounterexample.WeightedGraph.ofSequence line 143
  29. theorem OAI.LipschitzCounterexample.WeightedGraph.coord_ofSequence line 152
  30. theorem OAI.LipschitzCounterexample.WeightedGraph.ext line 156
  31. theorem OAI.LipschitzCounterexample.WeightedGraph.coord_zero line 165
  32. theorem OAI.LipschitzCounterexample.WeightedGraph.coord_sub line 168
  33. def OAI.LipschitzCounterexample.WeightedGraph.lift line 178
  34. theorem OAI.LipschitzCounterexample.WeightedGraph.coord_lift line 195
  35. theorem OAI.LipschitzCounterexample.WeightedGraph.lipschitz_lift line 199