OAI/Analysis/Littlewood/SamplingTail.lean

GitHub source file

15 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.AsymptoticallyMinimalLittlewood.Sampling.latticeWeight line 11
2. lemma OAI.AsymptoticallyMinimalLittlewood.Sampling.latticeWeight_pos line 13
3. lemma OAI.AsymptoticallyMinimalLittlewood.Sampling.latticeWeight_summable line 17
4. def OAI.AsymptoticallyMinimalLittlewood.Sampling.sampledChirp line 30
5. lemma OAI.AsymptoticallyMinimalLittlewood.Sampling.sampledChirp_compact line 33
6. lemma OAI.AsymptoticallyMinimalLittlewood.Sampling.sampledChirp_smooth line 39
7. lemma OAI.AsymptoticallyMinimalLittlewood.Sampling.sampledChirp_fourier line 43
8. lemma OAI.AsymptoticallyMinimalLittlewood.Sampling.poisson_chirp line 61
9. lemma OAI.AsymptoticallyMinimalLittlewood.Sampling.poisson_tail_bound line 76
10. def OAI.AsymptoticallyMinimalLittlewood.Sampling.stationaryWave line 111
11. lemma OAI.AsymptoticallyMinimalLittlewood.Sampling.stationaryWave_norm line 115
12. lemma OAI.AsymptoticallyMinimalLittlewood.Sampling.normalized_integral_error line 121
13. lemma OAI.AsymptoticallyMinimalLittlewood.Sampling.stationaryWave_zero line 152
14. lemma OAI.AsymptoticallyMinimalLittlewood.Sampling.int_abs_large_of_not_mem line 167
15. theorem OAI.AsymptoticallyMinimalLittlewood.Sampling.uniform_poisson_chirp line 179

    Source documentation

    The exact fixed-data sampling estimate, centered at zero; a nonzero center is obtained by shifting the linear frequency and a unit scalar phase.

    theorem uniform_poisson_chirp {g : ℝ → ℂ} (hg : HasCompactSupport g)
        (hgs : ContDiff ℝ ∞ g) {A B β : ℝ} (hA : 0≤A) (hB : 0≤B)
        (hsupp : tsupport g⊆Set.Icc (-A) A) (hβ : β≠0) :
        ∃ J : Finset ℤ, ∃ C : ℝ, 0≤C ∧ ∀ N b : ℝ, 1≤N → |b|≤B →
          (∀ l∉J, stationaryWave g N β b l=0) ∧
          ‖(1/(Real.sqrt N : ℂ))*(∑' k : ℤ, g ((k : ℝ)/N)*phase (β/N) (-b) k)-
            ∑ l∈J, stationaryWave g N β b l‖≤C/N := by
    …

    Mentions: OAI.AsymptoticallyMinimalLittlewood.Sampling.stationaryWave