test module

`Tests.WassersteinTriangleExact`

0 named declarations scanned from Tests/WassersteinTriangleExact.lean.

Imports

AutoSamplingTheory.TechnicalLemmas.Measure.WassersteinTriangleExact

Imported by

No local reverse import.

Placeholder scan

0 declaration(s) flagged

Gate status

Partial

Declarations

This aggregator contains no named declarations.

Complete Lean source

Tests/WassersteinTriangleExact.lean — full module with imports and context

Download module (.lean)

import AutoSamplingTheory.TechnicalLemmas.Measure.WassersteinTriangleExact

namespace AutoSamplingTheory.Tests.WassersteinTriangleExact

open MeasureTheory
open scoped ENNReal
open AutoSamplingTheory.TechnicalLemmas.Measure

#check WassersteinTriangleExact.wassersteinDistance_le_add_of_lt_left
#check WassersteinTriangleExact.wassersteinDistance_triangle

example {E : Type*} [NormedAddCommGroup E]
    [MeasurableSpace E] [BorelSpace E] [SecondCountableTopology E]
    [StandardBorelSpace E] [Nonempty E]
    (μ₁ μ₂ μ₃ : Measure E)
    [IsProbabilityMeasure μ₁] [IsProbabilityMeasure μ₂] [IsProbabilityMeasure μ₃] :
    WassersteinSpace.wassersteinDistance μ₁ μ₃ ≤
      WassersteinSpace.wassersteinDistance μ₁ μ₂ +
        WassersteinSpace.wassersteinDistance μ₂ μ₃ :=
  WassersteinTriangleExact.wassersteinDistance_triangle μ₁ μ₂ μ₃

end AutoSamplingTheory.Tests.WassersteinTriangleExact