OAI/Analysis/NumericalRange/FourierResolution.lean

GitHub source file

44 declarations, 0 contain sorry, 0 declared as axioms

  1. structure OAI.CompleteCrouzeix.FourierResolution line 27
  2. lemma OAI.CompleteCrouzeix.norm_sq_add_orthogonal line 34
  3. lemma OAI.CompleteCrouzeix.FourierResolution.decompose line 43
  4. lemma OAI.CompleteCrouzeix.FourierResolution.proj_proj line 46
  5. lemma OAI.CompleteCrouzeix.FourierResolution.orthogonal line 51
  6. lemma OAI.CompleteCrouzeix.FourierResolution.norm_decompose line 56
  7. def OAI.CompleteCrouzeix.FourierResolution.cauchy line 65
  8. def OAI.CompleteCrouzeix.FourierResolution.cauchyAdjoint line 68
  9. lemma OAI.CompleteCrouzeix.FourierResolution.adjoint_cauchy line 71
  10. lemma OAI.CompleteCrouzeix.FourierResolution.adjoint_markov_swap line 79
  11. lemma OAI.CompleteCrouzeix.FourierResolution.adjoint_apply line 85
  12. lemma OAI.CompleteCrouzeix.FourierResolution.adjoint_positive line 88
  13. lemma OAI.CompleteCrouzeix.FourierResolution.mean_adjoint line 93
  14. lemma OAI.CompleteCrouzeix.FourierResolution.negative_adjoint line 100
  15. theorem OAI.CompleteCrouzeix.FourierResolution.weighted_adjoint_bound line 107
  16. def OAI.CompleteCrouzeix.modeMask line 140
  17. lemma OAI.CompleteCrouzeix.modeMask_apply line 144
  18. lemma OAI.CompleteCrouzeix.modeMask_norm line 147
  19. def OAI.CompleteCrouzeix.modeMaskL line 154
  20. lemma OAI.CompleteCrouzeix.modeMaskL_apply line 161
  21. lemma OAI.CompleteCrouzeix.modeMaskL_adjoint line 164
  22. def OAI.CompleteCrouzeix.basisProjection line 175
  23. lemma OAI.CompleteCrouzeix.basisProjection_repr line 179
  24. lemma OAI.CompleteCrouzeix.basisProjection_inner line 186
  25. def OAI.CompleteCrouzeix.basisResolution line 196
  26. def OAI.CompleteCrouzeix.frequencyPart line 224
  27. abbrev OAI.CompleteCrouzeix.CircleL2 line 228
  28. def OAI.CompleteCrouzeix.scalarFourier line 230
  29. lemma OAI.CompleteCrouzeix.scalarFourier_coefficient line 233
  30. lemma OAI.CompleteCrouzeix.circle_fourier_ext line 245
  31. lemma OAI.CompleteCrouzeix.circle_fourier_star line 252
  32. lemma OAI.CompleteCrouzeix.integral_fourier_nonzero line 262
  33. lemma OAI.CompleteCrouzeix.scalarFourier_fourier line 267
  34. def OAI.CompleteCrouzeix.AnalyticBidiskKernel.scalarM line 291
  35. lemma OAI.CompleteCrouzeix.AnalyticBidiskKernel.kernel_complex line 293
  36. lemma OAI.CompleteCrouzeix.AnalyticBidiskKernel.scalarM_fourier_ae line 297
  37. lemma OAI.CompleteCrouzeix.AnalyticBidiskKernel.scalarM_fourier_positive_ae line 307
  38. lemma OAI.CompleteCrouzeix.AnalyticBidiskKernel.scalarM_fourier_positive_coefficient line 336
  39. lemma OAI.CompleteCrouzeix.AnalyticBidiskKernel.scalarM_star line 355
  40. lemma OAI.CompleteCrouzeix.AnalyticBidiskKernel.star_fourierLp line 371
  41. lemma OAI.CompleteCrouzeix.AnalyticBidiskKernel.scalarM_fourier_negative_coefficient line 378
  42. lemma OAI.CompleteCrouzeix.AnalyticBidiskKernel.scalarM_fourier_zero line 385
  43. lemma OAI.CompleteCrouzeix.AnalyticBidiskKernel.scalarM_fourier_swap line 395
  44. lemma OAI.CompleteCrouzeix.AnalyticBidiskKernel.scalarM_swap line 431