OAI/Geometry/Cannon/ScalarLimits/Osc.lean

GitHub source file

12 declarations, 0 contain sorry, 0 declared as axioms

  1. lemma OAI.CannonScales.inverse_geometric_tendsto_zero line 29
  2. lemma OAI.CannonScales.inverse_geometric_antitone line 33
  3. theorem OAI.CannonScales.exists_spaced_geometric line 39
  4. theorem OAI.CannonScalarLimit.finite_measure_subsequence line 70
  5. theorem OAI.CannonScalarLimit.scalar_subsequence line 91
  6. def OAI.CannonScalarLimit.osc line 127
  7. lemma OAI.CannonScalarLimit.continuous_osc line 130
  8. lemma OAI.CannonScalarLimit.tendsto_osc line 135
  9. theorem OAI.CannonScalarLimit.closed_domination_limit line 141
  10. theorem OAI.CannonScalarLimit.oscillation_measure_limit line 168
  11. theorem OAI.CannonScalarLimit.atomic_record_equicontinuous line 187
  12. theorem OAI.CannonScalarLimit.atomic_record_limit line 248