Product spaces for hyperreal and full conditional probabilities

I think the following is a consequence of a hyperreal variant of the Horn-Tarski extension theorem for measures on boolean algebras:

Claim: Suppose that <Ω_i, F_i, P_i> for i ∈ I is a finitely additive probability space with values in some field R^* of hyperreals. Then, assuming the Axiom of Choice, there is a hyperreal-valued finitely additive probability space <Ω, 2^Ω, P> where Ω = ∏_i ∈ IΩ_i and where the Ω_i-valued random variables π_i given by the natural projections of Ω to Ω_i are independent and have the distributions given by the P_i.

Note that the values of P might be in a hyperreal field larger than R^*.

Given the Claim, and given the well-known correspondences between hyperreal-valued probabilities and full conditional real-valued probabilities, it follows that we can define meaningful product-space conditional real-valued probabilities.

It would be really nice if the product-space conditional probabilities were unique in the special case where F_i is the power set of Ω_i, or at least if they were close enough to uniqueness to define the same real-valued conditional probabilities.

For a particularly interesting case, consider the case where X and Y are generated by uniform throws of a dart at the interval [0, 1], and we have a regular finitely additive hyperreal-valued probability on [0, 1] (regular meaning that all non-empty sets have positive measure). Let Z be the point (X, Y) in the unit square.

Looking at how the proof of the Horn-Tarski extension theorem works, it seems to me that for any positive real number r, and any non-trivial line segment L along the x = y diagonal in the square [0, 1]², there is a product measure P satisfying the conditions of the Claim (where P₁ and P₂ are the uniform measures on [0, 1]) such that P(L)=rP(H), where H is the horizontal line segment {(x, 0):x ∈ [0, 1]}. For instance, if L is the full diagonal, we would intuitively expect P(L)=2^1/2P(H), but in fact we can make P(L)=100000P(H) or P(L)=P(H)/100000 if we like. It is clear that such a discrepancy will generate different conditional probabilities.

I haven’t checked all the details yet, so this could be all wrong.

But if it is right, here is a philosophical upshot. We would expect there to be a unique canonical product probability for independent random variables. However, if we insist on probabilities that are so fine-grained as to tell infinitesimal differences apart, then we do not at present have any such unique canonical product probability. If we are to have one, we need some condition going beyond independence.

This is part of a larger set of claims, namely that we do not at present have a clear notion of what “uniform probability” means once we make our probabilities more finegrained than classical real-valued probability.

Putative Sketch of Proof of Claim: Embedding R^* in a larger field if necessary, we may assume that R^* is |2^Ω|-saturated. Define a product measure on the cylinder subsets of Ω as usual. The proof of the Horn-Tarski extension theorem for measures on boolean algebras looks to me like it works for |B|-saturated hyperreal-valued probability measures where B is the boolean algebra, and completes the proof of our claim.