Uniform table laws for measure-valued computations

Explicit uniform-measure hypotheses suffice to resample or extract table cells. The continuation may return any measurable result space and may lose mass. No sampling implementation or discrete probability representation is required.

theorem evalDist_bind_bind_update {m : Type → Type u_1} [Monad m] [LawfulMonad m] [EvalDistSemantics m] [LawfulEvalDistSemantics m] {D R α : Type} [Finite D] [DecidableEq D] [Finite R] [Nonempty R] [MeasurableSpace R] [MeasurableSingletonClass R] [MeasurableSpace α] (value : m R) (table : m (D → R)) (hvalue : 𝒟[value] = ProbabilityTheory.uniformOn Set.univ) (htable : 𝒟[table] = ProbabilityTheory.uniformOn Set.univ) (t : D) (f : (D → R) → m α) : 𝒟[do let u ← value let g ← table f (Function.update g t u)] = 𝒟[table >>= f]

Independent uniform cell resampling preserves every subsequent observation.

theorem evalDist_bind_bind_update_map {m : Type → Type u_1} [Monad m] [LawfulMonad m] [EvalDistSemantics m] [LawfulEvalDistSemantics m] {D R α : Type} [Finite D] [DecidableEq D] [Finite R] [Nonempty R] [MeasurableSpace R] [MeasurableSingletonClass R] [MeasurableSpace α] (value : m R) (table : m (D → R)) (hvalue : 𝒟[value] = ProbabilityTheory.uniformOn Set.univ) (htable : 𝒟[table] = ProbabilityTheory.uniformOn Set.univ) (t : D) (f : (D → R) → α) : 𝒟[do let u ← value let g ← table pure (f (Function.update g t u))] = 𝒟[do let g ← table pure (f g)]

Independent uniform cell resampling preserves a pure observation of the table.

theorem evalDist_bind_cell_extract {m : Type → Type u_1} [Monad m] [LawfulMonad m] [EvalDistSemantics m] [LawfulEvalDistSemantics m] {D R α : Type} [Finite D] [DecidableEq D] [Finite R] [Nonempty R] [MeasurableSpace R] [MeasurableSingletonClass R] [MeasurableSpace α] (value : m R) (table : m (D → R)) (hvalue : 𝒟[value] = ProbabilityTheory.uniformOn Set.univ) (htable : 𝒟[table] = ProbabilityTheory.uniformOn Set.univ) (t : D) (f : (D → R) → R → m α) : 𝒟[do let g ← table f g (g t)] = 𝒟[do let u ← value let g ← table f (Function.update g t u) u]

Expose a uniform table cell before running the continuation that reads it.

theorem evalDist_map_equiv_of_uniform {m : Type → Type u_1} [Monad m] [LawfulMonad m] [EvalDistSemantics m] [LawfulEvalDistSemantics m] {α : Type} [MeasurableSpace α] [Finite α] [MeasurableSingletonClass α] (draw : m α) (hdraw : 𝒟[draw] = ProbabilityTheory.uniformOn Set.univ) (e : α ≃ α) : 𝒟[⇑e <$> draw] = 𝒟[draw]

Reindexing a finite uniform draw by a permutation preserves its denotation.

theorem evalDist_bind_uniform_equiv {m : Type → Type u_1} [Monad m] [LawfulMonad m] [EvalDistSemantics m] [LawfulEvalDistSemantics m] {α : Type} [MeasurableSpace α] [Finite α] [MeasurableSingletonClass α] {β : Type} [MeasurableSpace β] (draw : m α) (hdraw : 𝒟[draw] = ProbabilityTheory.uniformOn Set.univ) (e : α ≃ α) (f : α → m β) : 𝒟[draw >>= f] = 𝒟[do let x ← draw f (e x)]

Reindexing a finite uniform draw by a permutation preserves every continuation measure.

theorem evalDist_bind_bind_bind_update_two_map {m : Type → Type u_1} [Monad m] [LawfulMonad m] [EvalDistSemantics m] [LawfulEvalDistSemantics m] {D R α : Type} [Finite D] [DecidableEq D] [Finite R] [Nonempty R] [MeasurableSpace R] [MeasurableSingletonClass R] [MeasurableSpace α] (value : m R) (table : m (D → R)) (hvalue : 𝒟[value] = ProbabilityTheory.uniformOn Set.univ) (htable : 𝒟[table] = ProbabilityTheory.uniformOn Set.univ) {t₁ t₂ : D} (hne : t₁ ≠ t₂) (f : (D → R) → α) : 𝒟[do let u₁ ← value let u₂ ← value let g ← table pure (f (Function.update (Function.update g t₁ u₁) t₂ u₂))] = 𝒟[do let g ← table pure (f g)]

Independently resample two distinct table cells before observing the table.

theorem evalDist_map_table_comp_injective {m : Type → Type u_1} [Monad m] [LawfulMonad m] [EvalDistSemantics m] [LawfulEvalDistSemantics m] {R : Type} [Finite R] [Nonempty R] [MeasurableSpace R] [MeasurableSingletonClass R] {A B : Type} [Finite A] [Finite B] (small : m (A → R)) (large : m (B → R)) (hsmall : 𝒟[small] = ProbabilityTheory.uniformOn Set.univ) (hlarge : 𝒟[large] = ProbabilityTheory.uniformOn Set.univ) {e : A → B} (he : Function.Injective e) : 𝒟[(fun (g : B → R) => g ∘ e) <$> large] = 𝒟[small]

An injective table restriction preserves uniformity under explicitly calibrated draws.