OAI/Analysis/RotationWeights/Covariance.lean

GitHub source file

21 declarations, 0 contain sorry, 0 declared as axioms

  1. lemma OAI.ContinuousCircleWeight.fiberShiftL2_indicator line 26
  2. lemma OAI.ContinuousCircleWeight.continuousPi_indicator line 43
  3. def OAI.ContinuousCircleWeight.circleJ line 61
  4. lemma OAI.ContinuousCircleWeight.circleJ_coe line 66
  5. lemma OAI.ContinuousCircleWeight.fiberShiftL2_circleJ line 70
  6. lemma OAI.ContinuousCircleWeight.continuousPiField_covariance line 85
  7. lemma OAI.ContinuousCircleWeight.continuousPi_circleJ line 94
  8. lemma OAI.ContinuousCircleWeight.doubleCentralizer_commute line 107
  9. lemma OAI.ContinuousCircleWeight.regular_doubleCentralizer_indicators line 124
  10. lemma OAI.ContinuousCircleWeight.regular_doubleCentralizer_circleJ line 142
  11. lemma OAI.ContinuousCircleWeight.invariant_eigenvector_zero line 165
  12. lemma OAI.ContinuousCircleWeight.invariant_eigenvector_one line 179
  13. lemma OAI.ContinuousCircleWeight.projection_diagonal_norm_sq line 189
  14. lemma OAI.ContinuousCircleWeight.projection_diagonal_strict line 198
  15. lemma OAI.ContinuousCircleWeight.ergodic_ae_ne_of_preimage_zero line 224
  16. lemma OAI.ContinuousCircleWeight.ergodic_ae_ne_of_zero_preimage line 239
  17. lemma OAI.ContinuousCircleWeight.covariant_field_zero line 257
  18. lemma OAI.ContinuousCircleWeight.covariant_field_one line 285
  19. lemma OAI.ContinuousCircleWeight.decomposable_eq_zero line 304
  20. lemma OAI.ContinuousCircleWeight.decomposable_eq_one line 317
  21. lemma OAI.ContinuousCircleWeight.invariant_covariant_diagonal_strict line 331