OAI/Analysis/CircleDomains/Selection/AtomlessQuantiles.lean

GitHub source file

5 declarations, 0 contain sorry, 0 declared as axioms

Separated positive-mass intervals for an atomless real probability law. These provide the four collar arcs in the crossing argument after choosing a circle coordinate.

  1. theorem OAI.CircleDomainRigidity.atomless_cdf_leftLim line 16
  2. theorem OAI.CircleDomainRigidity.continuous_atomless_cdf line 22
  3. theorem OAI.CircleDomainRigidity.exists_atomless_quantile line 29
  4. theorem OAI.CircleDomainRigidity.atomless_measure_Ioo_cdf line 38
  5. theorem OAI.CircleDomainRigidity.exists_eight_ordered_quantiles line 43