OAI/Analysis/RotationWeights/Decomposable.lean

GitHub source file

14 declarations, 0 contain sorry, 0 declared as axioms

  1. lemma OAI.ContinuousCircleWeight.fieldMulL2_indicator line 25
  2. lemma OAI.ContinuousCircleWeight.indicatorConstLp_eq_indicatorV2 line 42
  3. theorem OAI.ContinuousCircleWeight.commutes_indicators_decomposable line 53
  4. lemma OAI.ContinuousCircleWeight.inner_indicatorV2 line 95
  5. lemma OAI.ContinuousCircleWeight.decomposable_const line 105
  6. lemma OAI.ContinuousCircleWeight.ae_field_eq_of_dense line 113
  7. lemma OAI.ContinuousCircleWeight.decomposable_mul line 123
  8. lemma OAI.ContinuousCircleWeight.decomposable_eq line 131
  9. lemma OAI.ContinuousCircleWeight.decomposable_idempotent line 141
  10. lemma OAI.ContinuousCircleWeight.decomposable_selfAdjoint line 149
  11. def OAI.ContinuousCircleWeight.shiftedL2 line 189
  12. lemma OAI.ContinuousCircleWeight.shiftedL2_coe line 193
  13. lemma OAI.ContinuousCircleWeight.shiftedL2_const line 200
  14. lemma OAI.ContinuousCircleWeight.decomposable_covariance line 208