ActualDesignations.lean`

8 declarations, 0 contain sorry, 0 declared as axioms

Literal lit/unlit slot sets and the reciprocal coefficient of an actual word.

def OAI.TwoPointCorrelations.nonsingletonLitSlots line 14
def OAI.TwoPointCorrelations.nonsingletonUnlitSlots line 17
lemma OAI.TwoPointCorrelations.nonsingleton_lit_fiber line 20
lemma OAI.TwoPointCorrelations.nonsingleton_unlit_fiber line 28
lemma OAI.TwoPointCorrelations.singleton_not_nonsingleton line 36
lemma OAI.TwoPointCorrelations.nonsingleton_of_used_not_singleton line 42
lemma OAI.TwoPointCorrelations.nonsingleton_unlit_card line 51
Source documentation
The literal number of unlit nonsingleton slots is the sum of their per-label occurrence counts, without charging singleton slots.
```
lemma nonsingleton_unlit_card (label : τ → ι) (lit : τ → Bool) :
    (nonsingletonUnlitSlots label lit).card =
      ∑ i : nonsingletonLabels label, (unlitOccurrences label lit i.val).card := by
…
```
Mentions: OAI.TwoPointCorrelations.nonsingletonUnlitSlots, OAI.TwoPointCorrelations.nonsingletonLabels, OAI.TwoPointCorrelations.unlitOccurrences

theorem OAI.TwoPointCorrelations.actual_designation_reciprocal_bound line 59

Source documentation

On actual observed labels, the designated coefficient has one basic reciprocal per prime and the exact extra powers from the nonsingletons.

theorem actual_designation_reciprocal_bound (label : τ → ι) (lit : τ → Bool)
    (hused : ∀ i, 0 < (labelOccurrences label i).card)
    (p : ι → ℝ) (H : ℝ) (hH : 0 < H) (hp : ∀ i, H ≤ p i) :
    (∏ t ∈ nonsingletonUnlitSlots label lit, (p (label t))⁻¹) *
      (∏ i ∈ (nonsingletonLitSlots label lit).image label, (p i)⁻¹) *
      (∏ i ∈ singletonLabels label, (p i)⁻¹) ≤
        (∏ i, (p i)⁻¹) * H⁻¹ ^
          (∑ i : nonsingletonLabels label,
            extraReciprocalExponent (litOccurrences label lit i.val).card
              (unlitOccurrences label lit i.val).card) := by
…

Mentions: OAI.TwoPointCorrelations.labelOccurrences, OAI.TwoPointCorrelations.nonsingletonUnlitSlots, OAI.TwoPointCorrelations.nonsingletonLitSlots, OAI.TwoPointCorrelations.singletonLabels, OAI.TwoPointCorrelations.nonsingletonLabels, OAI.TwoPointCorrelations.extraReciprocalExponent, OAI.TwoPointCorrelations.litOccurrences, OAI.TwoPointCorrelations.unlitOccurrences