conv

Statistics

Name	Kind	Assumes	Proves	Validates	Depends On
`conv` 📖	mathematical	`MeasureTheory.Measure.AbsolutelyContinuous`	`MeasureTheory.Measure.HaveLebesgueDecomposition` `MeasureTheory.Measure.conv` `SubNegMonoid.toAddMonoid` `AddGroup.toSubNegMonoid`	—	`MeasureTheory.measurable_lconvolution` `MeasureTheory.Measure.measurable_rnDeriv` `MeasureTheory.Measure.MutuallySingular.zero_left` `zero_add` `MeasureTheory.conv_eq_withDensity_lconvolution_rnDeriv`

Name	Category	Theorems
`conv` 📖	CompOp	38 math math: `conv_zero`, `conv_comm`, `dirac_conv_dirac`, `finite_of_finite_conv`, `ProbabilityTheory.IndepFun.map_add_eq_map_conv_map₀'`, `map_conv_addMonoidHom`, `dirac_conv`, `ProbabilityTheory.IndepFun.hasLaw_fun_add`, `conv_add`, `MeasureTheory.HaveLebesgueDecomposition.conv`, `lintegral_conv_eq_lintegral_sum`, `MeasureTheory.rnDeriv_conv`, `zero_conv`, `ProbabilityTheory.gaussianReal_conv_gaussianReal`, `MeasureTheory.charFun_conv`, `conv_smul_left`, `conv_absolutelyContinuous`, `map_conv_continuousLinearMap`, `lintegral_conv`, `ProbabilityTheory.isGaussian_conv`, `MeasureTheory.conv_withDensity_eq_lconvolution`, `conv_assoc`, `conv_dirac`, `MeasureTheory.rnDeriv_conv'`, `ProbabilityTheory.IsGaussian.integral_dual_conv_map_neg_eq_zero`, `MeasureTheory.conv_eq_withDensity_lconvolution_rnDeriv`, `ProbabilityTheory.IndepFun.map_add_eq_map_conv_map'`, `probabilitymeasure_of_probabilitymeasures_conv`, `sfinite_conv_of_sfinite`, `ProbabilityTheory.IndepFun.map_add_eq_map_conv_map`, `conv_smul_right`, `add_conv`, `conv_dirac_zero`, `MeasureTheory.conv_withDensity_eq_mlconvolution₀`, `ProbabilityTheory.IndepFun.hasLaw_add`, `dirac_zero_conv`, `ProbabilityTheory.IndepFun.map_add_eq_map_conv_map₀`, `MeasureTheory.charFunDual_conv`

---