test module

`Tests.PermutedMarginalReplacement`

0 named declarations scanned from Tests/PermutedMarginalReplacement.lean.

Imports

AutoSamplingTheory.TechnicalLemmas.Measure.PermutedMarginalReplacement

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

Download module (.lean)

import AutoSamplingTheory.TechnicalLemmas.Measure.PermutedMarginalReplacement

#check AutoSamplingTheory.TechnicalLemmas.Measure.PermutedMarginalReplacement.mass_map_of_measurable
#check AutoSamplingTheory.TechnicalLemmas.Measure.PermutedMarginalReplacement.sourceMarginal
#check AutoSamplingTheory.TechnicalLemmas.Measure.PermutedMarginalReplacement.targetMarginal
#check AutoSamplingTheory.TechnicalLemmas.Measure.PermutedMarginalReplacement.sourceMarginal_mass
#check AutoSamplingTheory.TechnicalLemmas.Measure.PermutedMarginalReplacement.targetMarginal_mass
#check AutoSamplingTheory.TechnicalLemmas.Measure.PermutedMarginalReplacement.finiteMeasure_map_finset_sum
#check AutoSamplingTheory.TechnicalLemmas.Measure.PermutedMarginalReplacement.finiteMeasure_map_fintype_sum
#check AutoSamplingTheory.TechnicalLemmas.Measure.PermutedMarginalReplacement.permutedMarginalJoint
#check AutoSamplingTheory.TechnicalLemmas.Measure.PermutedMarginalReplacement.permutedMarginalJoint_map_fst
#check AutoSamplingTheory.TechnicalLemmas.Measure.PermutedMarginalReplacement.permutedMarginalJoint_map_snd
#check AutoSamplingTheory.TechnicalLemmas.Measure.PermutedMarginalReplacement.permutedMarginalJoint_mass
#check AutoSamplingTheory.TechnicalLemmas.Measure.PermutedMarginalReplacement.permutedMarginalReplacement
#check AutoSamplingTheory.TechnicalLemmas.Measure.PermutedMarginalReplacement.permutedMarginalReplacement_map_fst
#check AutoSamplingTheory.TechnicalLemmas.Measure.PermutedMarginalReplacement.permutedMarginalReplacement_map_snd