test module

`Tests.ConditionalResampling`

0 named declarations scanned from Tests/ConditionalResampling.lean.

Imports

AutoSamplingTheory.TechnicalLemmas.Probability.ConditionalResampling

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

Download module (.lean)

import AutoSamplingTheory.TechnicalLemmas.Probability.ConditionalResampling

namespace AutoSamplingTheory.Tests.ConditionalResampling

open MeasureTheory
open scoped ProbabilityTheory
open AutoSamplingTheory.TechnicalLemmas.Probability.ConditionalResampling

variable {α β : Type*} [MeasurableSpace α] [MeasurableSpace β]
  [StandardBorelSpace β] [Nonempty β]

example {μ : Measure (α × β)} [IsFiniteMeasure μ] :
    (μ.map Prod.fst) ⊗ₘ
        ProbabilityTheory.condDistrib Prod.snd Prod.fst μ = μ := by
  exact fst_compProd_condDistrib_snd_eq_self

end AutoSamplingTheory.Tests.ConditionalResampling