OAI/Probability/LatticeSurface/Moments/ControlledGradients.lean

GitHub source file

6 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.ExtremalEdges.height line 60
2. def OAI.ExtremalEdges.body line 63
3. def OAI.ExtremalEdges.cap line 66
4. lemma OAI.ExtremalEdges.height_restore line 70
5. lemma OAI.ExtremalEdges.body_conditional line 73
6. theorem OAI.ExtremalEdges.controlled_gradients line 76