OAI/Analysis/CoulombIonization/Variational/BlockSwap.lean
13 declarations, 0 contain sorry, 0 declared as axioms
- def
OAI.CoulombAtom.blockSwapline 17 - lemma
OAI.CoulombAtom.blockSwap_leftline 20 - lemma
OAI.CoulombAtom.blockSwap_rightline 24 - lemma
OAI.CoulombAtom.joinLists_blockSwapline 28 - def
OAI.CoulombAtom.swapBlocksline 34 - lemma
OAI.CoulombAtom.swapBlocks_valueline 37 - lemma
OAI.CoulombAtom.swapBlocks_sobolevline 43 - lemma
OAI.CoulombAtom.swapBlocks_massline 46 - lemma
OAI.CoulombAtom.swapBlocks_coreKineticline 49 - lemma
OAI.CoulombAtom.swapBlocks_coreRepulsionline 63 - lemma
OAI.CoulombAtom.weighted_coreSlice_reorderline 87 - lemma
OAI.CoulombAtom.retained_pressure_join_integrableline 120 - lemma
OAI.CoulombAtom.retained_direct_join_integrableline 134