OAI/Geometry/TamingCompatibility/Elliptic/LocalGarding.lean

GitHub source file

27 declarations, 0 contain sorry, 0 declared as axioms

  1. abbrev OAI.TamingCompatibility.EuclideanEnergy.V line 16
  2. abbrev OAI.TamingCompatibility.EuclideanEnergy.S line 17
  3. def OAI.TamingCompatibility.EuclideanEnergy.e line 18
  4. def OAI.TamingCompatibility.EuclideanEnergy.coordinateDeriv line 20
  5. lemma OAI.TamingCompatibility.EuclideanEnergy.second_partial_comm line 22
  6. lemma OAI.TamingCompatibility.EuclideanEnergy.partial_mul_integral_swap line 36
  7. def OAI.TamingCompatibility.EuclideanEnergy.codifferential line 45
  8. def OAI.TamingCompatibility.EuclideanEnergy.gradientEnergy line 49
  9. lemma OAI.TamingCompatibility.EuclideanEnergy.schwartz_mul_integrable line 52
  10. lemma OAI.TamingCompatibility.EuclideanEnergy.schwartz_sq_integrable line 55
  11. lemma OAI.TamingCompatibility.EuclideanEnergy.gradientEnergy_integrable line 58
  12. lemma OAI.TamingCompatibility.EuclideanEnergy.codifferential_energy_pointwise line 62
  13. theorem OAI.TamingCompatibility.EuclideanEnergy.codifferential_energy line 69
  14. abbrev OAI.TamingCompatibility.EuclideanEnergy.Pair line 93
  15. def OAI.TamingCompatibility.EuclideanEnergy.pair line 94
  16. lemma OAI.TamingCompatibility.EuclideanEnergy.pair_norm_sq line 95
  17. def OAI.TamingCompatibility.EuclideanEnergy.variableCodifferential line 98
  18. lemma OAI.TamingCompatibility.EuclideanEnergy.norm_add_sq_le line 104
  19. lemma OAI.TamingCompatibility.EuclideanEnergy.norm_sum_four_sq_le line 110
  20. lemma OAI.TamingCompatibility.EuclideanEnergy.principalError_bound line 120
  21. lemma OAI.TamingCompatibility.EuclideanEnergy.lowerError_bound line 137
  22. lemma OAI.TamingCompatibility.EuclideanEnergy.variableCodifferential_pointwise line 145
  23. lemma OAI.TamingCompatibility.EuclideanEnergy.codifferential_continuous line 164
  24. lemma OAI.TamingCompatibility.EuclideanEnergy.pair_continuous line 169
  25. lemma OAI.TamingCompatibility.EuclideanEnergy.codifferential_integrable_sq line 175
  26. lemma OAI.TamingCompatibility.EuclideanEnergy.variableCodifferential_integrable line 182
  27. theorem OAI.TamingCompatibility.EuclideanEnergy.local_garding line 212