OAI/Analysis/CircleDomains/Probability/BorelFamilyHitFusion.lean

GitHub source file

1 declarations, 0 contain sorry, 0 declared as axioms

Apply compact-dust fusion to a Borel, mixture-closed family of code laws. The compatible Polish refinement is constructed from the published probability-space topology inputs and Mathlib's refinement theorem.

  1. theorem OAI.CircleDomainRigidity.exists_law_in_borel_family_with_hit_bound line 22