OAI/Geometry/TamingCompatibility/Hodge/HodgeMatrixEnergy.lean

GitHub source file

28 declarations, 0 contain sorry, 0 declared as axioms

  1. abbrev OAI.TamingCompatibility.HodgeMatrixEnergy.W line 16
  2. abbrev OAI.TamingCompatibility.HodgeMatrixEnergy.Field line 17
  3. def OAI.TamingCompatibility.HodgeMatrixEnergy.value line 19
  4. def OAI.TamingCompatibility.HodgeMatrixEnergy.derivative line 20
  5. def OAI.TamingCompatibility.HodgeMatrixEnergy.gradient line 22
  6. lemma OAI.TamingCompatibility.HodgeMatrixEnergy.value_norm line 24
  7. lemma OAI.TamingCompatibility.HodgeMatrixEnergy.value_continuous line 26
  8. lemma OAI.TamingCompatibility.HodgeMatrixEnergy.value_integrable line 28
  9. lemma OAI.TamingCompatibility.HodgeMatrixEnergy.gradient_integrable line 31
  10. lemma OAI.TamingCompatibility.HodgeMatrixEnergy.gradient_nonneg line 33
  11. def OAI.TamingCompatibility.HodgeMatrixEnergy.system line 37
  12. def OAI.TamingCompatibility.HodgeMatrixEnergy.constantSystem line 39
  13. lemma OAI.TamingCompatibility.HodgeMatrixEnergy.principalError_bound line 42
  14. lemma OAI.TamingCompatibility.HodgeMatrixEnergy.lowerError_bound line 54
  15. lemma OAI.TamingCompatibility.HodgeMatrixEnergy.system_integrable line 60
  16. lemma OAI.TamingCompatibility.HodgeMatrixEnergy.constantSystem_integrable line 79
  17. lemma OAI.TamingCompatibility.HodgeMatrixEnergy.comparison_pointwise line 87
  18. theorem OAI.TamingCompatibility.HodgeMatrixEnergy.garding line 106
  19. abbrev OAI.TamingCompatibility.HodgeNormalSymbol.W line 144
  20. abbrev OAI.TamingCompatibility.HodgeNormalSymbol.Q line 145
  21. def OAI.TamingCompatibility.HodgeNormalSymbol.symbol line 147
  22. lemma OAI.TamingCompatibility.HodgeNormalSymbol.symbol_add line 155
  23. lemma OAI.TamingCompatibility.HodgeNormalSymbol.symbol_smul line 158
  24. def OAI.TamingCompatibility.HodgeNormalSymbol.normalSymbol line 162
  25. lemma OAI.TamingCompatibility.HodgeNormalSymbol.normalSymbol_apply line 168
  26. lemma OAI.TamingCompatibility.HodgeNormalSymbol.normalSymbol_inner line 169
  27. lemma OAI.TamingCompatibility.HodgeNormalSymbol.normalSymbol_polarized line 175
  28. theorem OAI.TamingCompatibility.HodgeNormalSymbol.normalSymbol_adjoint_polarized line 182