mathlib
09fb38cc - chore(analysis/box_integral): use GP instead of bot (#15939)

Commit

3 years ago

chore(analysis/box_integral): use GP instead of bot (#15939) This is how this integral is called in the original paper.

Author

urkud

Parents