Theorem: Composition of Dirac Delta Distribution with Function with Simple Zero

Let $\delta \in \map {\DD'} \R$ be the Dirac delta distribution.
Let $\sequence {\map {\delta_n} x}_{n \mathop \in \N}$ be a delta sequence.
Let $f : \R \to \R$ be a real function with a simple zero at $x_0$.
Let $f$ be strictly monotone.
Let $\phi \in \map \DD \R$ be a test function.
Then in the distributional sense it holds that:
:$\map \delta {\map f x} = \dfrac {\map \delta {x - x_0} } {\size {\map {f'} {x_0} } }$
which can be interpreted as:
:$\ds \int_{-\infty}^\infty \map \delta {\map f x} \map \phi x \rd x = \dfrac {\map \phi {x_0} } {\size {\map {f'} {x_0} } }$
which more strictly means that:
:$\ds \lim_{n \mathop \to \infty} \int_{-\infty}^\infty \map {\delta_n} {\map f x} \map \phi x \rd x = \dfrac {\map \phi {x_0} } {\size {\map {f'} {x_0} } }$

Proof:
Let $H$ be the Heaviside step function.
Let $T \in \map \DD \R$ be a Schwartz distribution associated with $\map H {\map f x}$:
:$T = T_{\map H {\map f x} }$
We have that:
{{begin-eqn}}
{{eqn | l = \map H {\map f x} 
      | r = \begin {cases} \map H {x - x_0} & : \forall x \in \R : \map {f'} x > 0 \\ 1 - \map H {x - x_0} & : \forall x \in \R : \map {f'} x < 0 \end {cases}
}}
{{end-eqn}}
Taking the derivative of the {{LHS}} yields:
{{begin-eqn}}
{{eqn | l = \dfrac \d {\d x} \map H {\map f x}
      | r = \dfrac {\d \map f x} {\d x} \dfrac {\d \map H {\map f x} } {\d \map f x}
}}
{{eqn | r = \map {f'} x \dfrac {\d \map H {\map f x} } {\d \map f x}
}}
{{end-eqn}}
Taking the derivative of the {{RHS}} yields:
:$\forall x \ne x_0 : \dfrac \d {\d x} \map H {\map f x} = 0$
Furthermore:
:$\forall x \in \R : \map {f'} x > 0 : \paren {\map f {x_0^+} = 1} \land \paren {\map f {x_0^-} = 0}$
:$\forall x \in \R : \map {f'} x < 0 : \paren {\map f {x_0^+} = 0} \land \paren {\map f {x_0^-} = 1}$
By Jump Rule the {{RHS}} reads:
{{begin-eqn}}
{{eqn | l = T_{ \map H {\map f x} }' 
      | r = \begin{cases} \delta_{x_0} & : \forall x \in \R : \map {f'} x > 0 \\ -\delta_{x_0} & : \forall x \in \R : \map {f'} x < 0 \end{cases}
}}
{{end-eqn}}
Define the composite Dirac delta distribution according to Distributional Derivative of Heaviside Step Function.
We have that:
:$T_{\map H x}' = \delta_0 = \delta_x$
Then:
{{begin-eqn}}
{{eqn | l = T_{\map H {\map f x} }'
      | r = T_{\map {f'} x \frac {\d \map H {\map f x} } {\d \map f x} }
      | c = Derivative of Composite Function
}}
{{eqn | r = \map {f'} x \delta_{\map f x}
      | c = Multiplication of Distribution induced by Locally Integrable Function by Smooth Function
}}
{{end-eqn}}
Hence:
{{begin-eqn}}
{{eqn | l = \forall x \in \R : \map {f'} x 
      | o = > 
      | r = 0
}}
{{eqn | ll= \leadsto
      | l = \size {\map {f'}  x} \delta_{\map f x}
      | r = \delta_{x_0}
}}
{{eqn | ll= \leadsto
      | l = \delta_{\map f x}
      | r = \frac {\delta_{x_0} } {\size {\map {f'} x} }
}}
{{eqn | r = \frac {\delta_{x_0} } {\size {\map {f'} {x_0} } }
      | c = Product of Smooth Function and Dirac Delta Distribution
}}
{{end-eqn}}
and:
{{begin-eqn}}
{{eqn | l = \forall x \in \R : \map {f'} x 
      | o = < 
      | r = 0
}}
{{eqn | ll= \leadsto
      | l = -\size {\map {f'} x} \delta_{\map f x}
      | r = -\delta_{x_0}
}}
{{eqn | ll= \leadsto
      | l = \delta_{\map f x}
      | r = \frac {\delta_{x_0} } {\size {\map {f'}  x} }
}}
{{eqn | r = \frac {\delta_{x_0} } {\size {\map {f'}  {x_0} } }
      | c = Product of Smooth Function and Dirac Delta Distribution
}}
{{end-eqn}}
{{qed}}
{{Research|The way composite Dirac distribution is introduced here is too sketchy.}}