OAI/Analysis/CircleDomains/Rigidity/PerturbedMeanFreeTrace.lean

GitHub source file

2 declarations, 0 contain sorry, 0 declared as axioms

At a point avoided by the compact arc law, a vanishing correction leaves a genuine mean trace. Its entire interval-band fiber is therefore the single value used in ordered compatibility.

  1. theorem OAI.CircleDomainRigidity.tendsto_perturbed_mean_at_avoided_point line 16
  2. theorem OAI.CircleDomainRigidity.perturbed_mean_band_at_avoided_point line 31