how to implement an integration rule ?

Question

Suppose I've checked the identity below, how to implement it in Mathematica ?

(* {\[Alpha] \[Element] Reals, \[Beta] \[Element] Reals, \[Mu] \[Element] Reals, \[Sigma] > 0} *)

Integrate[CDF[NormalDistribution[0, 1], \[Alpha] + \[Beta] x] PDF[
NormalDistribution[\[Mu], \[Sigma]], 
x], {x, -\[Infinity], \[Infinity]}] -> CDF[NormalDistribution[0, 1], (\[Alpha] + 
\[Beta] \[Mu])/Sqrt[1 + \[Beta]^2 \[Sigma]^2]]

Answer 1

Most ways to do what you request would probably involve adding rules to built-in functions (such as Integrate, CDF, PDF, etc), which may not be a good option. Here is a slightly softer way, using the Block trick - based macro:

ClearAll[withIntegrationRule];
SetAttributes[withIntegrationRule, HoldAll];
withIntegrationRule[code_] :=
   Block[{CDF, PDF, Integrate, NormalDistribution},
      Integrate[
        CDF[NormalDistribution[0, 1], \[Alpha]_ + \[Beta]_ x_] PDF[
           NormalDistribution[\[Mu]_, \[Sigma]_], x_], {x_, -\[Infinity], \[Infinity]}] :=
                CDF[NormalDistribution[0, 1], (\[Alpha] + \[Beta] \[Mu])/
                   Sqrt[1 + \[Beta]^2 \[Sigma]^2]];
      code];

Here is how we can use it:

In[27]:= 
withIntegrationRule[a=Integrate[CDF[NormalDistribution[0,1],\[Alpha]+\[Beta] x]
    PDF[NormalDistribution[\[Mu],\[Sigma]],x],{x,-\[Infinity],\[Infinity]}]];
a

Out[28]= 1/2 Erfc[-((\[Alpha]+\[Beta] \[Mu])/(Sqrt[2] Sqrt[1+\[Beta]^2 \[Sigma]^2]))]   

When our rule does not match, it will still work, automatically switching to the normal evaluation route:

In[36]:= 
  Block[{$Assumptions = \[Alpha]>0&&\[Beta]==0&&\[Mu]>0&&\[Sigma]>0},
    withIntegrationRule[b=Integrate[CDF[NormalDistribution[0,1],\[Alpha]+\[Beta] x]
        PDF[NormalDistribution[\[Mu],\[Sigma]],x],{x,0,\[Infinity]}]]]

Out[36]= 1/4 (1+Erf[\[Alpha]/Sqrt[2]]) (1+Erf[\[Mu]/(Sqrt[2] \[Sigma])])

where I set \[Alpha] to 0 in assumptions to make the integration possible in a closed form.

Another alternative may be to implement your own special-purpose integrator.