OAI/Analysis/IntegralMeans/Eigenmeasure.lean

GitHub source file

28 declarations, 0 contain sorry, 0 declared as axioms

  1. lemma OAI.Brennan.positive_operator_mono line 25
  2. lemma OAI.Brennan.positive_operator_abs_bound line 31
  3. lemma OAI.Brennan.positive_operator_norm line 45
  4. lemma OAI.Brennan.positive_operator_pow line 60
  5. lemma OAI.Brennan.log_norm_pow_subadditive line 69
  6. lemma OAI.Brennan.log_norm_pow_bddBelow line 79
  7. def OAI.Brennan.growthLog line 85
  8. def OAI.Brennan.growthRate line 88
  9. lemma OAI.Brennan.tendsto_log_norm_pow line 91
  10. lemma OAI.Brennan.growthLog_nonneg line 96
  11. lemma OAI.Brennan.growthRate_ge_one line 101
  12. lemma OAI.Brennan.norm_pow_eventually_le line 105
  13. lemma OAI.Brennan.summable_scaled_pow line 121
  14. lemma OAI.Brennan.growthRate_le_of_pow_bound line 137
  15. def OAI.Brennan.positiveResolvent line 159
  16. lemma OAI.Brennan.positiveResolvent_apply line 163
  17. lemma OAI.Brennan.summable_resolvent_eval line 169
  18. lemma OAI.Brennan.positiveResolvent_eval line 179
  19. lemma OAI.Brennan.positiveResolvent_nonneg line 187
  20. lemma OAI.Brennan.positiveResolvent_ge_one line 198
  21. lemma OAI.Brennan.positiveResolvent_mul line 210
  22. lemma OAI.Brennan.positive_operator_pow_bound line 247
  23. lemma OAI.Brennan.positiveResolvent_norm_bound line 275
  24. lemma OAI.Brennan.probability_of_positive_functional line 310
  25. lemma OAI.Brennan.exists_max_of_nonneg_continuous line 331
  26. lemma OAI.Brennan.exists_resolvent_probability line 341
  27. lemma OAI.Brennan.exists_growth_eigenmeasure line 378
  28. lemma OAI.Brennan.positive_functional_bound line 406