OAI/Analysis/RotationWeights/FieldExtraction.lean

GitHub source file

14 declarations, 0 contain sorry, 0 declared as axioms

  1. abbrev OAI.ContinuousCircleWeight.VectorL2 line 23
  2. def OAI.ContinuousCircleWeight.indicatorV2 line 25
  3. lemma OAI.ContinuousCircleWeight.indicatorV2_coe line 62
  4. lemma OAI.ContinuousCircleWeight.vectorL2_norm_sq_integral line 66
  5. lemma OAI.ContinuousCircleWeight.indicatorV2_norm_sq line 72
  6. lemma OAI.ContinuousCircleWeight.commutes_indicator_pointwise_bound line 82
  7. def OAI.ContinuousCircleWeight.complexOfRat line 117
  8. lemma OAI.ContinuousCircleWeight.complexOfRat_apply line 139
  9. lemma OAI.ContinuousCircleWeight.complexOfRat_norm_le line 142
  10. def OAI.ContinuousCircleWeight.rationalCore line 147
  11. instance OAI.ContinuousCircleWeight.rationalCore_countable line 150
  12. lemma OAI.ContinuousCircleWeight.rationalCore_I line 159
  13. lemma OAI.ContinuousCircleWeight.rationalCore_dense line 175
  14. theorem OAI.ContinuousCircleWeight.extract_bounded_field line 185