test module

`Tests.WassersteinSymmetry`

0 named declarations scanned from Tests/WassersteinSymmetry.lean.

Imports

AutoSamplingTheory.TechnicalLemmas.Measure.WassersteinSymmetry

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/WassersteinSymmetry.lean — full module with imports and context

Download module (.lean)

import AutoSamplingTheory.TechnicalLemmas.Measure.WassersteinSymmetry

namespace AutoSamplingTheory.Tests.WassersteinSymmetry

open MeasureTheory
open scoped ENNReal
open AutoSamplingTheory.TechnicalLemmas.Measure

#check WassersteinSymmetry.isCoupling_map_swapPair
#check WassersteinSymmetry.lintegral_quadraticCost_map_swapPair
#check WassersteinSymmetry.wassersteinDistance_le_reverse
#check WassersteinSymmetry.wassersteinDistance_comm

example {E : Type*} [NormedAddCommGroup E]
    [MeasurableSpace E] [BorelSpace E] [SecondCountableTopology E]
    (μ ν : Measure E) :
    WassersteinSpace.wassersteinDistance μ ν =
      WassersteinSpace.wassersteinDistance ν μ :=
  WassersteinSymmetry.wassersteinDistance_comm μ ν

end AutoSamplingTheory.Tests.WassersteinSymmetry