OAI/Analysis/Crouzeix/Fourier.lean

GitHub source file

50 declarations, 0 contain sorry, 0 declared as axioms

Fourier.

  1. abbrev OAI.CrouzeixHilbert.Boundary.CircleSpace line 16
  2. abbrev OAI.CrouzeixHilbert.Boundary.circleMeasure line 20
  3. abbrev OAI.CrouzeixHilbert.Boundary.BoundaryL2 line 22
  4. def OAI.CrouzeixHilbert.Boundary.lpEntry line 24
  5. lemma OAI.CrouzeixHilbert.Boundary.lpEntry_apply_ae line 27
  6. def OAI.CrouzeixHilbert.Boundary.matrixFourier line 31
  7. lemma OAI.CrouzeixHilbert.Boundary.matrixFourier_apply_ae line 36
  8. lemma OAI.CrouzeixHilbert.Boundary.inner_matrixFourier line 41
  9. lemma OAI.CrouzeixHilbert.Boundary.lpEntry_matrixFourier line 50
  10. lemma OAI.CrouzeixHilbert.Boundary.orthonormal_matrixFourier line 63
  11. lemma OAI.CrouzeixHilbert.Boundary.lpEntry_ext line 74
  12. lemma OAI.CrouzeixHilbert.Boundary.matrixFourier_orthogonal_eq_bot line 84
  13. def OAI.CrouzeixHilbert.Boundary.matrixFourierBasis line 100
  14. lemma OAI.CrouzeixHilbert.Boundary.matrixFourierBasis_apply line 104
  15. lemma OAI.CrouzeixHilbert.Boundary.matrixFourierBasis_repr line 108
  16. def OAI.CrouzeixHilbert.Boundary.l2Mask line 113
  17. lemma OAI.CrouzeixHilbert.Boundary.l2Mask_apply line 132
  18. lemma OAI.CrouzeixHilbert.Boundary.l2Mask_self_adjoint line 135
  19. def OAI.CrouzeixHilbert.Boundary.frequencyPart line 146
  20. lemma OAI.CrouzeixHilbert.Boundary.frequencyPart_zero line 149
  21. lemma OAI.CrouzeixHilbert.Boundary.frequencyPart_pos line 152
  22. lemma OAI.CrouzeixHilbert.Boundary.frequencyPart_neg line 155
  23. def OAI.CrouzeixHilbert.Boundary.fourierProjC line 158
  24. lemma OAI.CrouzeixHilbert.Boundary.repr_fourierProjC line 164
  25. lemma OAI.CrouzeixHilbert.Boundary.fourierProjC_self_adjoint line 171
  26. lemma OAI.CrouzeixHilbert.Boundary.fourierProjC_comp line 184
  27. lemma OAI.CrouzeixHilbert.Boundary.fourierProjC_total line 204
  28. lemma OAI.CrouzeixHilbert.Boundary.boundary_real_inner line 219
  29. def OAI.CrouzeixHilbert.Boundary.fourierSplitting line 230
  30. lemma OAI.CrouzeixHilbert.Boundary.repr_lpStar line 252
  31. lemma OAI.CrouzeixHilbert.Boundary.lpStar_fourierProj_zero line 264
  32. lemma OAI.CrouzeixHilbert.Boundary.lpStar_fourierProj_pos line 271
  33. def OAI.CrouzeixHilbert.Boundary.fourierInvolution line 279
  34. def OAI.CrouzeixHilbert.Boundary.matrixMean line 285
  35. lemma OAI.CrouzeixHilbert.Boundary.repr_zero_eq_mean line 288
  36. lemma OAI.CrouzeixHilbert.Boundary.mean_eq_zero_iff line 294
  37. lemma OAI.CrouzeixHilbert.Boundary.norm_fourier_proj_le line 314
  38. def OAI.CrouzeixHilbert.Boundary.upperTransfer line 317
  39. lemma OAI.CrouzeixHilbert.Boundary.upperTransfer_range line 321
  40. lemma OAI.CrouzeixHilbert.Boundary.norm_upperTransfer_le line 329
  41. def OAI.CrouzeixHilbert.Boundary.boundaryCauchyAdjoint line 339
  42. def OAI.CrouzeixHilbert.Boundary.boundaryCauchy line 343
  43. lemma OAI.CrouzeixHilbert.Boundary.adjoint_boundaryCauchy line 348
  44. lemma OAI.CrouzeixHilbert.Boundary.adjoint_boundaryCauchyAdjoint line 354
  45. lemma OAI.CrouzeixHilbert.Boundary.boundaryCauchyAdjoint_idempotent line 358
  46. lemma OAI.CrouzeixHilbert.Boundary.boundaryCauchy_idempotent line 370
  47. lemma OAI.CrouzeixHilbert.Boundary.boundaryCauchy_weighted_norm_sq line 376
  48. lemma OAI.CrouzeixHilbert.Boundary.boundaryCauchy_mean line 382
  49. lemma OAI.CrouzeixHilbert.Boundary.boundaryCauchyAdjoint_mean line 395
  50. theorem OAI.CrouzeixHilbert.Boundary.fourier_ordered_comparison line 405