OAI/Analysis/SymmetricDomains/BoundaryInjective.lean

GitHub source file

123 declarations, 0 contain sorry, 0 declared as axioms

  1. abbrev OAI.Release061.Wiener.Poly line 13
  2. def OAI.Release061.Wiener.weight line 15
  3. lemma OAI.Release061.Wiener.weight_pos line 16
  4. lemma OAI.Release061.Wiener.one_le_weight line 17
  5. lemma OAI.Release061.Wiener.weight_add_le line 18
  6. def OAI.Release061.Wiener.wnorm line 25
  7. lemma OAI.Release061.Wiener.wnorm_eq_sum line 27
  8. lemma OAI.Release061.Wiener.wnorm_nonneg line 31
  9. lemma OAI.Release061.Wiener.wnorm_zero line 35
  10. lemma OAI.Release061.Wiener.wnorm_add_le line 37
  11. lemma OAI.Release061.Wiener.wnorm_neg line 53
  12. lemma OAI.Release061.Wiener.wnorm_eq_zero line 56
  13. lemma OAI.Release061.Wiener.wnorm_single line 67
  14. lemma OAI.Release061.Wiener.wnorm_sum_le line 72
  15. lemma OAI.Release061.Wiener.wnorm_mul_le line 81
  16. def OAI.Release061.Wiener.ringNorm line 101
  17. instance OAI.Release061.Wiener.(instance at line 109) line 109
  18. lemma OAI.Release061.Wiener.norm_def line 113
  19. lemma OAI.Release061.Wiener.wnorm_smul line 115
  20. instance OAI.Release061.Wiener.(instance at line 123) line 123
  21. instance OAI.Release061.Wiener.(instance at line 127) line 127
  22. abbrev OAI.Release061.Wiener.Space line 133
  23. example OAI.Release061.Wiener.(example at line 135) line 135
  24. example OAI.Release061.Wiener.(example at line 136) line 136
  25. example OAI.Release061.Wiener.(example at line 137) line 137
  26. def OAI.Release061.Wiener.modesLinear line 142
  27. lemma OAI.Release061.Wiener.modesLinear_apply line 145
  28. lemma OAI.Release061.Wiener.modesLinear_bound line 148
  29. def OAI.Release061.Wiener.modesCLM line 159
  30. def OAI.Release061.Wiener.fromModes line 163
  31. lemma OAI.Release061.Wiener.fromModes_coe line 166
  32. lemma OAI.Release061.Wiener.fromModes_bound line 171
  33. lemma OAI.Release061.Wiener.fromModes_single line 179
  34. instance OAI.Release061.Wiener.(instance at line 186) line 186
  35. abbrev OAI.Release061.Wiener.Circle line 188
  36. def OAI.Release061.Wiener.boundary line 190
  37. lemma OAI.Release061.Wiener.boundary_coe line 193
  38. lemma OAI.Release061.Wiener.boundary_single line 197
  39. lemma OAI.Release061.Wiener.boundary_norm_le line 201
  40. lemma OAI.Release061.Wiener.boundary_one line 204
  41. lemma OAI.Release061.Wiener.boundary_poly_mul line 210
  42. lemma OAI.Release061.Wiener.boundary_mul line 231
  43. def OAI.Release061.Wiener.boundaryAlgHom line 236
  44. lemma OAI.Release061.Wiener.poly_expansion line 245
  45. lemma OAI.Release061.Wiener.continuous_eq_of_single line 252
  46. def OAI.Release061.Wiener.conjPoly line 258
  47. lemma OAI.Release061.Wiener.conjPoly_coeff line 264
  48. lemma OAI.Release061.Wiener.conjPoly_single line 267
  49. lemma OAI.Release061.Wiener.conjPoly_norm line 273
  50. def OAI.Release061.Wiener.conjugate line 280
  51. lemma OAI.Release061.Wiener.conjugate_coe line 285
  52. lemma OAI.Release061.Wiener.conjugate_single line 289
  53. lemma OAI.Release061.Wiener.conjugate_norm line 294
  54. lemma OAI.Release061.Wiener.conjugate_involutive line 299
  55. lemma OAI.Release061.Wiener.boundary_conjugate line 307
  56. def OAI.Release061.Wiener.multiplier line 319
  57. lemma OAI.Release061.Wiener.multiplier_single line 326
  58. lemma OAI.Release061.Wiener.multiplier_bound line 338
  59. def OAI.Release061.Wiener.hilbertSymbol line 341
  60. lemma OAI.Release061.Wiener.hilbertSymbol_bound line 343
  61. lemma OAI.Release061.Wiener.hilbertSymbol_neg line 347
  62. def OAI.Release061.Wiener.hilbert line 352
  63. lemma OAI.Release061.Wiener.hilbert_norm line 354
  64. lemma OAI.Release061.Wiener.hilbert_conjugate line 357
  65. def OAI.Release061.Wiener.realSubspace line 367
  66. lemma OAI.Release061.Wiener.mem_realSubspace line 369
  67. lemma OAI.Release061.Wiener.realSubspace_closed line 372
  68. instance OAI.Release061.Wiener.(instance at line 376) line 376
  69. lemma OAI.Release061.Wiener.real_boundary line 378
  70. lemma OAI.Release061.Wiener.hilbert_real line 383
  71. abbrev OAI.Release061.Wiener.ClosedDisc line 386
  72. def OAI.Release061.Wiener.schwarzMode line 388
  73. lemma OAI.Release061.Wiener.schwarzMode_continuous line 391
  74. lemma OAI.Release061.Wiener.schwarzMode_differentiable line 395
  75. lemma OAI.Release061.Wiener.schwarzMode_bound line 399
  76. def OAI.Release061.Wiener.schwarzModeC line 408
  77. def OAI.Release061.Wiener.schwarz line 411
  78. lemma OAI.Release061.Wiener.schwarz_coe line 419
  79. lemma OAI.Release061.Wiener.schwarz_norm line 422
  80. lemma OAI.Release061.Wiener.schwarz_single line 424
  81. def OAI.Release061.Wiener.discValue line 428
  82. lemma OAI.Release061.Wiener.discValue_eq line 432
  83. lemma OAI.Release061.Wiener.discValue_continuousOn line 435
  84. lemma OAI.Release061.Wiener.exists_poly_seq line 441
  85. def OAI.Release061.Wiener.polyDisc line 446
  86. lemma OAI.Release061.Wiener.polyDisc_eq line 448
  87. lemma OAI.Release061.Wiener.polyDisc_differentiable line 454
  88. lemma OAI.Release061.Wiener.polyDisc_tendsto_uniformly line 460
  89. lemma OAI.Release061.Wiener.discValue_analytic line 471
  90. lemma OAI.Release061.Wiener.fourier_nat line 477
  91. lemma OAI.Release061.Wiener.schwarzMode_boundary line 482
  92. lemma OAI.Release061.Wiener.schwarz_boundary line 496
  93. lemma OAI.Release061.Wiener.discValue_at_one line 515
  94. lemma OAI.Release061.Wiener.schwarz_has_real_part line 519
  95. lemma OAI.Release061.Wiener.schwarz_has_imag_part line 524
  96. lemma OAI.Release061.Wiener.single_mul line 530
  97. lemma OAI.Release061.Wiener.conjugate_mul line 536
  98. lemma OAI.Release061.Wiener.conjugate_one line 548
  99. lemma OAI.Release061.Wiener.conjugate_real line 554
  100. def OAI.Release061.Wiener.realAlgebra line 557
  101. lemma OAI.Release061.Wiener.realAlgebra_closed line 565
  102. instance OAI.Release061.Wiener.(instance at line 569) line 569
  103. instance OAI.Release061.Wiener.(instance at line 571) line 571
  104. instance OAI.Release061.Wiener.(instance at line 576) line 576
  105. lemma OAI.Release061.Wiener.realAlgebra_mem_subspace line 579
  106. lemma OAI.Release061.Wiener.realAlgebra_boundary_im line 582
  107. def OAI.Release061.Wiener.realEvaluation line 585
  108. lemma OAI.Release061.Wiener.realEvaluation_bound line 601
  109. def OAI.Release061.Wiener.realEvaluationCLM line 605
  110. def OAI.Release061.Wiener.realHilbert line 611
  111. def OAI.Release061.Wiener.constantReal line 622
  112. def OAI.Release061.Wiener.normalizedHilbert line 627
  113. lemma OAI.Release061.Wiener.normalizedHilbert_bound line 630
  114. lemma OAI.Release061.Wiener.normalizedHilbert_eval_zero line 640
  115. def OAI.Release061.Wiener.fourierCLM line 648
  116. def OAI.Release061.Wiener.coeff line 662
  117. lemma OAI.Release061.Wiener.coeff_single line 664
  118. lemma OAI.Release061.Wiener.coeff_coe line 673
  119. def OAI.Release061.Wiener.cutoff line 679
  120. lemma OAI.Release061.Wiener.cutoff_bound line 687
  121. lemma OAI.Release061.Wiener.cutoff_eq line 690
  122. lemma OAI.Release061.Wiener.cutoff_coe_self line 711
  123. lemma OAI.Release061.Wiener.boundary_injective line 720