OAI/Analysis/HardSphere/FormDomain/HilbertJet.lean

GitHub source file

32 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.HardSphere.optionJetEquiv line 17
  2. def OAI.HardSphere.hilbertJetEquiv line 27
  3. lemma OAI.HardSphere.hilbertJetEquiv_fst line 30
  4. lemma OAI.HardSphere.hilbertJetEquiv_snd line 32
  5. lemma OAI.HardSphere.hilbertJet_inner line 35
  6. lemma OAI.HardSphere.hilbertJet_norm_sq line 41
  7. def OAI.HardSphere.hilbertDomain line 46
  8. instance OAI.HardSphere.hilbertDomain_closed line 49
  9. instance OAI.HardSphere.hilbertDomain_complete line 52
  10. def OAI.HardSphere.scalarEmbedding line 55
  11. lemma OAI.HardSphere.scalarEmbedding_norm_le line 59
  12. def OAI.HardSphere.formResolvent line 64
  13. lemma OAI.HardSphere.formResolvent_isPositive line 67
  14. lemma OAI.HardSphere.formResolvent_norm_le_one line 72
  15. lemma OAI.HardSphere.resolvent_weak_equation line 86
  16. lemma OAI.HardSphere.IsGroundVector.resolvent_eigenvector line 95
  17. lemma OAI.HardSphere.strong_projection_limit line 125
  18. lemma OAI.HardSphere.scalarAdjoint_eq_projection line 152
  19. lemma OAI.HardSphere.formResolvent_eq_projection line 170
  20. lemma OAI.HardSphere.continuous_torusDistance line 176
  21. lemma OAI.HardSphere.isOpen_allowed line 180
  22. lemma OAI.HardSphere.allowed_antitone line 194
  23. def OAI.HardSphere.innerRadius line 198
  24. lemma OAI.HardSphere.innerRadius_gt line 200
  25. lemma OAI.HardSphere.innerRadius_antitone line 205
  26. lemma OAI.HardSphere.innerRadius_tendsto line 212
  27. lemma OAI.HardSphere.iUnion_allowed_innerRadius line 216
  28. lemma OAI.HardSphere.SmoothTest.exists_innerRadius line 231
  29. lemma OAI.HardSphere.dirichletDomain_antitone line 241
  30. lemma OAI.HardSphere.hilbertDomain_antitone line 248
  31. lemma OAI.HardSphere.hilbertDomain_exhaustion line 252
  32. lemma OAI.HardSphere.formResolvent_innerRadius_tendsto line 277