ResidueTraceBound.lean`

2 declarations, 0 contain sorry, 0 declared as axioms

The manuscript's designated-term majorant for actual uniform residues.

def OAI.TwoPointCorrelations.designatedReciprocal line 17
Source documentation
The exact reciprocal coefficient of one lit/unlit designation, including the singleton atoms.
```
noncomputable def designatedReciprocal (p : ι → ℕ) (S : Finset ι)
    (L U : Finset τ) (label : τ → ι) : ℝ :=
…
```

theorem OAI.TwoPointCorrelations.uniform_designated_trace_bound line 24

Source documentation

Singleton integration and lit forcing are carried out on one common residue sample. The unlit slots impose no further residue condition.

theorem uniform_designated_trace_bound (B : ℕ) (p : ι → ℕ)
    (hp : ∀ i, 0 < p i) (hpB : ∀ i, p i ≤ B)
    (S : Finset ι) (L U : Finset τ) (label : τ → ι) (target : τ → Fin B)
    (a base : ι → Fin B) (R : ℝ) (G : (ι → Fin B) → ℝ)
    (hR : 0 ≤ R) (hL : LitConsistent L label target)
    (hSL : Disjoint S (L.image label))
    (ha : ∀ i ∈ S, (a i).val < p i)
    (htarget : ∀ t ∈ L, (target t).val < p (label t)) :
    |(FiniteLaw.independent (fun i => uniformResidueLaw B (p i) (hp i) (hpB i))).average
      (fun x => (R * ((-1 : ℝ) ^ U.card * ∏ t ∈ U, (p (label t) : ℝ)⁻¹)) *
        ((∏ t ∈ L, if x (label t) = target t then (1 : ℝ) else 0) *
          ((∏ i ∈ S, ((if x i = a i then (1 : ℝ) else 0) - (p i : ℝ)⁻¹)) * G x)))| ≤
…

Mentions: OAI.TwoPointCorrelations.LitConsistent, OAI.TwoPointCorrelations.FiniteLaw.independent, OAI.TwoPointCorrelations.uniformResidueLaw