Clean up the files in the Antichain folder (#470)

In particular, this PR:
- Adds documentation.
- Renames some lemmas for consistency with blueprint and use of snake
case.
- Deletes outdated comments.
- Realigns equation numbers in code and blueprint.
- Slightly golfs some proofs.
- Deletes lemma `mem_ball_of_mem_tsupport_correlation`, since the weaker
version `mem_ball_of_correlation_ne_zero` suffices for the current
version of `holder_van_der_corput`.
- Fixes some issues in the blueprint's proof of Lemma 6.1.5 (e.g,
conflicting notations p and p' vs p_1 and p_2 withing the proof, missing
terms in ineq. 6.2.28, 6.2.29.)
- Add some section variables.
- Deletes redundant imports.

Author: mariainesdff