OAI/Analysis/CoulombRadii/FieldAnalysis/OuterJoinConfiguration.lean

GitHub source file

38 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.Coulomb.outerJoinConfiguration line 129
  2. lemma OAI.Coulomb.outerJoinConfiguration_apply line 133
  3. lemma OAI.Coulomb.outerJoinConfiguration_measurePreserving line 135
  4. lemma OAI.Coulomb.outerJoinConfiguration_right_single line 139
  5. abbrev OAI.Coulomb.outerAppend line 155
  6. def OAI.Coulomb.outerAppendEquiv line 156
  7. def OAI.Coulomb.outerPerm line 158
  8. lemma OAI.Coulomb.outerPerm_left line 161
  9. lemma OAI.Coulomb.outerPerm_right line 163
  10. lemma OAI.Coulomb.outerPerm_sign line 165
  11. lemma OAI.Coulomb.append_outerPerm line 167
  12. lemma OAI.Coulomb.permute_outer_join line 173
  13. lemma OAI.Coulomb.H1Vector.weak_partial_outerJoin line 187
  14. lemma OAI.Coulomb.H1Vector.outer_slices_H1 line 200
  15. def OAI.Coulomb.H1Vector.OuterSliceRegular line 228
  16. lemma OAI.Coulomb.H1Vector.outerSliceRegular_ae line 240
  17. def OAI.Coulomb.H1Vector.outerSlice line 243
  18. lemma OAI.Coulomb.H1Vector.outerSlice_value line 255
  19. lemma OAI.Coulomb.H1Vector.outerSlice_gradient line 260
  20. lemma OAI.Coulomb.mass_outerSlice_ae line 267
  21. lemma OAI.Coulomb.mass_outerSlice_integrable line 273
  22. lemma OAI.Coulomb.integral_mass_outerSlice line 282
  23. lemma OAI.Coulomb.H1Vector.outerSlice_antisymmetric line 307
  24. lemma OAI.Coulomb.Antisymmetric.outerSlice line 324
  25. lemma OAI.Coulomb.kinetic_outerSlice_ae line 328
  26. lemma OAI.Coulomb.kinetic_outerSlice_integrable line 336
  27. lemma OAI.Coulomb.integral_kinetic_outerSlice line 347
  28. lemma OAI.Coulomb.potentialForm_outerSlice_ae line 377
  29. lemma OAI.Coulomb.potentialForm_outerSlice_integrable line 384
  30. lemma OAI.Coulomb.integral_potentialForm_outerSlice line 402
  31. lemma OAI.Coulomb.outerJoinConfiguration_symm_snd line 435
  32. lemma OAI.Coulomb.outer_finePower_integrable line 437
  33. theorem OAI.Coulomb.outer_block_retained_fine_kinetic_lower line 451
  34. lemma OAI.Coulomb.ae_outer_block_position_injective line 477
  35. lemma OAI.Coulomb.ae_outer_fine_pair_bound line 484
  36. lemma OAI.Coulomb.outer_fineCoulomb_integrable line 501
  37. theorem OAI.Coulomb.outer_block_retained_fine_pair_lower line 515
  38. theorem OAI.Coulomb.outer_block_retained_fine_energy_lower line 524