OAI/Geometry/TamingCompatibility/Hodge/HodgeCompactExtension.lean

GitHub source file

24 declarations, 0 contain sorry, 0 declared as axioms

  1. lemma OAI.TamingCompatibility.GeometricHilbert.OperatorCalculus.exists_compact_smooth_extension line 18
  2. lemma OAI.TamingCompatibility.GeometricHilbert.OperatorCalculus.differential_congr_nhds line 65
  3. lemma OAI.TamingCompatibility.GeometricHilbert.OperatorCalculus.differential_zero_off line 72
  4. lemma OAI.TamingCompatibility.GeometricHilbert.OperatorCalculus.integral_square_residual_local line 82
  5. def OAI.TamingCompatibility.GeometricHilbert.GeometricNormalCharts.normalDomain line 140
  6. def OAI.TamingCompatibility.GeometricHilbert.GeometricNormalCharts.normalDensity line 143
  7. def OAI.TamingCompatibility.GeometricHilbert.GeometricNormalCharts.normalPrincipal line 144
  8. def OAI.TamingCompatibility.GeometricHilbert.GeometricNormalCharts.normalFirst line 146
  9. def OAI.TamingCompatibility.GeometricHilbert.GeometricNormalCharts.normalZero line 150
  10. def OAI.TamingCompatibility.GeometricHilbert.GeometricNormalCharts.normalGauge line 154
  11. def OAI.TamingCompatibility.GeometricHilbert.GeometricNormalCharts.gaugedDomain line 158
  12. def OAI.TamingCompatibility.GeometricHilbert.GeometricNormalCharts.gaugedFirst line 161
  13. def OAI.TamingCompatibility.GeometricHilbert.GeometricNormalCharts.gaugedZero line 166
  14. lemma OAI.TamingCompatibility.GeometricHilbert.GeometricNormalCharts.normalDomain_open line 172
  15. lemma OAI.TamingCompatibility.GeometricHilbert.GeometricNormalCharts.gaugedDomain_open line 177
  16. lemma OAI.TamingCompatibility.GeometricHilbert.GeometricNormalCharts.ActualData.metric_zero line 182
  17. lemma OAI.TamingCompatibility.GeometricHilbert.GeometricNormalCharts.ActualData.center line 192
  18. lemma OAI.TamingCompatibility.GeometricHilbert.GeometricNormalCharts.normalDensity_smooth line 204
  19. lemma OAI.TamingCompatibility.GeometricHilbert.GeometricNormalCharts.normalPrincipal_smooth line 209
  20. lemma OAI.TamingCompatibility.GeometricHilbert.GeometricNormalCharts.normalFirst_smooth line 214
  21. lemma OAI.TamingCompatibility.GeometricHilbert.GeometricNormalCharts.normalZero_smooth line 223
  22. lemma OAI.TamingCompatibility.GeometricHilbert.GeometricNormalCharts.normalGauge_smooth line 234
  23. lemma OAI.TamingCompatibility.GeometricHilbert.GeometricNormalCharts.gaugedFirst_smooth line 247
  24. lemma OAI.TamingCompatibility.GeometricHilbert.GeometricNormalCharts.gaugedZero_smooth line 255