Recovering joint probability mass from one marginal

1. Let \(\pi_1:\alpha\times\beta\to\alpha\) be the first projection, which is measurable for the product measurable structure. The inverse image of the whole first space is the whole product space: \[\pi_1^{-1}(\alpha)=\alpha\times\beta.\]

2. By the definition of pushforward mass and the prescribed first marginal, \[\gamma(\alpha\times\beta)=(\gamma.\mathrm{fst})(\alpha)=\mu(\alpha)=1.\] The last equality is exactly the probability assumption on \(μ\).

3. A measure of total mass one is a probability measure. Thus \(γ\) has the required probability interface; its finiteness is a consequence, not an extra premise used to obtain the mass identity.

4. This deduction uses only the first marginal identity. The second marginal remains part of the coupling data but no separate probability assumption on \(ν\) is needed. This local mass result asserts no optimality, moment bound or integrability of arbitrary unbounded functions.

/- SamplingOptimisationGeometryBench public-dev reference.
   Reuses the existing project proof; retain LICENSE and NOTICE. -/
import Mathlib.MeasureTheory.Measure.Prod

open MeasureTheory
namespace AutoSamplingTheory.TechnicalLemmas.Measure.Transport
def IsCoupling {α β : Type*} [MeasurableSpace α] [MeasurableSpace β]
    (γ : Measure (α × β)) (μ : Measure α) (ν : Measure β) : Prop :=
  γ.fst = μ ∧ γ.snd = ν
end AutoSamplingTheory.TechnicalLemmas.Measure.Transport
open AutoSamplingTheory.TechnicalLemmas.Measure.Transport

example
    {α β : Type*} [MeasurableSpace α] [MeasurableSpace β]
    {γ : Measure (α × β)} {μ : Measure α} {ν : Measure β}
    [IsProbabilityMeasure μ] (hγ : IsCoupling γ μ ν) :
    IsProbabilityMeasure γ := by
  constructor
  rw [← Measure.fst_univ, hγ.1, measure_univ]

1. Reduces joint probability normalization to proving \(γ\) has total mass one, without assuming \(γ\) is already finite or a probability measure. (1 point)
2. Uses the measurable first projection and its inverse image of the whole space to identify joint mass with first-marginal mass. (1 point)
3. Uses \(γ.fst=μ\) and \(μ\) being a probability measure to obtain the exact mass one. (1 point)
4. Identifies that the second-marginal identity is unused in this calculation and does not add a probability premise on \(ν\). (1 point)

/- SamplingOptimisationGeometryBench public-dev reference.
   Reuses the existing project proof; retain LICENSE and NOTICE. -/
import Mathlib.MeasureTheory.Measure.Prod

open MeasureTheory
namespace AutoSamplingTheory.TechnicalLemmas.Measure.Transport
def IsCoupling {α β : Type*} [MeasurableSpace α] [MeasurableSpace β]
    (γ : Measure (α × β)) (μ : Measure α) (ν : Measure β) : Prop :=
  γ.fst = μ ∧ γ.snd = ν
end AutoSamplingTheory.TechnicalLemmas.Measure.Transport
open AutoSamplingTheory.TechnicalLemmas.Measure.Transport

example
    {α β : Type*} [MeasurableSpace α] [MeasurableSpace β]
    {γ : Measure (α × β)} {μ : Measure α} {ν : Measure β}
    [IsProbabilityMeasure μ] (hγ : IsCoupling γ μ ν) :
    IsProbabilityMeasure γ := by
  -- Replace this comment with your proof.

Download task template

The given context reproduces the existing public IsCoupling definition exactly; it is not a new library lemma, and the target module is not imported. The constructor tactic reduces IsProbabilityMeasure \(γ\) to its total-mass field. Rewriting by the reverse of Measure.fst_univ turns joint mass into first-marginal mass, hγ.1 substitutes \(μ\), and measure_univ uses the existing probability instance for \(μ\). The second conjunct hγ.2 is not needed. This is a fixed-target reconstruction, not a claim of finite moments or a solved transport problem.

/- SamplingOptimisationGeometryBench public-dev reference.
   Reuses the existing project proof; retain LICENSE and NOTICE. -/
import Mathlib.MeasureTheory.Measure.Prod

open MeasureTheory
namespace AutoSamplingTheory.TechnicalLemmas.Measure.Transport
def IsCoupling {α β : Type*} [MeasurableSpace α] [MeasurableSpace β]
    (γ : Measure (α × β)) (μ : Measure α) (ν : Measure β) : Prop :=
  γ.fst = μ ∧ γ.snd = ν
end AutoSamplingTheory.TechnicalLemmas.Measure.Transport
open AutoSamplingTheory.TechnicalLemmas.Measure.Transport

example
    {α β : Type*} [MeasurableSpace α] [MeasurableSpace β]
    {γ : Measure (α × β)} {μ : Measure α} {ν : Measure β}
    [IsProbabilityMeasure μ] (hγ : IsCoupling γ μ ν) :
    IsProbabilityMeasure γ := by
  constructor
  rw [← Measure.fst_univ, hγ.1, measure_univ]

Download runnable reference