API docs for Positive distribution

Stream: new members

[Nicholas Wilson]

Where in mathlib would I go looking for things related to positive distributions defined on some domain (a subset of the real line)?

I essentially want to start my proof off with:
let p1 be a positive distribution (with finite area under the curve)
defined on (non-zero on and zero elsewhere) a domain D1 a b from [a,b] ⊂ ℝ
with (¬ (a = ∞ ∧ b = ∞ )) ∧ a ≠ b