Proof obligation for `sampledFrom_inj` in `src/Bluebell/Logic/Ownership.lean`

[alexanderlhicks]

A proof in src/Bluebell/Logic/Ownership.lean contains a sorry.

🤖 AI Analysis:

Statement Explanation

This theorem, sampledFrom_inj, establishes a uniqueness property for probability distributions within the hyper-assertion logic. It states that if an expression E at a specific index i is asserted to be sampled from a probability mass function (PMF) μ, and simultaneously asserted to be sampled from another PMF μ', then these two PMFs must be identical (μ = μ').

The hypothesis is a conjunction (HyperAssertion.and) of two assertSampledFrom assertions. The conclusion is a pure assertion, which lifts the standard proposition μ = μ' into the logic. Essentially, this rule allows you to deduce the equality of two distributions from the fact that they both describe the same random variable.

Context

This theorem is a fundamental rule for ensuring consistency in probabilistic reasoning. It's an "injectivity" property for the assertSampledFrom assertion constructor. Without this rule, the logic could potentially hold contradictory information about the distribution of a variable.

The proof relies on digging into the definitions of assertSampledFrom, ownIndexedProb, and the structure of the underlying resource model, IndexedPSpPm. A key insight is that owning a probability space resource (ownIndexedProb) constrains the underlying ProbabilitySpace to be a specific one. The structure of the PSpPm CMRA, particularly its compatibility predicate, prevents owning a "top" or "universal" probability space that would otherwise break this uniqueness. This theorem connects the abstract logical assertions with the concrete properties of the mathematical model of probability spaces.

Proof Suggestion

1. Start by unfolding the HyperAssertion.entails definition. This will give you a resource x and the hypothesis that x satisfies the and of the two assertSampledFrom assertions.
2. Unfold HyperAssertion.and and assertSampledFrom. This will introduce two existentially quantified families of probability spaces, let's call them P and P'. You will also get propositions stating that μ.toMeasure is the pushforward measure of (P i).μ along E, and similarly for μ' and P'.
3. The core of the argument is to show that these two families of probability spaces must be identical, i.e., P = P'. To do this, unpack the ownIndexedProb assertions. You will find that for each index j, the resource x j must be an upper bound for both a resource constructed from P j and one from P' j.
4. The definition of the PSpPm CMRA is crucial here. The compatibility predicate within PSpPm rules out the possibility of the probability space component of x j being ⊤ (the top element). This forces P j and P' j to be equal to the space owned by x j.
5. Since P = P', it follows that P i = P' i.
6. Substitute this equality into the measure equations obtained in step 2. You will find that μ.toMeasure = μ'.toMeasure.
7. Use the injectivity of the toMeasure function for PMFs, such as PMF.toMeasure_inj or PMF.ext_iff_toMeasure_eq, to conclude that μ = μ'. Note that this may require an assumption like [MeasurableSingletonClass β].
8. Finally, unfold HyperAssertion.pure in the goal and use the derived equality μ = μ' to complete the proof. Useful tactics for this proof will be intro, rcases, unfold, simp, and rw.

Goal: Replace the sorry with a complete proof.

Link to the sorry on GitHub

Code Snippet:

theorem sampledFrom_inj {β : Type*} [MeasurableSpace β]
    {i : I} {E : (α → V) → β} {μ μ' : PMF β} :
    HyperAssertion.entails
      (HyperAssertion.and
        (assertSampledFrom (I := I) (α := α) (V := V) (F := F) i E μ)
        (assertSampledFrom (I := I) (α := α) (V := V) (F := F) i E μ'))
      (HyperAssertion.pure (μ = μ')) := by
  sorry