SparseResidueProjection.lean`

1 declarations, 0 contain sorry, 0 declared as axioms

Sparse projection of the actual normalized residue indicator

theorem OAI.Ostmann.sparse_residue_projection line 13

Source documentation

The projection chosen in (5.7) kills constants and loses at most epsilon squared of the normalized residue indicator's energy.

theorem sparse_residue_projection {p : ℕ} [Fact p.Prime]
    (S : Finset (ZMod p)) (hS : S.Nonempty) (hSp : S.card < p)
    (ε : ℝ) (hε : 0 ≤ ε) (hε1 : ε ≤ 1)
    (hL1 : (p : ℝ)⁻¹ * ∑ b, ‖normalizedResidueTransform S b‖ ≤ ε ^ 2) :
    let E := largeTransformSpectrum (normalizedResidueTransform S)
…

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