OAI/Analysis/StrictMeans/TransferOperator.lean

GitHub source file

31 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.StrictInverseFirstPower.affineDiskFunction line 33
  2. lemma OAI.StrictInverseFirstPower.affineDiskFunction_differentiableOn line 35
  3. lemma OAI.StrictInverseFirstPower.affineDiskFunction_injOn line 40
  4. lemma OAI.StrictInverseFirstPower.affineDiskFunction_hasDerivAt_zero line 46
  5. def OAI.StrictInverseFirstPower.affineDiskMap line 51
  6. lemma OAI.StrictInverseFirstPower.affineDiskMap_extension line 56
  7. lemma OAI.StrictInverseFirstPower.affineDiskMap_normalized line 60
  8. def OAI.StrictInverseFirstPower.affineFamily line 71
  9. instance OAI.StrictInverseFirstPower.(instance at line 73) line 73
  10. lemma OAI.StrictInverseFirstPower.halfPlaneFunction_affineFamily line 75
  11. lemma OAI.StrictInverseFirstPower.halfPlaneFunction_affineFamily_deriv line 87
  12. lemma OAI.StrictInverseFirstPower.halfPlaneQ_affineFamily line 94
  13. lemma OAI.StrictInverseFirstPower.rebase_affineFamily line 97
  14. def OAI.StrictInverseFirstPower.rebaseUncurried line 109
  15. def OAI.StrictInverseFirstPower.rebaseMap line 112
  16. def OAI.StrictInverseFirstPower.weightMap line 115
  17. def OAI.StrictInverseFirstPower.affineOperator line 119
  18. lemma OAI.StrictInverseFirstPower.affineOperator_apply line 123
  19. lemma OAI.StrictInverseFirstPower.affineOperator_monotone line 126
  20. lemma OAI.StrictInverseFirstPower.affineOperator_mul line 131
  21. lemma OAI.StrictInverseFirstPower.affineOperator_one line 138
  22. lemma OAI.StrictInverseFirstPower.affineOperator_affineFamily line 142
  23. lemma OAI.StrictInverseFirstPower.continuous_affineOperator_apply line 145
  24. lemma OAI.StrictInverseFirstPower.continuous_affineOperator_strong line 150
  25. def OAI.StrictInverseFirstPower.dyadicLeft line 154
  26. def OAI.StrictInverseFirstPower.dyadicRight line 155
  27. def OAI.StrictInverseFirstPower.dyadicOperator line 157
  28. lemma OAI.StrictInverseFirstPower.dyadicOperator_monotone line 160
  29. lemma OAI.StrictInverseFirstPower.dyadicOperator_affineFamily line 167
  30. lemma OAI.StrictInverseFirstPower.dyadicOperator_pow_affineFamily line 174
  31. lemma OAI.StrictInverseFirstPower.dyadicOperator_pow_norm_ge_one line 181