WikiLeanRecent changes · Proposals · Flags · Stats · About

Diff — Median

Revision #1402 → #1767 · back to history

addedMedoida2b99ffa86a0
addedCantelli's inequality (alternative proof)a2b572e8722e
addedBootstrap variance estimate consistency66b5f537b7d0
modifiedMean-unbiased minimizes squared-error riskc56408e2567f
FieldFrom #1402To #1767
noteMathlib has variance lemmas (e.g. `variance_le_expectation_sq`) but no decision-theoretic statement that mean-unbiased estimators minimize squared-error risk.Mathlib has variance lemmas (e.g. `ProbabilityTheory.variance_le_expectation_sq`) but no decision-theoretic statement that mean-unbiased estimators minimize squared-error risk.