OAI/MathematicalPhysics/Heisenberg/LayerEnergy.lean

GitHub source file

21 declarations, 0 contain sorry, 0 declared as axioms

  1. lemma OAI.Heisenberg.Exposure.layerExposure_equivalence line 27
  2. lemma OAI.Heisenberg.Exposure.residual_integral line 41
  3. theorem OAI.Heisenberg.Exposure.layer_exposure_full line 65
  4. theorem OAI.Heisenberg.Exposure.conditional_layer_exposure line 96
  5. abbrev OAI.Heisenberg.MeshEnergy.Op line 133
  6. lemma OAI.Heisenberg.MeshEnergy.square_derivative line 137
  7. theorem OAI.Heisenberg.MeshEnergy.uniform_energy_error line 148
  8. theorem OAI.Heisenberg.MeshEnergy.finite_uniform_energy_error line 174
  9. def OAI.Heisenberg.MeshEnergy.sweep line 182
  10. lemma OAI.Heisenberg.MeshEnergy.sweep_zero line 187
  11. lemma OAI.Heisenberg.MeshEnergy.sweep_derivative line 193
  12. def OAI.Heisenberg.MeshPair.generator line 211
  13. lemma OAI.Heisenberg.MeshPair.generator_apply line 213
  14. lemma OAI.Heisenberg.MeshPair.generator_energy line 218
  15. lemma OAI.Heisenberg.MeshPair.step_norm_square line 222
  16. lemma OAI.Heisenberg.MeshPair.step_contraction line 229
  17. def OAI.Heisenberg.MeshPair.edgeVector line 245
  18. lemma OAI.Heisenberg.MeshPair.edge_inner line 249
  19. lemma OAI.Heisenberg.MeshPair.edge_norm line 255
  20. theorem OAI.Heisenberg.MeshPair.sweep_dirichlet line 261
  21. theorem OAI.Heisenberg.MeshPair.sweep_energy line 270