← Mathematical handbook

Uniqueness from marginals on a forward contact graph

theorem Verification.forward_graph_marginals_unique (τ : ↑unitInterval → ↑unitInterval) (hτ : Measurable τ) (q : ℝ) (hq : 0 < q) (α β γ δ : MeasureTheory.Measure ↑unitInterval) [MeasureTheory.IsFiniteMeasure α] [MeasureTheory.IsFiniteMeasure β] [MeasureTheory.IsFiniteMeasure γ] [MeasureTheory.IsFiniteMeasure δ] (hα : ∀ᵐ (x : ↑unitInterval) ∂α, ↑x + q ≤ ↑(τ x)) (hβ : ∀ᵐ (x : ↑unitInterval) ∂β, ↑x + q ≤ ↑(τ x)) (hγ : ∀ᵐ (x : ↑unitInterval) ∂γ, ↑x + q ≤ ↑(τ x)) (hδ : ∀ᵐ (x : ↑unitInterval) ∂δ, ↑x + q ≤ ↑(τ x)) (h₁ : α + MeasureTheory.Measure.map τ β = γ + MeasureTheory.Measure.map τ δ) (h₂ : β + MeasureTheory.Measure.map τ α = δ + MeasureTheory.Measure.map τ γ) : α = γ ∧ β = δ

Two pairs of finite measures on a forward graph are determined by their two marginals. The strict positive shift makes the marginal recursion terminate after finitely many strips.