Kernels.lean`

30 declarations, 0 contain sorry, 0 declared as axioms

Kernels

Constrained rank-gap sums, correlated anchor kernels, window kernels, lattice Laplace sums, and geometric degree bounds.

theorem OAI.TraceReconstruction.constrained_sum_product_le line 20

Source documentation

Eliminate one output gap by its prescribed total before dropping the other rank constraints. This is the exact finite summation step used in the conditional rank-kernel estimate.

theorem constrained_sum_product_le (r L : ℕ)
    (f : Fin (r + 1) → Fin (L + 1) → ℝ)
    (hf : ∀ i k, 0 ≤ f i k) (M : ℝ) (hM : 0 ≤ M)
    (hbound : ∀ k, f 0 k ≤ M) :
    (∑ z : Fin (r + 1) → Fin (L + 1),
      if ∑ j, (z j).val = L then ∏ j, f j (z j) else 0) ≤
        M * ∏ i : Fin r, ∑ k, f i.succ k := by
…

theorem OAI.TraceReconstruction.constrained_cross_kernel_le line 58

Source documentation

The product of two rank kernels has one scalar denominator factor, one uniform gap factor and independent one-dimensional cross-overlaps.

theorem constrained_cross_kernel_le (r L : ℕ)
    (f g : Fin (r + 1) → Fin (L + 1) → ℝ)
    (hf : ∀ i k, 0 ≤ f i k) (hg : ∀ i k, 0 ≤ g i k)
    (M : ℝ) (hM : 0 ≤ M) (hbound : ∀ k, f 0 k * g 0 k ≤ M) :
    (∑ z : Fin (r + 1) → Fin (L + 1),
      if ∑ j, (z j).val = L then (∏ j, f j (z j)) * (∏ j, g j (z j)) else 0) ≤
        M * ∏ i : Fin r, ∑ k, f i.succ k * g i.succ k := by
…

def OAI.TraceReconstruction.jointKernel line 88

Source documentation

Mixture of conditional products; p is the common displacement law.

def jointKernel (p : Ω → ℝ) (a : Ω → I → ℝ) (b : Ω → J → ℝ)
    (i : I) (j : J) : ℝ := ∑ w, p w * a w i * b w j
…

theorem OAI.TraceReconstruction.jointKernel_nonneg line 92
theorem OAI.TraceReconstruction.sum_jointKernel line 99
theorem OAI.TraceReconstruction.jointKernel_le line 115

theorem OAI.TraceReconstruction.correlated_anchor_square_sum line 131

Source documentation

The joint squared-sum estimate retaining the common jitter. In the manuscript A=L/(omega*sqrt(T*t)) and B=M/(omega*sqrt(t)), up to the explicit absolute binomial constants.

theorem correlated_anchor_square_sum
    (p : Ω → ℝ) (a : Ω → I → ℝ) (b : Ω → J → ℝ)
    (L M A B : ℝ)
    (hp0 : ∀ w, 0 ≤ p w) (hp1 : ∑ w, p w = 1)
    (ha0 : ∀ w i, 0 ≤ a w i) (hb0 : ∀ w j, 0 ≤ b w j)
    (ha1 : ∀ w, ∑ i, a w i = L) (hb1 : ∀ w, ∑ j, b w j = M)
    (hB : 0 ≤ B) (hb : ∀ w j, b w j ≤ B)
    (hA : ∀ i, ∑ w, p w * a w i ≤ A) :
    ∑ i, ∑ j, (jointKernel p a b i j) ^ 2 ≤ (A * B) * (L * M) := by
…

Mentions: OAI.TraceReconstruction.jointKernel

theorem OAI.TraceReconstruction.binomial_overlap_truncate line 162

Source documentation

Truncating output ranks cannot increase a binomial cross-overlap.

theorem binomial_overlap_truncate (g h L : ℕ) {p : ℝ}
    (hp : p ∈ Set.Icc 0 1) :
    (∑ k : Fin (L + 1), binomialMass g p k * binomialMass h p k) ≤
      ∑ k ∈ Finset.range (h + 1), binomialMass g p k * binomialMass h p k := by
…

Mentions: OAI.TraceReconstruction.binomialMass

theorem OAI.TraceReconstruction.binomial_gaussian_overlap_general line 182

Source documentation

Gaussian cross-overlap with the prefactor attached to either prescribed first length, removing the order restriction in the tilting proof.

theorem binomial_gaussian_overlap_general (g h L : ℕ) {p : ℝ}
    (hp : p ∈ Set.Ico (1 / 2 : ℝ) 1) (hS : 0 < g + h) :
    (∑ k : Fin (L + 1), binomialMass g p k * binomialMass h p k) ≤
      Real.sqrt (2 / (((g : ℝ) + 1) * p * (1 - p))) *
        Real.exp (-((g : ℝ) - h) ^ 2 / (16 * ((g : ℝ) + h))) := by
…

Mentions: OAI.TraceReconstruction.binomialMass

def OAI.TraceReconstruction.rankKernel line 212
Source documentation
The exact conditional rank kernel, including the fixed count normalization, before any coarse-gap estimates or restrictions.
```
def rankKernel (r n l : ℕ) (p : ℝ) (g : Fin (r + 1) → ℕ)
    (z : Fin (r + 1) → Fin (l + 1)) : ℝ :=
