OAI/Analysis/RotationWeights/ContinuousWeight.lean

GitHub source file

14 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.ContinuousCircleWeight.concentratedWeight line 86
  2. lemma OAI.ContinuousCircleWeight.concentratedWeight_self line 89
  3. lemma OAI.ContinuousCircleWeight.concentratedWeight_bounds line 92
  4. lemma OAI.ContinuousCircleWeight.concentratedWeight_eq_zero line 101
  5. def OAI.ContinuousCircleWeight.LocallyFiniteOff line 109
  6. lemma OAI.ContinuousCircleWeight.finite_support_of_locallyFiniteOff line 112
  7. lemma OAI.ContinuousCircleWeight.concentratedWeight_continuousAt_off line 121
  8. lemma OAI.ContinuousCircleWeight.concentratedWeight_le_finite line 135
  9. theorem OAI.ContinuousCircleWeight.continuous_concentratedWeight line 149
  10. lemma OAI.ContinuousCircleWeight.negativeLog_concentratedWeight line 173
  11. theorem OAI.ContinuousCircleWeight.lintegral_negativeLog_concentratedWeight line 196
  12. lemma OAI.ContinuousCircleWeight.locallyFiniteOff_of_shrinking_supports line 206
  13. lemma OAI.ContinuousCircleWeight.ae_finite_support_of_support_measure_sum line 224
  14. theorem OAI.ContinuousCircleWeight.concentrated_coboundary line 230