OAI/Geometry/Riemannian/HarmonicCore/WarpingBounds.lean

GitHub source file

11 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.HarmonicCounterexample.tailBarrier line 17
  2. lemma OAI.HarmonicCounterexample.tailBarrier_hasDerivAt line 20
  3. lemma OAI.HarmonicCounterexample.tailBarrier_antitone line 38
  4. lemma OAI.HarmonicCounterexample.b_deriv_transient_bound line 57
  5. def OAI.HarmonicCounterexample.transientWeight line 80
  6. lemma OAI.HarmonicCounterexample.transientWeight_hasDerivAt line 82
  7. lemma OAI.HarmonicCounterexample.transientWeight_antitone line 91
  8. lemma OAI.HarmonicCounterexample.transient_uniform line 108
  9. lemma OAI.HarmonicCounterexample.b_uniform_bounds line 129
  10. lemma OAI.HarmonicCounterexample.transient_eventually_small line 169
  11. theorem OAI.HarmonicCounterexample.scalar_warping_realization line 181