Entry.lean`

1 declarations, 0 contain sorry, 0 declared as axioms

Entry depth for the all-dimensional assembly

This is the numerical content of asm:entry. The dimension enters through the Lipschitz constant of the two excess profiles. The envelope and dimension constants are independent.

theorem OAI.Falconer.exists_assembly_entry line 21

Source documentation

A common entry depth with a small graph cost and two positive tail potentials. The large-scale hypothesis is explicit; the manuscript uses this only for all sufficiently large N.

theorem exists_assembly_entry (A : Fin 2 → ℕ → ℝ) (N Q : ℕ)
    {d χ β ε : ℝ} (hd : 0 < d) (hχ : 0 < χ) (hβ : 0 < β)
    (hε : 0 ≤ ε) (hsmall : β + ε < χ / 4)
    (hN : 0 < N) (hlarge : 2 * d ≤ β * (N : ℝ))
    (hQ : 0 < Q) (hQsmall : 4 * Q ≤ N)
    (hzero : ∀ i, A i 0 = 0)
    (henvelope : ∀ i n, n ≤ N → χ * (n : ℝ) / N - ε ≤ A i n)
    (hlip : ∀ i m n, m ≤ N → n ≤ N →
      |A i n - A i m| ≤ d * |(n : ℝ) - m| / N) :
    ∃ c : ℕ, c < N ∧ β * N / (2 * d) ≤ (c : ℝ) ∧ (c : ℝ) < N / 4 ∧
      c + Q ≤ N ∧
      (∀ i n, c ≤ n → n ≤ N → β - d / N ≤ A i n) ∧
…