OAI/Analysis/CircleDomains/Probability/CompactLawSplit.lean

GitHub source file

4 declarations, 0 contain sorry, 0 declared as axioms

A finite mixture uniformly controls all compact test configurations if every probability distribution on configurations admits a good candidate. This is the finite splitting step of the manuscript's fusion argument.

  1. def OAI.CircleDomainRigidity.probabilityConvexCombination line 18
  2. theorem OAI.CircleDomainRigidity.integral_probabilityConvexCombination line 26
  3. theorem OAI.CircleDomainRigidity.convex_integral_vectors line 38
  4. theorem OAI.CircleDomainRigidity.exists_finite_compact_law_split line 46