RankEnumeration.lean`

3 declarations, 0 contain sorry, 0 declared as axioms

Explicit enumeration costs before the high-rank saving.

lemma OAI.TwoPointCorrelations.rankPairChoices_exp_bound line 13

Source documentation

Count the column and the ordered choices of its controlling pairs.

lemma rankPairChoices_exp_bound (J R r a b : ℕ) (L : ℝ)
    (hL : 1 ≤ L) (hJ : (J : ℝ) ≤ L ^ a)
    (hR : (R : ℝ) + 1 ≤ L ^ b) (hr : (r : ℝ) ≤ L) :
    (J * R ^ (2 * r) : ℕ) ≤
      Real.exp (((a : ℝ) + 2 * b) * L * Real.log L) := by
…

lemma OAI.TwoPointCorrelations.harmonic_power_exp_bound line 48

Source documentation

A reciprocal mass bounded by L² costs only two logarithms per slot.

lemma harmonic_power_exp_bound (V L C : ℝ) (n : ℕ)
    (hL : 0 < L) (hV : 0 ≤ V) (hV' : V ≤ L ^ (2 : ℕ))
    (hn : (n : ℝ) ≤ C * L * Real.log L) (hlog : 0 ≤ Real.log L) :
    V ^ n ≤ Real.exp (2 * C * L * (Real.log L) ^ 2) := by
…

theorem OAI.TwoPointCorrelations.rank_enumeration_exp_bound line 68

Source documentation

The crude pattern, selected-pair, harmonic, and external costs, all before imposing any congruences. The constants describe only fixed polynomial alphabets and the slot budget.

theorem rank_enumeration_exp_bound (J R N D d a b r n : ℕ)
    (L C Cmass Cweight V W : ℝ)
    (hL : 1 ≤ Real.log L) (hL' : 1 ≤ L)
    (hRN : R ≤ N) (hR : (R : ℝ) ≤ 2 * L) (hC : 0 ≤ C)
    (hslots : (N : ℝ) ≤ C * R * Real.log L)
    (hN : (N : ℝ) + 1 ≤ L ^ (2 : ℕ)) (hD : (D : ℝ) + 1 ≤ L ^ d)
    (hJ : (J : ℝ) ≤ L ^ a) (hRpoly : (R : ℝ) + 1 ≤ L ^ b)
    (hr : (r : ℝ) ≤ L)
    (hV : 0 ≤ V) (hV' : V ≤ L ^ (2 : ℕ))
    (hn : (n : ℝ) ≤ Cmass * L * Real.log L)
    (hW : 0 ≤ W) (hW' : W ≤ Real.exp (Cweight * L * (Real.log L) ^ 2)) :
    (Fintype.card (CrudeWordCode R N D) : ℝ) *
…

Mentions: OAI.TwoPointCorrelations.CrudeWordCode