OAI/Geometry/CAT0Fillings/Sobolev/Completion.lean

GitHub source file

23 declarations, 0 contain sorry, 0 declared as axioms

  1. abbrev OAI.CAT0Fillings.ChartGeometry.GraphAmbient line 16
  2. def OAI.CAT0Fillings.ChartGeometry.graphPoint line 19
  3. lemma OAI.CAT0Fillings.ChartGeometry.graphPoint_add line 22
  4. lemma OAI.CAT0Fillings.ChartGeometry.graphPoint_smul line 29
  5. def OAI.CAT0Fillings.ChartGeometry.lipschitzGraph line 35
  6. def OAI.CAT0Fillings.ChartGeometry.closedGraph line 47
  7. abbrev OAI.CAT0Fillings.ChartGeometry.Sobolev line 49
  8. lemma OAI.CAT0Fillings.ChartGeometry.closedGraph_isClosed line 51
  9. instance OAI.CAT0Fillings.ChartGeometry.(instance at line 54) line 54
  10. def OAI.CAT0Fillings.ChartGeometry.valueProjection line 56
  11. def OAI.CAT0Fillings.ChartGeometry.gradientProjection line 59
  12. lemma OAI.CAT0Fillings.ChartGeometry.valueProjection_graphPoint line 62
  13. lemma OAI.CAT0Fillings.ChartGeometry.gradientProjection_graphPoint line 64
  14. lemma OAI.CAT0Fillings.ChartGeometry.graph_norm_sq line 67
  15. lemma OAI.CAT0Fillings.ChartGeometry.graphPoint_mem line 71
  16. lemma OAI.CAT0Fillings.ChartGeometry.exists_lipschitz_approximants line 75
  17. lemma OAI.CAT0Fillings.ChartGeometry.closedGraph_zero_value line 99
  18. lemma OAI.CAT0Fillings.ChartGeometry.closedGraph_value_injective line 110
  19. def OAI.CAT0Fillings.ChartGeometry.inclusion line 125
  20. def OAI.CAT0Fillings.ChartGeometry.closedGradient line 128
  21. lemma OAI.CAT0Fillings.ChartGeometry.inclusion_injective line 131
  22. lemma OAI.CAT0Fillings.ChartGeometry.sobolev_norm_sq line 134
  23. lemma OAI.CAT0Fillings.ChartGeometry.closedGradient_closed line 137