OAI/Analysis/CircleDomains/Topology/CurveLowerDistance.lean

GitHub source file

3 declarations, 0 contain sorry, 0 declared as axioms

A strict derivative gives lower distance bounds on a small interval. These bounds will supply the reverse arclength inequality.

  1. lemma OAI.CircleDomainRigidity.real_clm_eq_toSpanSingleton line 16
  2. lemma OAI.CircleDomainRigidity.norm_real_clm_apply line 23
  3. lemma OAI.CircleDomainRigidity.local_curve_lower_distance line 30