OAI/Probability/LatticeSurface/Moments/EnergyDeficits.lean

GitHub source file

7 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.RetainedShell.blockDeficit line 737
2. def OAI.RetainedShell.coarseTail line 742
3. lemma OAI.RetainedShell.shared_face line 751
4. lemma OAI.RetainedShell.coarseTail_pin line 759
5. lemma OAI.RetainedShell.tail_face line 765
6. lemma OAI.RetainedShell.blockDeficit_nonneg line 770
7. theorem OAI.RetainedShell.energy_deficits line 796