OAI/Analysis/NumericalRange/MarkovOperator.lean

GitHub source file

46 declarations, 0 contain sorry, 0 declared as axioms

  1. lemma OAI.CompleteCrouzeix.weighted_norm_integral_sq_le line 26
  2. structure OAI.CompleteCrouzeix.MarkovKernel line 53
  3. lemma OAI.CompleteCrouzeix.MarkovKernel.row_measurable line 65
  4. lemma OAI.CompleteCrouzeix.MarkovKernel.row_integrable line 71
  5. lemma OAI.CompleteCrouzeix.MarkovKernel.integrable_row_smul line 76
  6. lemma OAI.CompleteCrouzeix.MarkovKernel.integrable_sq_norm line 85
  7. lemma OAI.CompleteCrouzeix.MarkovKernel.integrable_row_sq line 91
  8. lemma OAI.CompleteCrouzeix.MarkovKernel.integrable_prod_smul line 97
  9. lemma OAI.CompleteCrouzeix.MarkovKernel.integrable_prod_sq line 106
  10. def OAI.CompleteCrouzeix.MarkovKernel.applyFun line 112
  11. lemma OAI.CompleteCrouzeix.MarkovKernel.applyFun_aestronglyMeasurable line 114
  12. lemma OAI.CompleteCrouzeix.MarkovKernel.applyFun_sq_le line 118
  13. lemma OAI.CompleteCrouzeix.MarkovKernel.applyFun_memLp line 124
  14. def OAI.CompleteCrouzeix.MarkovKernel.applyLp line 132
  15. lemma OAI.CompleteCrouzeix.MarkovKernel.applyLp_ae line 135
  16. lemma OAI.CompleteCrouzeix.MarkovKernel.l2_norm_sq line 138
  17. lemma OAI.CompleteCrouzeix.MarkovKernel.applyLp_norm_sq_le line 146
  18. lemma OAI.CompleteCrouzeix.MarkovKernel.applyLp_norm_le line 164
  19. lemma OAI.CompleteCrouzeix.MarkovKernel.applyFun_add line 168
  20. lemma OAI.CompleteCrouzeix.MarkovKernel.applyFun_smul line 179
  21. lemma OAI.CompleteCrouzeix.MarkovKernel.applyLp_add line 193
  22. lemma OAI.CompleteCrouzeix.MarkovKernel.applyLp_smul line 201
  23. def OAI.CompleteCrouzeix.MarkovKernel.toCLM line 209
  24. lemma OAI.CompleteCrouzeix.MarkovKernel.toCLM_apply line 216
  25. lemma OAI.CompleteCrouzeix.MarkovKernel.toCLM_norm_le line 218
  26. lemma OAI.CompleteCrouzeix.MarkovKernel.applyFun_integral line 222
  27. lemma OAI.CompleteCrouzeix.MarkovKernel.toCLM_integral line 230
  28. lemma OAI.CompleteCrouzeix.MarkovKernel.applyFun_const line 236
  29. lemma OAI.CompleteCrouzeix.MarkovKernel.toCLM_const line 245
  30. lemma OAI.CompleteCrouzeix.MarkovKernel.toCLM_compLpL_real line 251
  31. structure OAI.CompleteCrouzeix.AnalyticBidiskKernel line 273
  32. def OAI.CompleteCrouzeix.AnalyticBidiskKernel.circleB line 286
  33. def OAI.CompleteCrouzeix.AnalyticBidiskKernel.kernel line 288
  34. lemma OAI.CompleteCrouzeix.AnalyticBidiskKernel.norm_inv_circle line 290
  35. lemma OAI.CompleteCrouzeix.AnalyticBidiskKernel.inv_circle_mem line 293
  36. lemma OAI.CompleteCrouzeix.AnalyticBidiskKernel.continuous_circleB line 296
  37. lemma OAI.CompleteCrouzeix.AnalyticBidiskKernel.continuous_kernel line 303
  38. lemma OAI.CompleteCrouzeix.AnalyticBidiskKernel.circleB_row_integral line 306
  39. lemma OAI.CompleteCrouzeix.AnalyticBidiskKernel.circleB_column_integral line 311
  40. lemma OAI.CompleteCrouzeix.AnalyticBidiskKernel.kernel_row_integral line 316
  41. lemma OAI.CompleteCrouzeix.AnalyticBidiskKernel.kernel_column_integral line 330
  42. def OAI.CompleteCrouzeix.AnalyticBidiskKernel.toMarkovKernel line 344
  43. lemma OAI.CompleteCrouzeix.AnalyticBidiskKernel.circleB_right_nonpos_fourier line 354
  44. lemma OAI.CompleteCrouzeix.AnalyticBidiskKernel.circleB_left_nonpos_fourier line 368
  45. lemma OAI.CompleteCrouzeix.AnalyticBidiskKernel.conj_circleB_right_nonneg_fourier line 382
  46. lemma OAI.CompleteCrouzeix.AnalyticBidiskKernel.conj_circleB_left_nonneg_fourier line 388