OAI/Analysis/KadisonKastler/RemoteSiteDoubling.lean

GitHub source file

6 declarations, 0 contain sorry, 0 declared as axioms

Interleaving two site families beyond a finite prefix

  1. def OAI.KadisonKastler.remoteNatDoubling line 12

    Source documentation

    The left copy starts beyond the prefix, which belongs to the right copy.

    def remoteNatDoubling (n : ℕ) : (ℕ ⊕ ℕ) ≃ ℕ :=
…
  2. theorem OAI.KadisonKastler.remoteNatDoubling_left line 19
  3. theorem OAI.KadisonKastler.remoteNatDoubling_right_prefix line 22
  4. def OAI.KadisonKastler.remoteTwoRatioDoubling line 30
  5. theorem OAI.KadisonKastler.remoteTwoRatioDoubling_parameter line 34
  6. theorem OAI.KadisonKastler.remoteTwoRatioDoubling_prefix line 39