OAI/Analysis/FiniteFactor/Fiber/Shift.lean

GitHub source file

9 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.FiniteFactor.fiberShiftVector line 11

    Source documentation

    Coordinate translation on the original l2 fiber.

    def fiberShiftVector (n : ℤ) (v : SourceFiberHilbert) : SourceFiberHilbert :=
…

    Mentions: OAI.FiniteFactor.SourceFiberHilbert

  2. theorem OAI.FiniteFactor.fiberShiftVector_norm line 15
  3. def OAI.FiniteFactor.fiberShift line 26
  4. theorem OAI.FiniteFactor.fiberShift_apply line 35
  5. theorem OAI.FiniteFactor.fiberShift_single line 38
  6. theorem OAI.FiniteFactor.fiberShift_mul line 50
  7. theorem OAI.FiniteFactor.fiberShift_zero line 58
  8. theorem OAI.FiniteFactor.fiber_covariance_operator line 66
  9. theorem OAI.FiniteFactor.invariant_projection_pow line 79

    Source documentation

    Invariance of a projection range persists under every nonnegative power.

    theorem invariant_projection_pow {R : Type*} [Ring R] (p T : R)
    (hp : p*p = p) (hinv : (1-p)*T*p = 0) : ∀ n : ℕ, (1-p)*(T^n)*p = 0 := by
…