OAI/Analysis/BackwardIntertwiners/GlobalOperators.lean

GitHub source file

62 declarations, 0 contain sorry, 0 declared as axioms

  1. lemma OAI.BackwardIntertwiners.weightedPermutation_stronglyMeasurable line 16
  2. lemma OAI.BackwardIntertwiners.weightedPermutation_aestronglyMeasurable line 25
  3. def OAI.BackwardIntertwiners.scalarMultiplier line 35
  4. def OAI.BackwardIntertwiners.fieldVector line 42
  5. lemma OAI.BackwardIntertwiners.fieldVector_ae line 50
  6. lemma OAI.BackwardIntertwiners.fieldVector_norm line 56
  7. def OAI.BackwardIntertwiners.fieldOperator line 68
  8. lemma OAI.BackwardIntertwiners.fieldOperator_ae line 89
  9. lemma OAI.BackwardIntertwiners.fieldOperator_norm line 95
  10. lemma OAI.BackwardIntertwiners.scalarMultiplier_ae line 101
  11. lemma OAI.BackwardIntertwiners.scalarMultiplier_norm_le line 103
  12. abbrev OAI.BackwardIntertwiners.GlobalHilbert line 107
  13. def OAI.BackwardIntertwiners.OperatorInvariant line 109
  14. def OAI.BackwardIntertwiners.generatedAlgebra line 112
  15. def OAI.BackwardIntertwiners.AlgebraTransitive line 116
  16. structure OAI.BackwardIntertwiners.DirectModelData line 121
  17. structure OAI.BackwardIntertwiners.DirectModelProperties line 131
  18. def OAI.BackwardIntertwiners.forwardFiber line 157
  19. def OAI.BackwardIntertwiners.backwardFiber line 161
  20. lemma OAI.BackwardIntertwiners.forwardFiber_apply line 164
  21. lemma OAI.BackwardIntertwiners.backwardFiber_apply line 166
  22. lemma OAI.BackwardIntertwiners.forwardFiber_norm_le line 168
  23. lemma OAI.BackwardIntertwiners.backwardFiber_norm_le line 170
  24. lemma OAI.BackwardIntertwiners.forwardFiber_single line 172
  25. lemma OAI.BackwardIntertwiners.backwardFiber_single line 181
  26. lemma OAI.BackwardIntertwiners.forwardFiber_norm line 190
  27. lemma OAI.BackwardIntertwiners.backwardFiber_intertwines line 198
  28. lemma OAI.BackwardIntertwiners.coordinateTail_isClosed line 207
  29. lemma OAI.BackwardIntertwiners.forwardFiber_tail line 215
  30. lemma OAI.BackwardIntertwiners.backwardFiber_tail line 219
  31. lemma OAI.BackwardIntertwiners.single_mem_coordinateTail line 223
  32. lemma OAI.BackwardIntertwiners.backwardFiber_tail_closure line 228
  33. lemma OAI.BackwardIntertwiners.backwardFiber_denseRange line 252
  34. lemma OAI.BackwardIntertwiners.explicitExponent_distance line 266
  35. lemma OAI.BackwardIntertwiners.interval_exponent_lower line 284
  36. lemma OAI.BackwardIntertwiners.forwardFiber_power_input line 293
  37. lemma OAI.BackwardIntertwiners.forwardFiber_power_norm line 307
  38. lemma OAI.BackwardIntertwiners.forwardFiber_aestronglyMeasurable line 328
  39. lemma OAI.BackwardIntertwiners.backwardFiber_aestronglyMeasurable line 333
  40. def OAI.BackwardIntertwiners.forwardOperator line 339
  41. lemma OAI.BackwardIntertwiners.forwardOperator_ae line 342
  42. lemma OAI.BackwardIntertwiners.forwardOperator_norm_le line 345
  43. def OAI.BackwardIntertwiners.inverseOdometer line 348
  44. lemma OAI.BackwardIntertwiners.inverseOdometer_odometer line 349
  45. lemma OAI.BackwardIntertwiners.odometer_inverseOdometer line 352
  46. lemma OAI.BackwardIntertwiners.inverseOdometer_preserving line 355
  47. def OAI.BackwardIntertwiners.odometerMeasurableEquiv line 363
  48. def OAI.BackwardIntertwiners.backwardFieldOperator line 371
  49. def OAI.BackwardIntertwiners.backwardOperator line 374
  50. lemma OAI.BackwardIntertwiners.backwardOperator_ae_inverse line 377
  51. lemma OAI.BackwardIntertwiners.backwardOperator_ae line 384
  52. lemma OAI.BackwardIntertwiners.backwardOperator_norm line 390
  53. lemma OAI.BackwardIntertwiners.forward_backward_commute line 397
  54. lemma OAI.BackwardIntertwiners.forward_scalar_commute line 411
  55. def OAI.BackwardIntertwiners.constantBasis line 420
  56. lemma OAI.BackwardIntertwiners.constantBasis_norm line 421
  57. lemma OAI.BackwardIntertwiners.constantBasis_ae line 424
  58. lemma OAI.BackwardIntertwiners.forwardOperator_constantBasis_zero line 426
  59. lemma OAI.BackwardIntertwiners.forwardOperator_norm line 434
  60. lemma OAI.BackwardIntertwiners.forwardOperator_ne_zero line 440
  61. lemma OAI.BackwardIntertwiners.forwardOperator_power_ae line 446
  62. lemma OAI.BackwardIntertwiners.forwardOperator_power_norm line 454