ObservedDesignationWeights.lean`

7 declarations, 0 contain sorry, 0 declared as axioms

Exact designation weights when the ambient prime pool contains unused primes.

lemma OAI.TwoPointCorrelations.filtered_power_product line 14

theorem OAI.TwoPointCorrelations.observed_designation_reciprocal_factor line 27

Source documentation

Each observed prime contributes one baseline reciprocal, including singletons. Only repeated labels contribute additional exponents.

theorem observed_designation_reciprocal_factor (label : τ → ι) (lit : τ → Bool)
    (p : ι → ℝ) :
    (∏ t ∈ nonsingletonUnlitSlots label lit, (p (label t))⁻¹) *
      (∏ i ∈ (nonsingletonLitSlots label lit).image label, (p i)⁻¹) *
      (∏ i ∈ singletonLabels label, (p i)⁻¹) =
        (∏ i ∈ univ.image label, (p i)⁻¹) *
          ∏ i ∈ nonsingletonLabels label, (p i)⁻¹ ^
            extraReciprocalExponent (litOccurrences label lit i).card
              (unlitOccurrences label lit i).card := by
…

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

theorem OAI.TwoPointCorrelations.observed_designation_reciprocal_bound line 82
def OAI.TwoPointCorrelations.designationLit line 101
lemma OAI.TwoPointCorrelations.designationLit_unlit line 103
lemma OAI.TwoPointCorrelations.designationLit_lit line 114
theorem OAI.TwoPointCorrelations.full_word_designated_reciprocal_bound line 121
Source documentation
The coefficient in the full signed expansion retains the actual extra-exponent saving even when unused primes occur in the ambient pool.
```
theorem full_word_designated_reciprocal_bound (label : τ → ι) (U : Finset τ)
    (hU : U ⊆ nonsingletonSlots label) (p : ι → ℕ) (H : ℝ)
    (hH : 0 < H) (hp : ∀ i, H ≤ p i) :
    designatedReciprocal p (singletonLabels label) (nonsingletonSlots label \ U) U label ≤
      (∏ i ∈ univ.image label, (p i : ℝ)⁻¹) * H⁻¹ ^
        (∑ i ∈ nonsingletonLabels label,
          extraReciprocalExponent (litOccurrences label (designationLit U) i).card
            (unlitOccurrences label (designationLit U) i).card) := by
…
```
Mentions: OAI.TwoPointCorrelations.nonsingletonSlots, OAI.TwoPointCorrelations.designatedReciprocal, OAI.TwoPointCorrelations.singletonLabels, OAI.TwoPointCorrelations.nonsingletonLabels, OAI.TwoPointCorrelations.extraReciprocalExponent, OAI.TwoPointCorrelations.litOccurrences, OAI.TwoPointCorrelations.designationLit, OAI.TwoPointCorrelations.unlitOccurrences