OAI/Analysis/RotationWeights/FiberActions.lean

GitHub source file

36 declarations, 0 contain sorry, 0 declared as axioms

  1. lemma OAI.ContinuousCircleWeight.continuous_bounded_lp_field line 19
  2. lemma OAI.ContinuousCircleWeight.lpDiagonal_norm_le line 51
  3. abbrev OAI.ContinuousCircleWeight.CircleFiberL2 line 63
  4. abbrev OAI.ContinuousCircleWeight.CircleFiberOperator line 64
  5. def OAI.ContinuousCircleWeight.fiberBasis line 65
  6. lemma OAI.ContinuousCircleWeight.fiberBasis_apply line 67
  7. def OAI.ContinuousCircleWeight.circleFiberBasis line 70
  8. lemma OAI.ContinuousCircleWeight.circleFiberBasis_coe line 73
  9. def OAI.ContinuousCircleWeight.continuousPiField line 81
  10. lemma OAI.ContinuousCircleWeight.continuousPiField_apply line 85
  11. lemma OAI.ContinuousCircleWeight.continuousPiField_bound line 89
  12. lemma OAI.ContinuousCircleWeight.continuousPiField_continuous line 93
  13. def OAI.ContinuousCircleWeight.continuousPi line 108
  14. lemma OAI.ContinuousCircleWeight.continuousPi_coe line 113
  15. lemma OAI.ContinuousCircleWeight.continuousPi_norm_le line 117
  16. lemma OAI.ContinuousCircleWeight.continuousPi_add line 121
  17. lemma OAI.ContinuousCircleWeight.continuousPi_mul line 134
  18. lemma OAI.ContinuousCircleWeight.continuousPi_one line 146
  19. lemma OAI.ContinuousCircleWeight.continuousPi_zero line 156
  20. lemma OAI.ContinuousCircleWeight.continuousPi_smul line 166
  21. lemma OAI.ContinuousCircleWeight.continuousPiField_inner_star line 180
  22. lemma OAI.ContinuousCircleWeight.continuousPi_star line 190
  23. def OAI.ContinuousCircleWeight.continuousPiHom line 204
  24. lemma OAI.ContinuousCircleWeight.continuous_continuousPiHom line 215
  25. def OAI.ContinuousCircleWeight.fiberShiftL2 line 225
  26. lemma OAI.ContinuousCircleWeight.fiberShiftL2_coe line 228
  27. lemma OAI.ContinuousCircleWeight.fiberShift_single line 232
  28. lemma OAI.ContinuousCircleWeight.fiberShiftL2_basis line 239
  29. lemma OAI.ContinuousCircleWeight.circleFiberBasis_ext line 246
  30. lemma OAI.ContinuousCircleWeight.regularShift_single line 266
  31. lemma OAI.ContinuousCircleWeight.circleFiberBasis_conj_U line 273
  32. lemma OAI.ContinuousCircleWeight.continuousPi_basis line 282
  33. lemma OAI.ContinuousCircleWeight.regularMagnetic_single line 301
  34. lemma OAI.ContinuousCircleWeight.fourier_one_real line 313
  35. lemma OAI.ContinuousCircleWeight.fourier_one_zsmul_real line 317
  36. lemma OAI.ContinuousCircleWeight.circleFiberBasis_conj_V line 322