…
```

theorem OAI.TraceReconstruction.rankKernel_cross_le line 219

Source documentation

Largest-gap elimination for the conditional rank kernel. The displayed constant is absolute; no asymptotic proposal or Stirling theorem is assumed.

theorem rankKernel_cross_le (r n l : ℕ) {p : ℝ}
    (hp : p ∈ Set.Ico (1 / 2 : ℝ) 1) (hl : l ≤ n)
    (hmean : (n : ℝ) * p = l) (hv : 1 ≤ (n : ℝ) * p * (1 - p))
    (g h : Fin (r + 1) → ℕ) :
    (∑ z : Fin (r + 1) → Fin (l - r + 1),
      if ∑ j, (z j).val = l - r then
        (p ^ r / binomialMass n p l) ^ 2 *
          (∏ j, binomialMass (g j) p (z j)) *
          (∏ j, binomialMass (h j) p (z j)) else 0) ≤
      (4608 * n / ((g 0 : ℝ) + 1)) *
        ∏ i : Fin r, ∑ k : Fin (l - r + 1),
          binomialMass (g i.succ) p k * binomialMass (h i.succ) p k := by
…

Mentions: OAI.TraceReconstruction.binomialMass

theorem OAI.TraceReconstruction.fairSeries_total line 279
theorem OAI.TraceReconstruction.fairSeries_sum_finite_le_one line 284
def OAI.TraceReconstruction.windowKernel line 294
theorem OAI.TraceReconstruction.windowKernel_nonneg line 297
theorem OAI.TraceReconstruction.windowKernel_sup line 300
theorem OAI.TraceReconstruction.windowKernel_sum line 309
theorem OAI.TraceReconstruction.windowKernel_energy line 321
def OAI.TraceReconstruction.jointWindowKernel line 334
theorem OAI.TraceReconstruction.windowKernel_average line 338
theorem OAI.TraceReconstruction.jointWindowKernel_nonneg line 352
theorem OAI.TraceReconstruction.jointWindowKernel_sup line 359
theorem OAI.TraceReconstruction.jointWindowKernel_sum line 380
theorem OAI.TraceReconstruction.jointWindowKernel_energy line 413
theorem OAI.TraceReconstruction.sum_inverse_sqrt line 440
Source documentation
Elementary discrete integral comparison, including the singular first cell.
```
theorem sum_inverse_sqrt (N : ℕ) :
    (∑ k ∈ Finset.range N, (Real.sqrt (k+1:ℝ))⁻¹) ≤ 2*Real.sqrt N := by
…
```
theorem OAI.TraceReconstruction.exp_gap_lower line 457
theorem OAI.TraceReconstruction.sum_exp_decay line 467

theorem OAI.TraceReconstruction.coarse_laplace_sum line 489

Source documentation

The uniform lattice Laplace estimate used by the initial-pair construction, with an absolute constant.

theorem coarse_laplace_sum {h : ℝ} (hh : 0 < h) (h1 : h ≤ 1) (M : ℕ) :
    (∑ k ∈ Finset.range M, (Real.sqrt (k+1:ℝ))⁻¹ *
      Real.exp (-h*(k+1:ℝ))) ≤ 6/Real.sqrt h := by
…

theorem OAI.TraceReconstruction.coarse_simplex_sum line 558

Source documentation

Exponential tilting removes the coarse-gap simplex constraint without a dimension loss.

theorem coarse_simplex_sum (r M : ℕ) {h u : ℝ} (hh : 0<h) (h1 : h≤1) :
    (∑ v : Fin r → Fin M, if (∑ i, ((v i).val+1:ℝ)) ≤ u then
      ∏ i, (Real.sqrt ((v i).val+1:ℝ))⁻¹ else 0) ≤
      Real.exp (h*u) * (6/Real.sqrt h)^r := by
…

theorem OAI.TraceReconstruction.degree_series_bound line 602
Source documentation
The degree-series estimate in the common-mass argument, with no asymptotic notation.
```
theorem degree_series_bound (a : ℝ) (N : ℕ) :
    (∑ r ∈ Finset.range N, a^r / (Real.sqrt (r:ℝ))^r)^2 ≤
      2 * Real.exp (2*a^2) := by
…
```