DepartureWeightBounds.lean`

4 declarations, 0 contain sorry, 0 declared as axioms

Bounds for the actual normalized departure factors after the cutoffs are discarded.

def OAI.TwoPointCorrelations.departureWeight line 11
lemma OAI.TwoPointCorrelations.departureWeight_nonneg line 15
lemma OAI.TwoPointCorrelations.departureWeight_le_crude line 23

theorem OAI.TwoPointCorrelations.departureWeight_designation_cost line 41

Source documentation

All designation and singleton multiplicities are included in this cost.

theorem departureWeight_designation_cost {r m S : ℕ}
    (L external Cexternal Csingle : ℝ) (u : ℕ → ℝ) (q : Fin r → ℕ)
    (denom cutoff : Fin r → ℝ)
    (hL : 1 ≤ L) (hlog : 1 ≤ Real.log L) (hr : (r : ℝ) ≤ 2 * L)
    (hS : ((m + S : ℕ) : ℝ) ≤ Csingle * L * Real.log L)
    (hCe : 0 ≤ Cexternal) (he : 0 ≤ external)
    (hext : external ≤ Real.exp (Cexternal * L))
    (hpad : ∀ i, ((q i).primeFactors.card : ℝ) ≤ 100 * Real.log L)
    (hu : ∀ i, 0 ≤ u (q i)) (hub : ∀ i, u (q i) ≤ crudePaddingWeight (q i))
    (hd : ∀ i, 1 ≤ denom i) (hc : ∀ i, 0 ≤ cutoff i) (hcb : ∀ i, cutoff i ≤ 1) :
    (external * departureWeight L u q denom cutoff) * 2 ^ (m + S) ≤
      Real.exp ((Cexternal + Csingle + 402) * L * (Real.log L) ^ 2) := by
…

Mentions: OAI.TwoPointCorrelations.crudePaddingWeight, OAI.TwoPointCorrelations.departureWeight