feat: Port Criterion to Lean

[samuelburnham]

Ports the core benchmarking and statistical analysis logic from https://github.com/bheisler/criterion.rs to Lean. This includes:

• Warmup time to estimate total runtime
• Flat and linear sampling modes
• Sample analysis: Bootstrap sampling, point estimates and distributions for mean, stdDev, median, etc., and linear regression if in linear sampling mode
• Outlier detection via Tukey's method
• Disk caching as Ixon data in .lake/benches for comparison between runs
• Change analysis: Bootstrapped T-test and p value, noise threshold
• Configurable parameters
• Formatted output similar to Criterion.rs

Usage: lake exe bench will run all of the benchmarks specified in the Benchmarks.Main file's main function.

Some TODOs for another PR:

• Throughput measurement
• General performance enhancements
• Testing
• Documentation
• Logging/verbosity
• Disk cache for Tukey outliers
• Plots

[arthurpaulino]

This is great work already!
Can you break this patch so that you don't need to complete the whole TODO list before we can use it, please?

[arthurpaulino]

Left some comments.

Module docstrings are written as

/-!
# A header if necessary
Some markdown text
-/

[arthurpaulino]

🎉 🥳 🎊