Lean 4.33.1
Dependencies: Mathlib 4.33.1 (see bundled lake-manifest.json)
File: Gruss.lean
SHA-256: 36adf642bd5ae96a43a2f77bf1dc7309ece7291fa3b67b05c337b5334cf6dbc3
Result: passed

'PaperToLean.Gruss.centered_covariance' depends on axioms: [propext, Classical.choice, Quot.sound]
'PaperToLean.Gruss.centered_variance' depends on axioms: [propext, Classical.choice, Quot.sound]
'PaperToLean.Gruss.variance_nonneg' depends on axioms: [propext, Classical.choice, Quot.sound]
'PaperToLean.Gruss.range_variance_bound' depends on axioms: [propext, Classical.choice, Quot.sound]
'PaperToLean.Gruss.covariance_cauchy' depends on axioms: [propext, Classical.choice, Quot.sound]
'PaperToLean.Gruss.inequality' depends on axioms: [propext, Classical.choice, Quot.sound]