Measure semantics for finite-range sampling

The finite-range oracle is interpreted by a native uniform measure. Its event law is stated directly in the measure-backed probability notation and exposes exact finite cardinality only when the event predicate is decidable.

@[simp]

theorem ProbComp.evalDist_uniformFin (n : ℕ) : 𝒟[$[0..n]] = ProbabilityTheory.uniformOn Set.univ

A finite-range draw denotes the uniform measure chosen for its oracle response.

theorem ProbComp.lintegral_evalDist_uniformFin (n : ℕ) (f : Fin (n + 1) → ENNReal) : ∫⁻ (i : Fin (n + 1)), f i ∂𝒟[$[0..n]] = (∑ i : Fin (n + 1), f i) / (↑n + 1)

Integrating a finite-range draw is a finite average, including for infinite integrands.

theorem ProbComp.prEvent_uniformFin (n : ℕ) (p : Fin (n + 1) → Prop) [DecidablePred p] : 𝒟[do let x ← $[0..n] pure (p x)] {True} = ↑(Finset.filter p Finset.univ).card / (↑n + 1)

A decidable event on a finite-range draw has its normalized cardinality.