Squared Helliger distance #
Main definitions #
FooBar
Main statements #
fooBar_unique
Notation #
Implementation details #
noncomputable def
ProbabilityTheory.sqHellinger
{α : Type u_1}
{mα : MeasurableSpace α}
(μ : MeasureTheory.Measure α)
(ν : MeasureTheory.Measure α)
:
Squared Hellinger distance between two measures.
Equations
- ProbabilityTheory.sqHellinger μ ν = (ProbabilityTheory.fDiv (fun (x : ℝ) => 2⁻¹ * (1 - √x) ^ 2) μ ν).toReal