OAI/Analysis/Crouzeix/BoundaryOperators.lean

GitHub source file

29 declarations, 0 contain sorry, 0 declared as axioms

Boundary Operators.

  1. lemma OAI.CrouzeixHilbert.Boundary.norm_integral_weight_sq_le line 18
  2. abbrev OAI.CrouzeixHilbert.Boundary.CircleKernel line 41
  3. def OAI.CrouzeixHilbert.Boundary.kernelApply line 43
  4. lemma OAI.CrouzeixHilbert.Boundary.boundaryLp_integrable line 46
  5. lemma OAI.CrouzeixHilbert.Boundary.kernel_integrable line 49
  6. lemma OAI.CrouzeixHilbert.Boundary.kernel_sq_integrable line 57
  7. lemma OAI.CrouzeixHilbert.Boundary.continuous_kernelApply line 64
  8. def OAI.CrouzeixHilbert.Boundary.kernelLp line 77
  9. lemma OAI.CrouzeixHilbert.Boundary.kernelLp_apply_ae line 80
  10. lemma OAI.CrouzeixHilbert.Boundary.norm_kernelApply_sq_le line 83
  11. lemma OAI.CrouzeixHilbert.Boundary.kernel_sq_integrable_prod line 95
  12. lemma OAI.CrouzeixHilbert.Boundary.norm_kernelLp_le line 101
  13. lemma OAI.CrouzeixHilbert.Boundary.kernelLp_add line 123
  14. lemma OAI.CrouzeixHilbert.Boundary.kernelLp_smul line 137
  15. def OAI.CrouzeixHilbert.Boundary.kernelOperator line 153
  16. lemma OAI.CrouzeixHilbert.Boundary.norm_kernelOperator_le line 164
  17. def OAI.CrouzeixHilbert.Boundary.transposeKernel line 173
  18. lemma OAI.CrouzeixHilbert.Boundary.transposeKernel_apply line 176
  19. lemma OAI.CrouzeixHilbert.Boundary.transposeKernel_transposeKernel line 179
  20. lemma OAI.CrouzeixHilbert.Boundary.kernel_inner_integrable line 184
  21. lemma OAI.CrouzeixHilbert.Boundary.inner_kernelLp line 198
  22. lemma OAI.CrouzeixHilbert.Boundary.inner_kernelLp_swap line 216
  23. lemma OAI.CrouzeixHilbert.Boundary.adjoint_kernelOperator line 231
  24. lemma OAI.CrouzeixHilbert.Boundary.kernelLp_star line 242
  25. lemma OAI.CrouzeixHilbert.Boundary.kernel_integrable_prod line 258
  26. lemma OAI.CrouzeixHilbert.Boundary.integral_kernelLp line 266
  27. lemma OAI.CrouzeixHilbert.Boundary.matrixMean_eq_integral line 280
  28. lemma OAI.CrouzeixHilbert.Boundary.matrixMean_kernelLp line 286
  29. lemma OAI.CrouzeixHilbert.Boundary.kernelLp_const line 291