OccurrenceCounts.lean`

GitHub source file

9 declarations, 0 contain sorry, 0 declared as axioms

Counts of the actual slots belonging to each prime label.

def OAI.TwoPointCorrelations.labelOccurrences line 13
def OAI.TwoPointCorrelations.litOccurrences line 16
def OAI.TwoPointCorrelations.unlitOccurrences line 19
lemma OAI.TwoPointCorrelations.lit_unlit_count line 23
lemma OAI.TwoPointCorrelations.total_label_occurrences line 33
def OAI.TwoPointCorrelations.singletonLabels line 38
def OAI.TwoPointCorrelations.nonsingletonLabels line 41
lemma OAI.TwoPointCorrelations.twice_labels_le_slots_add_singletons line 46
Source documentation
The number of labels is at most half the slot count plus half the singleton count. All labels here are observed in the word.
```
lemma twice_labels_le_slots_add_singletons (label : τ → ι)
    (hused : ∀ i, 0 < (labelOccurrences label i).card) :
    2 * Fintype.card ι ≤ Fintype.card τ + (singletonLabels label).card := by
…
```
Mentions: OAI.TwoPointCorrelations.labelOccurrences, OAI.TwoPointCorrelations.singletonLabels
lemma OAI.TwoPointCorrelations.actual_unlit_le_twice_extra line 62
Source documentation
The extra-exponent bound applies to the literal occurrence counts of every nonsingleton in the given designation.
```
lemma actual_unlit_le_twice_extra (label : τ → ι) (lit : τ → Bool) :
    (∑ i : nonsingletonLabels label, (unlitOccurrences label lit i.val).card) ≤
      2 * ∑ i : nonsingletonLabels label,
        extraReciprocalExponent (litOccurrences label lit i.val).card
          (unlitOccurrences label lit i.val).card := by
…
```
Mentions: OAI.TwoPointCorrelations.nonsingletonLabels, OAI.TwoPointCorrelations.unlitOccurrences, OAI.TwoPointCorrelations.extraReciprocalExponent, OAI.TwoPointCorrelations.litOccurrences