OAI/Analysis/Laughlin/Charge/Overlap.lean

GitHub source file

11 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.Laughlin.Charge.weightedCreate line 10
  2. def OAI.Laughlin.Charge.weightedAnnihilate line 13
  3. theorem OAI.Laughlin.Charge.weighted_adjoint line 16
  4. theorem OAI.Laughlin.Charge.weighted_adjoint_rev line 23
  5. theorem OAI.Laughlin.Charge.weighted_car line 29
  6. theorem OAI.Laughlin.Charge.weighted_norm_identity line 53
  7. theorem OAI.Laughlin.Charge.occupation_cauchy_sq line 66
  8. theorem OAI.Laughlin.Charge.creation_frame_bound line 73
  9. theorem OAI.Laughlin.Charge.annihilator_frame_bound line 107
  10. theorem OAI.Laughlin.Charge.unit_generator line 115
  11. theorem OAI.Laughlin.Charge.lnwyRankOneInput line 130