OAI/NumberTheory/JointDickman/Counting/SamplingComparisonLimit.lean

GitHub source file

1 declarations, 0 contain sorry, 0 declared as axioms

1. theorem OAI.JointDickman.samplingComparison_eventually line 14

   Source documentation

   The manuscript's sampling transfer, uniformly over the finite site spaces and all kernels satisfying its moment and fixed-test estimates. No conditional second-moment bound at each row type is required.

   theorem samplingComparison_eventually {C q c U e ε : ℝ}
       (hC : 0 ≤ C) (hq : 0 ≤ q) (hc : 0 < c) (hU : 0 ≤ U)
       (he : 0 ≤ e) (hε : 0 < ε) :
       ∀ᶠ B : ℝ in atTop,
       ∀ (ι A : Type*) [Fintype ι] [DecidableEq ι] [Nonempty ι] [Fintype A] [DecidableEq A],
       FiniteMcDiarmidInput ι A →
       ∀ (p : ι → A → ℝ), (∀ i b, 0 ≤ p i b) → (∀ i, ∑ b, p i b = 1) →
       ∀ (E H : ι → ι → A → A → ℝ),
       (∀ i j b z, E i j b z = E j i z b) →
       (∀ i j b z, H i j b z = H j i z b) →
       (∀ i b, E i i b b = 0) → (∀ i b, H i i b b = 0) →
       (∀ i j b z, |E i j b z| ≤ H i j b z) →
   …