CrudeWordCounting.lean`

GitHub source file

12 declarations, 0 contain sorry, 0 declared as axioms

Finite descriptions used by the reciprocal crude count.

def OAI.TwoPointCorrelations.slotPartitionCode line 16
Source documentation
A partition is recorded by a representative slot for each slot.
Also declared: OAI/NumberTheory/TwoPointCorrelations/CrudeWordCounting.lean:16 (same declaration text).
```
noncomputable def slotPartitionCode (N : ℕ) (s : Setoid (Fin N)) : Fin N → Fin N :=
…
```
lemma OAI.TwoPointCorrelations.slotPartitionCode_eq_iff line 19
Also declared: OAI/NumberTheory/TwoPointCorrelations/CrudeWordCounting.lean:19 (same declaration text).
lemma OAI.TwoPointCorrelations.slotPartitionCode_injective line 23
Also declared: OAI/NumberTheory/TwoPointCorrelations/CrudeWordCounting.lean:23 (same declaration text).
theorem OAI.TwoPointCorrelations.card_slotPartitions_le line 30
Source documentation
The elementary Bell-number bound used in q:crude-count.
Also declared: OAI/NumberTheory/TwoPointCorrelations/CrudeWordCounting.lean:30 (same declaration text).
```
theorem card_slotPartitions_le (N : ℕ) : Nat.card (Setoid (Fin N)) ≤ N ^ N := by
…
```
abbrev OAI.TwoPointCorrelations.CrudeWordCode line 35
Source documentation
Signs, a partition code, bounded records per slot, and lit designations.
Also declared: OAI/NumberTheory/TwoPointCorrelations/CrudeWordCounting.lean:35 (same declaration text).
```
abbrev CrudeWordCode (R N D : ℕ) :=
…
```
theorem OAI.TwoPointCorrelations.card_crudeWordCode line 38
Also declared: OAI/NumberTheory/TwoPointCorrelations/CrudeWordCounting.lean:38 (same declaration text).
abbrev OAI.TwoPointCorrelations.RankPairChoices line 45
Source documentation
A column and an ordered list of candidate lit pairs have at most this many descriptions. Repeated or invalid descriptions only enlarge the bound.
Also declared: OAI/NumberTheory/TwoPointCorrelations/CrudeWordCounting.lean:45 (same declaration text).
```
abbrev RankPairChoices (J R r : ℕ) := Fin J × (Fin r → Fin R × Fin R)
```
theorem OAI.TwoPointCorrelations.card_rankPairChoices line 47
Also declared: OAI/NumberTheory/TwoPointCorrelations/CrudeWordCounting.lean:47 (same declaration text).
theorem OAI.TwoPointCorrelations.FiniteLaw.probability_exists_le line 54
Source documentation
A finite union bound for arbitrary events under the concrete finite law.
Also declared: OAI/NumberTheory/TwoPointCorrelations/CrudeWordCounting.lean:54 (same declaration text).
```
theorem FiniteLaw.probability_exists_le {A I : Type*} [Fintype A] [Fintype I]
    (μ : FiniteLaw A) (E : I → A → Prop) :
    μ.probability (fun x => ∃ i, E i x) ≤ ∑ i, μ.probability (E i) := by
…
```
Mentions: OAI.TwoPointCorrelations.FiniteLaw
theorem OAI.TwoPointCorrelations.rank_pair_union_bound line 72
Source documentation
Uniform bounds may be summed over the explicit column/pair records.
Also declared: OAI/NumberTheory/TwoPointCorrelations/CrudeWordCounting.lean:72 (same declaration text).
```
theorem rank_pair_union_bound {A : Type*} [Fintype A]
    (μ : FiniteLaw A) (J R r : ℕ) (E : RankPairChoices J R r → A → Prop)
    (B : ℝ) (hB : ∀ c, μ.probability (E c) ≤ B) :
    μ.probability (fun x => ∃ c, E c x) ≤ (J * R ^ (2 * r) : ℕ) * B := by
…
```
Mentions: OAI.TwoPointCorrelations.FiniteLaw, OAI.TwoPointCorrelations.RankPairChoices
lemma OAI.TwoPointCorrelations.card_crudeWordCode_exp line 81
Also declared: OAI/NumberTheory/TwoPointCorrelations/CrudeWordCounting.lean:81 (same declaration text).
theorem OAI.TwoPointCorrelations.crudeWordCode_bound line 102
Source documentation
The slot bound N ≤ C R log L and polynomial record alphabets yield the manuscript's exp (O(R log² L)) count with an explicit coefficient.
Also declared: OAI/NumberTheory/TwoPointCorrelations/CrudeWordCounting.lean:102 (same declaration text).
```
theorem crudeWordCode_bound (R N D d : ℕ) (L C : ℝ)
    (hL : 1 ≤ Real.log L) (hRN : R ≤ N)
    (hslots : (N : ℝ) ≤ C * R * Real.log L)
    (hN : (N : ℝ) + 1 ≤ L ^ (2 : ℕ))
    (hD : (D : ℝ) + 1 ≤ L ^ d) :
    (Fintype.card (CrudeWordCode R N D) : ℝ) ≤
      Real.exp (((d : ℝ) + 4) * C * R * (Real.log L) ^ 2) := by
…
```
Mentions: OAI.TwoPointCorrelations.CrudeWordCode