OAI/Analysis/CircleDomains/Selection/MeanBranchTransitions.lean

GitHub source file

2 declarations, 0 contain sorry, 0 declared as axioms

The actual mean branches have integer transitions before and after adding a common smoothing correction. Thus their interval bands glue.

  1. theorem OAI.CircleDomainRigidity.mean_logarithmic_branches_eventually_add_int line 18
  2. theorem OAI.CircleDomainRigidity.perturbed_mean_branches_eventually_add_int line 46