OAI/Analysis/RotationWeights/Fibers.lean

GitHub source file

20 declarations, 0 contain sorry, 0 declared as axioms

  1. abbrev OAI.ContinuousCircleWeight.FiberHilbert line 12
  2. abbrev OAI.ContinuousCircleWeight.FiberOperator line 13
  3. def OAI.ContinuousCircleWeight.lpDiagonal line 15
  4. theorem OAI.ContinuousCircleWeight.lpDiagonal_apply line 39
  5. def OAI.ContinuousCircleWeight.fiberShift line 43
  6. theorem OAI.ContinuousCircleWeight.fiberShift_apply line 46
  7. theorem OAI.ContinuousCircleWeight.fiberShift_add line 51
  8. def OAI.ContinuousCircleWeight.fiberWeightedShift line 58
  9. theorem OAI.ContinuousCircleWeight.fiberWeightedShift_apply line 61
  10. def OAI.ContinuousCircleWeight.fiberCocycleShift line 68
  11. theorem OAI.ContinuousCircleWeight.fiberCocycleShift_apply line 75
  12. theorem OAI.ContinuousCircleWeight.fiberCocycleShift_pow_apply line 80
  13. theorem OAI.ContinuousCircleWeight.invariant_fixed_vector line 95
  14. theorem OAI.ContinuousCircleWeight.invariant_fixed_vector_pow line 104
  15. theorem OAI.ContinuousCircleWeight.projection_complement_inner line 113
  16. def OAI.ContinuousCircleWeight.cocycleRatioDiagonal line 120
  17. theorem OAI.ContinuousCircleWeight.cocycleRatioDiagonal_apply line 127
  18. theorem OAI.ContinuousCircleWeight.cocycle_action_coordinate line 131
  19. theorem OAI.ContinuousCircleWeight.fiber_full_convolution line 143
  20. theorem OAI.ContinuousCircleWeight.cocycle_two_ratio_bounds line 173