OAI/Analysis/Laughlin/FourBody/BesselAllowance.lean

GitHub source file

9 declarations, 0 contain sorry, 0 declared as axioms

  1. theorem OAI.Laughlin.Fock.orthonormal_occupation_sum_bound line 11
  2. theorem OAI.Laughlin.Spin.source_fourBody_local_orthonormal line 29
  3. theorem OAI.Laughlin.Fock.source_fourBody_bessel_allowance line 80
  4. theorem OAI.Laughlin.Fock.physical_fourBody_bessel_haar_allowance line 92
  5. theorem OAI.Laughlin.Fock.source_bessel_allowance_count_fin line 123
  6. theorem OAI.Laughlin.Fock.physical_fourBody_total_bessel_haar_allowance line 126
  7. theorem OAI.Laughlin.Fock.retainedFourAllowance_bessel_bound line 142
  8. theorem OAI.Laughlin.Fock.sourceA4Form_retained_bessel_bound line 148
  9. theorem OAI.Laughlin.Fock.sourceA4Form_bessel_bound line 174