OAI/Analysis/CircleDomains/Topology/IntervalPoincare.lean

GitHub source file

3 declarations, 0 contain sorry, 0 declared as axioms

A one-dimensional mean-oscillation bound, keeping the actual integrable derivative in the right-hand side.

  1. lemma OAI.CircleDomainRigidity.interval_increment_le_integral line 13
  2. lemma OAI.CircleDomainRigidity.volume_restrict_Icc_ne_zero line 26
  3. lemma OAI.CircleDomainRigidity.interval_abs_sub_average_le_integral line 34