test module

`Tests.DisplacementInterpolation`

0 named declarations scanned from Tests/DisplacementInterpolation.lean.

Imports

AutoSamplingTheory.TechnicalLemmas.Measure.DisplacementInterpolation

Imported by

Tests

Placeholder scan

0 declaration(s) flagged

Gate status

Partial

Declarations

This aggregator contains no named declarations.

Complete Lean source

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

Download module (.lean)

import AutoSamplingTheory.TechnicalLemmas.Measure.DisplacementInterpolation

namespace AutoSamplingTheory.Tests.DisplacementInterpolation

open AutoSamplingTheory.TechnicalLemmas.Measure.DisplacementInterpolation

#check IsQuadraticOptimalCoupling
#check displacementInterpolation
#check displacementInterpolation_zero
#check displacementInterpolation_one
#check IsWassersteinGeodesic
#check isWassersteinGeodesic_displacementInterpolation
#check endpoints_of_isWassersteinGeodesic

end AutoSamplingTheory.Tests.DisplacementInterpolation