OAI/NumberTheory/Ostmann/Characters/SparseFiniteContraction.lean

GitHub source file

2 declarations, 0 contain sorry, 0 declared as axioms

1. theorem OAI.Ostmann.sparse_normalizer_error_bounds line 11
2. theorem OAI.Ostmann.sparse_finite_contraction line 46

   Source documentation

   The concrete finite output used by Proposition 5.1: the nonnegative weight keeps a positive unit mean while its pair kernel contracts.

   theorem sparse_finite_contraction {n : ℕ}
       (p : Fin n → ℕ) [∀ i, Fact (p i).Prime]
       (S : ∀ i, Finset (ZMod (p i)))
       (hS : ∀ i, (S i).Nonempty) (hSp : ∀ i, (S i).card < p i)
       (hp : ∀ i, (100 : ℝ) ≤ p i)
       (hlo : ∀ i, (1 / 3 : ℝ) ≤ residueDensity (S i))
       (hhi : ∀ i, residueDensity (S i) ≤ 2 / 3)
       (ε : ℝ) (hε : 0 ≤ ε) (hεsmall : ε ≤ 1 / 1000000)
       (hL1 : ∀ i, (p i : ℝ)⁻¹ * ∑ b, ‖normalizedResidueTransform (S i) b‖ ≤ ε ^ 2)
       (L : ℝ) (hL : 1 ≤ L) (hH : (∑ i, (p i : ℝ)⁻¹) ≤ L)
       (K : ℕ) (hK : 1000 * L ≤ K) :
       let U := ∏ i, sparseKernelUnitFactor (p i)
   …

   Mentions: OAI.Ostmann.residueDensity, OAI.Ostmann.normalizedResidueTransform, OAI.Ostmann.sparseKernelUnitFactor