DirectionTuples.lean`

8 declarations, 0 contain sorry, 0 declared as axioms

Supports and events for direction tuples

Tuples are arbitrary functions from Fin h; repeated indices are allowed. The support records distinct indices, so its cardinality can be smaller than h.

def OAI.MetricEntropyDuality.tupleSupport line 22
Source documentation
The set of indices appearing in an ordered tuple, including repeated-index tuples.
```
noncomputable def tupleSupport (a : Fin h → U) : Finset U := by
…
```
theorem OAI.MetricEntropyDuality.mem_tupleSupport line 26
theorem OAI.MetricEntropyDuality.tupleSupport_card_le line 31
theorem OAI.MetricEntropyDuality.tupleSupport_nonempty line 36
theorem OAI.MetricEntropyDuality.tupleSupport_subset_iff line 40
def OAI.MetricEntropyDuality.DisjointSupports line 50
Source documentation
Different tuples in the list use disjoint sets of indices.
```
def DisjointSupports (L : Fin w → Fin h → U) : Prop :=
…
```

def OAI.MetricEntropyDuality.tupleEvent line 54

Source documentation

Samples for which the specified tuple of sampled values satisfies bad.

noncomputable def tupleEvent [Fintype U] [Fintype E]
    (bad : (Fin h → E) → Prop) (a : Fin h → U) : Finset (U → E) := by
…

theorem OAI.MetricEntropyDuality.mem_tupleEvent line 59