PrimeWordEncoding.lean`

6 declarations, 0 contain sorry, 0 declared as axioms

A single finite universe covers all numerical words with bounded prime slots.

abbrev OAI.TwoPointCorrelations.PrimeWordEncoding line 13
Source documentation
Slot count, complete equality-pattern code, and separate prime-pool assignments.
```
abbrev PrimeWordEncoding (R T : ℕ) (P Q : Finset ℕ) :=
…
```
def OAI.TwoPointCorrelations.PrimeWordEncoding.decode line 21
def OAI.TwoPointCorrelations.PrimeWordEncoding.weight line 25
lemma OAI.TwoPointCorrelations.PrimeWordEncoding.weight_nonneg line 29

theorem OAI.TwoPointCorrelations.PrimeWordEncoding.covers line 34

Source documentation

No loss in the reciprocal weight occurs on encoding an actual word.

theorem covers (w : Fin R → SignedStep)
    (hT : Fintype.card (ActualPrimeSlot w) ≤ T)
    (ht : ∀ i, Squarefree (w i).tuple) (hq : ∀ i, Squarefree (w i).padding)
    (hP : ∀ i, (w i).tuple.primeFactors ⊆ P)
    (hQ : ∀ i, (w i).padding.primeFactors ⊆ Q)
    (hd : ∀ i j, Disjoint (w i).tuple.primeFactors (w j).padding.primeFactors) :
    ∃ e : PrimeWordEncoding R T P Q, e.decode = List.ofFn w ∧
      e.2.1.KindConsistent ∧ e.2.1.RowInjective ∧
      Function.Injective (fun z => (e.2.2.1 z).val) ∧
      e.weight = ∏ p ∈ wordDivisorPrimeSupport (List.ofFn w), (p : ℝ)⁻¹ := by
…

Mentions: OAI.TwoPointCorrelations.SignedStep, OAI.TwoPointCorrelations.ActualPrimeSlot, OAI.TwoPointCorrelations.PrimeWordEncoding, OAI.TwoPointCorrelations.wordDivisorPrimeSupport

theorem OAI.TwoPointCorrelations.finite_decoding_weight_bound line 71

Source documentation

A finite decoding cover also covers every nonnegative weighted sum. The chosen representatives are injective because decoding recovers the word.

theorem finite_decoding_weight_bound {W C : Type*} [DecidableEq W] [Fintype C]
    (F : Finset W) (decode : C → W) (weight : W → ℝ) (cost : C → ℝ)
    (hcost : ∀ c, 0 ≤ cost c)
    (hcover : ∀ w ∈ F, ∃ c, decode c = w ∧ weight w ≤ cost c) :
    (∑ w ∈ F, weight w) ≤ ∑ c, cost c := by
…