OAI/Analysis/Crouzeix/BoundaryForms.lean

GitHub source file

77 declarations, 0 contain sorry, 0 declared as axioms

Boundary Forms.

  1. abbrev OAI.CrouzeixHilbert.Boundary.HS line 15
  2. def OAI.CrouzeixHilbert.Boundary.toHS line 17
  3. def OAI.CrouzeixHilbert.Boundary.ofHS line 20
  4. theorem OAI.CrouzeixHilbert.Boundary.ofHS_toHS line 23
  5. theorem OAI.CrouzeixHilbert.Boundary.toHS_ofHS line 26
  6. theorem OAI.CrouzeixHilbert.Boundary.norm_toHS_sq line 30
  7. theorem OAI.CrouzeixHilbert.Boundary.trace_conjTranspose_mul_re line 35
  8. theorem OAI.CrouzeixHilbert.Boundary.trace_mul_nonneg line 48
  9. theorem OAI.CrouzeixHilbert.Boundary.trace_fromBlocks line 57
  10. theorem OAI.CrouzeixHilbert.Boundary.block_posSemidef_norm_sq line 62
  11. theorem OAI.CrouzeixHilbert.Boundary.lp_norm_sq_eq_integral line 86
  12. theorem OAI.CrouzeixHilbert.Boundary.lp_block_posSemidef_norm_sq line 92
  13. structure OAI.CrouzeixHilbert.Boundary.ThreeWaySplitting line 108
  14. theorem OAI.CrouzeixHilbert.Boundary.ThreeWaySplitting.proj_proj line 119
  15. theorem OAI.CrouzeixHilbert.Boundary.ThreeWaySplitting.proj_orthogonal line 127
  16. theorem OAI.CrouzeixHilbert.Boundary.ThreeWaySplitting.total_apply line 132
  17. theorem OAI.CrouzeixHilbert.Boundary.ThreeWaySplitting.norm_sq_decomposition line 136
  18. theorem OAI.CrouzeixHilbert.Boundary.ThreeWaySplitting.norm_proj_le line 147
  19. def OAI.CrouzeixHilbert.Boundary.ThreeWaySplitting.cauchyAdjoint line 165
  20. theorem OAI.CrouzeixHilbert.Boundary.ThreeWaySplitting.cauchyAdjoint_apply line 168
  21. theorem OAI.CrouzeixHilbert.Boundary.ThreeWaySplitting.range_support line 173
  22. theorem OAI.CrouzeixHilbert.Boundary.ThreeWaySplitting.proj0_cauchyAdjoint line 185
  23. theorem OAI.CrouzeixHilbert.Boundary.ThreeWaySplitting.proj1_cauchyAdjoint line 189
  24. theorem OAI.CrouzeixHilbert.Boundary.ThreeWaySplitting.proj2_cauchyAdjoint line 193
  25. theorem OAI.CrouzeixHilbert.Boundary.ThreeWaySplitting.norm_cauchyAdjoint_sq line 197
  26. theorem OAI.CrouzeixHilbert.Boundary.ThreeWaySplitting.norm_apply_le_of_norm_le_one line 205
  27. theorem OAI.CrouzeixHilbert.Boundary.ThreeWaySplitting.weighted_norm_sq line 212
  28. structure OAI.CrouzeixHilbert.Boundary.ThreeWaySplitting.CompatibleInvolution line 223
  29. theorem OAI.CrouzeixHilbert.Boundary.ThreeWaySplitting.CompatibleInvolution.op_op line 233
  30. theorem OAI.CrouzeixHilbert.Boundary.ThreeWaySplitting.CompatibleInvolution.proj_neg line 235
  31. theorem OAI.CrouzeixHilbert.Boundary.ThreeWaySplitting.CompatibleInvolution.norm_add_op_sq line 239
  32. theorem OAI.CrouzeixHilbert.Boundary.ThreeWaySplitting.CompatibleInvolution.cauchyAdjoint_add_op_sq line 261
  33. theorem OAI.CrouzeixHilbert.Boundary.ThreeWaySplitting.CompatibleInvolution.adjoint_reflected_orthogonal line 268
  34. theorem OAI.CrouzeixHilbert.Boundary.ThreeWaySplitting.CompatibleInvolution.norm_cross_ge line 291
  35. theorem OAI.CrouzeixHilbert.Boundary.ThreeWaySplitting.ordered_projection line 302
  36. theorem OAI.CrouzeixHilbert.Boundary.ThreeWaySplitting.norm_adjoint_apply_le_of_norm_le_one line 312
  37. theorem OAI.CrouzeixHilbert.Boundary.ThreeWaySplitting.diagonal_estimate line 316
  38. theorem OAI.CrouzeixHilbert.Boundary.ThreeWaySplitting.ordered_comparison_of_block_norm line 335
  39. def OAI.CrouzeixHilbert.Boundary.fieldAction line 378
  40. theorem OAI.CrouzeixHilbert.Boundary.fieldAction_apply_ae line 411
  41. theorem OAI.CrouzeixHilbert.Boundary.norm_fieldAction_le line 419
  42. theorem OAI.CrouzeixHilbert.Boundary.adjoint_fieldAction line 429
  43. def OAI.CrouzeixHilbert.Boundary.hsEquiv line 447
  44. theorem OAI.CrouzeixHilbert.Boundary.hsEquiv_apply line 455
  45. theorem OAI.CrouzeixHilbert.Boundary.hsEquiv_symm_apply line 458
  46. theorem OAI.CrouzeixHilbert.Boundary.inner_toHS line 461
  47. theorem OAI.CrouzeixHilbert.Boundary.real_inner_toHS line 473
  48. theorem OAI.CrouzeixHilbert.Boundary.norm_toHS_conjTranspose line 479
  49. theorem OAI.CrouzeixHilbert.Boundary.norm_toHS_mul_le line 486
  50. theorem OAI.CrouzeixHilbert.Boundary.norm_toHS_mul_le_right line 504
  51. def OAI.CrouzeixHilbert.Boundary.hsLeft line 513
  52. def OAI.CrouzeixHilbert.Boundary.hsRight line 517
  53. theorem OAI.CrouzeixHilbert.Boundary.hsLeft_apply line 521
  54. theorem OAI.CrouzeixHilbert.Boundary.hsRight_apply line 524
  55. theorem OAI.CrouzeixHilbert.Boundary.norm_hsLeft_le line 527
  56. theorem OAI.CrouzeixHilbert.Boundary.norm_hsRight_le line 533
  57. theorem OAI.CrouzeixHilbert.Boundary.adjoint_hsLeft line 539
  58. theorem OAI.CrouzeixHilbert.Boundary.adjoint_hsRight line 549
  59. def OAI.CrouzeixHilbert.Boundary.hsLeftCoefficient line 560
  60. def OAI.CrouzeixHilbert.Boundary.hsRightCoefficient line 577
  61. def OAI.CrouzeixHilbert.Boundary.hsStar line 594
  62. theorem OAI.CrouzeixHilbert.Boundary.hsStar_apply line 611
  63. theorem OAI.CrouzeixHilbert.Boundary.hsStar_hsStar line 613
  64. def OAI.CrouzeixHilbert.Boundary.lpStar line 621
  65. theorem OAI.CrouzeixHilbert.Boundary.lpStar_apply_ae line 643
  66. theorem OAI.CrouzeixHilbert.Boundary.lpStar_lpStar line 647
  67. def OAI.CrouzeixHilbert.Boundary.lpLeft line 652
  68. def OAI.CrouzeixHilbert.Boundary.lpRight line 658
  69. theorem OAI.CrouzeixHilbert.Boundary.lpLeft_apply_ae line 664
  70. theorem OAI.CrouzeixHilbert.Boundary.lpRight_apply_ae line 670
  71. theorem OAI.CrouzeixHilbert.Boundary.norm_lpLeft_le line 676
  72. theorem OAI.CrouzeixHilbert.Boundary.norm_lpRight_le line 680
  73. theorem OAI.CrouzeixHilbert.Boundary.aestronglyMeasurable_conjTranspose line 684
  74. theorem OAI.CrouzeixHilbert.Boundary.lpLeft_adjoint_apply_ae line 688
  75. theorem OAI.CrouzeixHilbert.Boundary.lpRight_adjoint_apply_ae line 701
  76. theorem OAI.CrouzeixHilbert.Boundary.lpStar_eq_self_iff line 714
  77. theorem OAI.CrouzeixHilbert.Boundary.lp_ordered_comparison line 727