CrudeTraceWeights.lean`

5 declarations, 0 contain sorry, 0 declared as axioms

Padding, mixed-difference, and external factors in the crude trace count.

lemma OAI.TwoPointCorrelations.crudePaddingWeight_exp_bound line 11
lemma OAI.TwoPointCorrelations.crudePaddingFactors_exp_bound line 34
def OAI.TwoPointCorrelations.crudeTraceWeight line 58
Source documentation
The positive trace factors left after discarding all denominator cutoffs. This includes the full mixed-difference multiplicity.
```
noncomputable def crudeTraceWeight (R S : ℕ) (q : Fin R → ℕ) (L external : ℝ) : ℝ :=
…
```
lemma OAI.TwoPointCorrelations.crudeTraceWeight_nonneg line 61

theorem OAI.TwoPointCorrelations.crudeTraceWeight_exp_bound line 69

Source documentation

Fixed exponential dimension factors and all step weights are absorbed by an explicit L log² L cost.

theorem crudeTraceWeight_exp_bound (R S : ℕ) (q : Fin R → ℕ)
    (L external Cexternal Csingle : ℝ)
    (hL : 1 ≤ L) (hlog : 1 ≤ Real.log L)
    (hR : (R : ℝ) ≤ 2 * L) (hS : (S : ℝ) ≤ Csingle * L * Real.log L)
    (hCexternal : 0 ≤ Cexternal)
    (hext : external ≤ Real.exp (Cexternal * L))
    (hq : ∀ i, ((q i).primeFactors.card : ℝ) ≤ 100 * Real.log L) :
    crudeTraceWeight R S q L external ≤
      Real.exp ((Cexternal + Csingle + 402) * L * (Real.log L) ^ 2) := by
…

Mentions: OAI.TwoPointCorrelations.crudeTraceWeight