OAI/Analysis/CircleDomains/Probability/PublishedProbabilityTopology.lean

GitHub source file

2 declarations, 0 contain sorry, 0 declared as axioms

Probability-space topology for fusion.

A. S. Kechris, Classical Descriptive Set Theory, GTM 156 (1995), Theorems 17.23 and 17.24, pp. 112–113, give the Polish weak topology on probability laws on a Polish space and identify its Borel sigma algebra with the evaluation sigma algebra. The following paragraph gives the standard Borel consequence.

  1. def OAI.CircleDomainRigidity.StandardBorelProbabilityLaws line 19
  2. def OAI.CircleDomainRigidity.PolishProbabilityLaws line 22