OAI/Analysis/IntegralMeans/TransferOperator.lean

GitHub source file

35 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.Brennan.halfMul line 24
  2. def OAI.Brennan.halfPoint line 26
  3. def OAI.Brennan.horizontal line 29
  4. lemma OAI.Brennan.halfPoint_mul line 31
  5. lemma OAI.Brennan.halfMul_assoc line 36
  6. lemma OAI.Brennan.halfOne_mul line 39
  7. lemma OAI.Brennan.halfMul_one line 41
  8. lemma OAI.Brennan.continuous_halfPoint line 43
  9. lemma OAI.Brennan.rerootClass_one line 48
  10. lemma OAI.Brennan.classWeight_one line 54
  11. def OAI.Brennan.weightAt line 59
  12. def OAI.Brennan.actionAt line 64
  13. def OAI.Brennan.affineOperator line 69
  14. lemma OAI.Brennan.affineOperator_apply line 72
  15. lemma OAI.Brennan.affineOperator_pos line 75
  16. lemma OAI.Brennan.affineOperator_mul line 78
  17. lemma OAI.Brennan.affineOperator_one line 85
  18. lemma OAI.Brennan.continuous_affineOperator_apply line 90
  19. lemma OAI.Brennan.affineOperator_norm_le line 99
  20. lemma OAI.Brennan.classFun_identityClass line 108
  21. lemma OAI.Brennan.classWeight_identityClass line 111
  22. lemma OAI.Brennan.reroot_identityClass line 116
  23. def OAI.Brennan.dyadicLeft line 127
  24. def OAI.Brennan.dyadicRight line 129
  25. def OAI.Brennan.transferOperator line 131
  26. lemma OAI.Brennan.transferOperator_pos line 134
  27. lemma OAI.Brennan.transferOperator_identityClass line 139
  28. lemma OAI.Brennan.transferOperator_pow_identityClass line 144
  29. lemma OAI.Brennan.transferOperator_pow_norm_ge_one line 149
  30. lemma OAI.Brennan.diskCayley_norm_sq_identity line 154
  31. lemma OAI.Brennan.classFun_deriv_norm line 163
  32. lemma OAI.Brennan.classFun_reciprocal_norm line 170
  33. lemma OAI.Brennan.classFun_reciprocal_bound line 175
  34. lemma OAI.Brennan.classFun_strip_bound line 204
  35. lemma OAI.Brennan.classFun_strip_bound_two line 220