mathlib
85453a2a - feat(probability/variance): introduce `ℝ≥0∞`-valued variance (#16730)

Commit

3 years ago

feat(probability/variance): introduce `ℝ≥0∞`-valued variance (#16730) This PR introduces `ℝ≥0∞`-valued variance and define the real-valued variance in terms of it.

Author

kex-y

Parents

ffd1e5cb

mathlib 85453a2a - feat(probability/variance): introduce `ℝ≥0∞`-valued variance (#16730)

mathlib
85453a2a - feat(probability/variance): introduce `ℝ≥0∞`-valued variance (#16730)