PaddingSum.lean`

6 declarations, 0 contain sorry, 0 declared as axioms

Summing padding choices in one fixed residue environment

This is the backwards induction of manuscript Lemma q:padding-sum. A state is the current integer site. The transitions may depend on the current padding choice and all earlier choices through that site. No independence of translated residue coordinates is assumed.

def OAI.TwoPointCorrelations.paddingMass line 20

Source documentation

The finite sum over successive padding choices, with i the step index.

def paddingMass (Q : Finset ℕ) (weight : ℕ → ℤ → ℕ → ℝ)
    (next : ℕ → ℤ → ℕ → ℤ) : ℕ → ℕ → ℤ → ℝ
  | 0, _, _ => 1
  | m + 1, i, n => ∑ q ∈ Q, weight i n q * paddingMass Q weight next m (i + 1) (next i n q)

/-- A row bound at every site controls the full path sum, despite the dependence
of later sites on earlier padding choices. -/

theorem OAI.TwoPointCorrelations.paddingMass_le line 27

Source documentation

A row bound at every site controls the full path sum, despite the dependence of later sites on earlier padding choices.

theorem paddingMass_le (Q : Finset ℕ) (weight : ℕ → ℤ → ℕ → ℝ)
    (next : ℕ → ℤ → ℕ → ℤ) (K : ℝ) (hK : 0 ≤ K)
    (hweight : ∀ i n q, q ∈ Q → 0 ≤ weight i n q)
    (hrow : ∀ i n, ∑ q ∈ Q, weight i n q ≤ K)
    (m i : ℕ) (n : ℤ) : paddingMass Q weight next m i n ≤ K ^ m := by
…

Mentions: OAI.TwoPointCorrelations.paddingMass

def OAI.TwoPointCorrelations.cutPaddingWeight line 47

Source documentation

The departure cutoff retains a row only when its total mass is at most K.

noncomputable def cutPaddingWeight (Q : Finset ℕ) (raw : ℕ → ℤ → ℕ → ℝ)
    (K : ℝ) (i : ℕ) (n : ℤ) (q : ℕ) : ℝ :=
…

theorem OAI.TwoPointCorrelations.cutPaddingWeight_nonneg line 51
theorem OAI.TwoPointCorrelations.cutPaddingWeight_row line 60
theorem OAI.TwoPointCorrelations.cut_paddingMass_le line 69
Source documentation
Manuscript padding bound, after the departure cutoff. The choice next i n q = n + εᵢ h q dᵢ is allowed, as is a different residue at every site.
```
theorem cut_paddingMass_le (Q : Finset ℕ) (raw : ℕ → ℤ → ℕ → ℝ)
    (next : ℕ → ℤ → ℕ → ℤ) (K : ℝ) (hK : 0 ≤ K)
    (hraw : ∀ i n q, q ∈ Q → 0 ≤ raw i n q)
    (m i : ℕ) (n : ℤ) :
    paddingMass Q (cutPaddingWeight Q raw K) next m i n ≤ K ^ m := by
…
```
Mentions: OAI.TwoPointCorrelations.paddingMass, OAI.TwoPointCorrelations.cutPaddingWeight