OAI/NumberTheory/Ostmann/Supply/LocalSparseKernelContraction.lean

GitHub source file

1 declarations, 0 contain sorry, 0 declared as axioms

The contracting local sparse block at (u,v)=(1,1)

  1. theorem OAI.Ostmann.local_sparse_kernel_contraction line 15

    Source documentation

    The finite local contraction in Lemma 5.2, with the actual sparse spectrum, actual residue vectors, and the exact nonzero-residue normalizing factor.

    theorem local_sparse_kernel_contraction {p : ℕ} [Fact p.Prime]
    (S : Finset (ZMod p)) (hS : S.Nonempty) (hSp : S.card < p)
    (hp : (100 : ℝ) ≤ p)
    (hlo : (1 / 3 : ℝ) ≤ residueDensity S) (hhi : residueDensity S ≤ 2 / 3)
    (ε : ℝ) (hε : 0 ≤ ε) (hεsmall : ε ≤ 1 / 1000000)
    (hL1 : (p : ℝ)⁻¹ * ∑ b, ‖normalizedResidueTransform S b‖ ≤ ε ^ 2) :
    let E := largeTransformSpectrum (normalizedResidueTransform S)
…

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