OAI/Analysis/CircleDomains/Probability/ClosedSubsetHitFusion.lean

GitHub source file

1 declarations, 0 contain sorry, 0 declared as axioms

The fusion theorem applied to a closed dust subset. Its tests are ordinary ambient measures supported on the dust, exactly as in the modulus extraction.

  1. theorem OAI.CircleDomainRigidity.exists_hit_norm_mixture_on_closed_subset line 19