TupleRecovery.lean`

7 declarations, 0 contain sorry, 0 declared as axioms

The prime-occurrence allocation bound in equations (residual-factorization) and (tuple-recovery-cost). Repeated prime factors are counted with multiplicity.

lemma OAI.TotientAsymptotic.prod_update_div line 14
lemma OAI.TotientAsymptotic.update_div_injOn line 22

theorem OAI.TotientAsymptotic.ordered_factorizations_card_le line 40

Source documentation

Ordered factorizations into k labeled slots are bounded by assigning each prime occurrence to a slot. The finite set may contain any chosen restrictions.

theorem ordered_factorizations_card_le {ι : Type*} [Fintype ι] [DecidableEq ι]
    (n : ℕ) (hn : 0 < n) (T : Finset (ι → ℕ))
    (hT : ∀ f ∈ T, ∏ i, f i = n) :
    T.card ≤ (Fintype.card ι)^n.primeFactorsList.length := by
…

theorem OAI.TotientAsymptotic.ordered_factorization_pairs_card_le line 94

Source documentation

The two residual factorizations in an ordered collision pair have the product of the two prime-occurrence bounds, including repeated factors.

theorem ordered_factorization_pairs_card_le {ι κ : Type*}
    [Fintype ι] [DecidableEq ι] [Fintype κ] [DecidableEq κ]
    (n m : ℕ) (hn : 0 < n) (hm : 0 < m)
    (T : Finset (ι → ℕ)) (U : Finset (κ → ℕ))
    (hT : ∀ f ∈ T, ∏ i, f i = n) (hU : ∀ f ∈ U, ∏ i, f i = m) :
    (T ×ˢ U).card ≤ (Fintype.card ι)^n.primeFactorsList.length *
      (Fintype.card κ)^m.primeFactorsList.length := by
…

Mentions: OAI.TotientAsymptotic.m

def OAI.TotientAsymptotic.prefixDatumEncoding line 105
lemma OAI.TotientAsymptotic.prefixDatumEncoding_injOn line 108
theorem OAI.TotientAsymptotic.prefixData_card_le line 128
Source documentation
Concrete tuple data inside a residual totient are bounded by the ordered factorization estimate. The tail totient is a separate, final factor.
```
theorem prefixData_card_le {n D : ℕ} (hD : 0 < D) (T : Finset (PrefixDatum n))
    (hp : ∀ t ∈ T, ∀ i, 1 ≤ t.primes i)
    (hprod : ∀ t ∈ T, t.d * (∏ i, (t.primes i-1)) = D) :
    T.card ≤ (n+1)^D.primeFactorsList.length := by
…
```
Mentions: OAI.TotientAsymptotic.D, OAI.TotientAsymptotic.PrefixDatum