SparseTransformSpectrum.lean`

5 declarations, 0 contain sorry, 0 declared as axioms

Concentration of a small-L1 normalized additive transform

This is the finite argument (5.7), before the contracting kernel in Proposition 5.1. It requires no analytic input.

def OAI.Ostmann.largeTransformSpectrum line 14
theorem OAI.Ostmann.largeTransformSpectrum_zero_not_mem line 17
theorem OAI.Ostmann.largeTransformSpectrum_neg line 21

theorem OAI.Ostmann.largeTransformSpectrum_bounds line 28

Source documentation

The large coefficients occupy a small set and retain almost all energy.

theorem largeTransformSpectrum_bounds {p : ℕ} [NeZero p]
    (g : ZMod p → ℂ) (δ : ℝ)
    (hL1 : (∑ b, ‖g b‖) ≤ δ * p) (hL2 : (∑ b, ‖g b‖ ^ 2) = p) :
    ((largeTransformSpectrum g).card : ℝ) ≤ δ * p ∧
      (1 - δ) * p ≤ ∑ b ∈ largeTransformSpectrum g, ‖g b‖ ^ 2 := by
…

Mentions: OAI.Ostmann.largeTransformSpectrum

theorem OAI.Ostmann.normalizedResidueTransform_sparse line 62

Source documentation

The exact normalized residue transform satisfies the sparse-spectrum conclusions used in Section 5 whenever its probability L1 norm is small.

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

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