MeasurableNatEnumeration.lean`

14 declarations, 0 contain sorry, 0 declared as axioms

Measurably enumerating nonzero frame indices

The nth index of a point-dependent subset of the naturals is measurable when each membership predicate is measurable. The library's value zero outside the finite range is retained; dimension strata remove that case.

def OAI.KadisonKastler.measurableIndexCount line 21
theorem OAI.KadisonKastler.measurable_indexCount line 25
theorem OAI.KadisonKastler.nth_eq_nonzero_iff line 36
theorem OAI.KadisonKastler.measurable_natNth line 50
def OAI.KadisonKastler.frameIndexAvailable line 77
Source documentation
There are at least k + 1 indices satisfying the predicate.
```
def frameIndexAvailable (p : ℕ → Prop) (k : ℕ) : Prop :=
…
```
theorem OAI.KadisonKastler.frameIndexAvailable_mono line 80
theorem OAI.KadisonKastler.measurableSet_frameIndexAvailable line 85
theorem OAI.KadisonKastler.frameIndexAvailable_valid line 97
theorem OAI.KadisonKastler.frameIndexAvailable_count line 106
def OAI.KadisonKastler.frameIndexEquiv line 114
Source documentation
The ascending enumeration, restricted to its genuine indices, is a bijection.
```
def frameIndexEquiv (p : ℕ → Prop) : {k // frameIndexAvailable p k} ≃ {m // p m} := by
…
```
Mentions: OAI.KadisonKastler.frameIndexAvailable

def OAI.KadisonKastler.frameDimensionStratum line 123

Source documentation

Index zero is the infinite-rank stratum; index n + 1 is rank n.

def frameDimensionStratum (p : X → ℕ → Prop) : ℕ → Set X
  | 0 => {x | ∀ k, frameIndexAvailable (p x) k}
  | n + 1 => {x | (∀ k < n, frameIndexAvailable (p x) k) ∧
      ¬frameIndexAvailable (p x) n}

Mentions: OAI.KadisonKastler.frameIndexAvailable

theorem OAI.KadisonKastler.measurableSet_frameDimensionStratum line 128
theorem OAI.KadisonKastler.exists_frameDimensionStratum line 144
theorem OAI.KadisonKastler.frameDimensionStratum_finite_iff line 154