OAI/NumberTheory/TwoPoint/Bounds/PaddingWordSum.lean

GitHub source file

3 declarations, 0 contain sorry, 0 declared as axioms

The recursive padding bound is the full sum over actual padding words.

  1. def OAI.TwoPointCorrelations.paddingWordWeight line 12
  2. theorem OAI.TwoPointCorrelations.paddingMass_eq_sum_words line 18
  3. theorem OAI.TwoPointCorrelations.retained_padding_word_sum_le line 35

    Source documentation

    Literal finite path sum, retaining the departure density cutoff at every visited site, uniformly in all earlier padding choices.

    theorem retained_padding_word_sum_le (Q : Finset ℕ) (u : ℕ → ℝ)
    (eligible : ℕ → ℕ → Prop) (g : ℤ → ℝ) (L K : ℝ)
    (extra : ℕ → ℤ → Prop) (next : ℕ → ℤ → ℕ → ℤ)
    (hL : 0 < L) (hK : 0 ≤ K) (hu : ∀ q ∈ Q, 0 ≤ u q)
    (m i : ℕ) (n : ℤ) :
    (∑ q : Fin m → Q, paddingWordWeight Q
      (fun i n q => retainedPaddingAtom Q u (eligible i) g L K (extra i) n q)
      next i n q) ≤ K ^ m := by
…

    Mentions: OAI.TwoPointCorrelations.paddingWordWeight, OAI.TwoPointCorrelations.retainedPaddingAtom