Total bounded screened bit predictors
Abstract
Total bounded screened bit predictors
Theorem 1.1 (Conditioning inside a screened pair).
Lean statement: D5/S3/Observer/ProbabilisticClosure/TrajectoryLaws/ScreenedBinaryPredictor.screened_binary_predictor
Proof. Machine-checked in Lean as D5/S3/Observer/ProbabilisticClosure/TrajectoryLaws/ScreenedBinaryPredictor.screened_binary_predictor (✓ std3). ∎
Source. Repository-derived.
Commentary.
Let Omega be a standard Borel measurable probability space with probability measure mu. Let Q be measurable, let U and V be nonempty standard Borel spaces, and assume the Mathlib CountableOrCountablyGenerated condition for Q and V. Take measurable maps q:Omega to Q, u:Omega to U, v:Omega to V and x:Omega to Bool. Assume u and the pair (v,x) are conditionally independent under mu given the sigma-algebra generated by q. Then there exists a measurable real-valued function g on the entire product Q times V, bounded between zero and one at every product point, such that the conditional expectation of the indicator of x=true given (q,(u,v)) equals g(q,v) mu-almost everywhere.
The predictor is the mass of true in the total Markov conditional kernel obtained by disintegrating the actual conditional distribution of (v,x) given q. Product-measure rectangle identities show that the same conditional kernel remains valid after adjoining the screened u coordinate. Conditional-distribution uniqueness identifies it with the actual conditional expectation. Pointwise Markov bounds apply also to pairs outside the support of the actual (q,v) law. Substitution of a wrong predicted class therefore remains measurable and bounded; no null-fiber division or separate probability law is introduced.