OAI/Analysis/CoulombRadii/Packets/PacketSynthesisIndicator.lean

GitHub source file

8 declarations, 0 contain sorry, 0 declared as axioms

1. lemma OAI.Coulomb.packetSynthesis_indicator_eq line 89
2. lemma OAI.Coulomb.packetState_joint_continuous line 98
3. lemma OAI.Coulomb.compactPhase_finite line 103
4. lemma OAI.Coulomb.packetFrame_smooth_range line 113
5. lemma OAI.Coulomb.packetFrame_eigen_smooth line 165
6. lemma OAI.Coulomb.packetSynthesis_zero_of_notMem_region line 182
7. lemma OAI.Coulomb.packetFrame_smooth_range_supported line 194
8. lemma OAI.Coulomb.packetFrame_eigen_smooth_supported line 247