Organization of Multiplication of "Random Variables"

Stream: mathlib4

[David Ledvinka]

I am wondering where I should put the following theorems (and variations) in possibly one or multiple files.

theorem IndepFun.map_mul_eq_map_mconv_map [MeasurableMul₂ M]
    {f g : Ω → M} (hf : AEMeasurable f μ) (hg : AEMeasurable g μ) (hfg : IndepFun f g μ) :
    μ.map (f * g) = (μ.map f) ∗ (μ.map g)

theorem mconv_withDensity_eq_mlconvolution {f g : G → ℝ≥0∞}
    (hf : AEMeasurable f π) (hg : AEMeasurable g π) :
    π.withDensity f ∗ π.withDensity g = π.withDensity (f ⋆ₗ[π] g)

theorem IndepFun.map_mul_eq_pdf_mlconvolution {μ : Measure Ω} [IsFiniteMeasure μ]
     {f g : Ω → G} (hf : AEMeasurable f μ) (hg : AEMeasurable g μ)
    (hfg : IndepFun f g μ) [HasPDF f μ π] [HasPDF g μ π] :
    pdf (f * g) μ π =ᶠ[ae π] (pdf f μ π) ⋆ₗ[π] (pdf g μ π)

[Yaël Dillies]

What does #min_imports in before each of these say?

[Ruben Van de Velde]

TIL about #min_imports in

[David Ledvinka]

First one has min imports

import Mathlib.MeasureTheory.Group.Convolution
import Mathlib.Probability.Independence.Basic
import Init.Data.List.Nat.Pairwise

Second one has min imports

import Mathlib.Analysis.LConvolution
import Mathlib.MeasureTheory.Group.Convolution
import Mathlib.MeasureTheory.Measure.WithDensity
import Init.Data.List.Nat.Pairwise

Third one has min imports

import Mathlib.Analysis.LConvolution
import Mathlib.Probability.Density
import Mathlib.MeasureTheory.Group.Convolution
import Init.Data.List.Nat.Pairwise