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

'PaperToLean.Welford.mean_accumulator' depends on axioms: [propext, Classical.choice, Quot.sound]
'PaperToLean.Welford.square_accumulator' depends on axioms: [propext, Classical.choice, Quot.sound]
'PaperToLean.Welford.scatter_increment' depends on axioms: [propext, Classical.choice, Quot.sound]
'PaperToLean.Welford.update_nonneg' depends on axioms: [propext, Classical.choice, Quot.sound]
'PaperToLean.Welford.moments' depends on axioms: [propext, Classical.choice, Quot.sound]
'PaperToLean.Welford.mean_correct' depends on axioms: [propext, Classical.choice, Quot.sound]
'PaperToLean.Welford.centered_sum' depends on axioms: [propext, Classical.choice, Quot.sound]
'PaperToLean.Welford.scatter_correct' depends on axioms: [propext, Classical.choice, Quot.sound]
