Zulip Chat Archive

Stream: triage

Topic: PR !4#26156: feat(MeasureTheory.VectorMeasure) : add a de...

Random Issue Bot (Sep 20 2025 at 14:10):

Today I chose PR #26156 for discussion!

feat(MeasureTheory.VectorMeasure) : add a definition of total variation for VectorMeasure
Created by @Oliver Butterley (@oliver-butterley) on 2025-06-19
Labels: awaiting-author, t-measure-probability, new-contributor

Is this PR still relevant? Any recent updates? Anyone making progress?

Last updated: Dec 20 2025 at 21:32 UTC