OAI/Analysis/Littlewood/BlockSampling.lean

GitHub source file

14 declarations, 0 contain sorry, 0 declared as axioms

1. theorem OAI.AsymptoticallyMinimalLittlewood.Cutoff.block_cutoffs line 12
2. lemma OAI.AsymptoticallyMinimalLittlewood.Cutoff.block_support_unit line 43
3. lemma OAI.AsymptoticallyMinimalLittlewood.Cutoff.blocks_disjoint line 54
4. lemma OAI.AsymptoticallyMinimalLittlewood.Packing.circle_int_zero line 80
5. lemma OAI.AsymptoticallyMinimalLittlewood.Packing.center_mem_interval line 83
6. lemma OAI.AsymptoticallyMinimalLittlewood.Packing.disjoint_centers_noninteger line 86
7. lemma OAI.AsymptoticallyMinimalLittlewood.Packing.block_center_distance line 95
8. lemma OAI.AsymptoticallyMinimalLittlewood.Packing.stationary_in_interval line 104
9. lemma OAI.AsymptoticallyMinimalLittlewood.Packing.stationary_unique line 121
10. lemma OAI.AsymptoticallyMinimalLittlewood.Sampling.mFourier_lift line 161
11. lemma OAI.AsymptoticallyMinimalLittlewood.Sampling.mFourier_chirp line 174
12. lemma OAI.AsymptoticallyMinimalLittlewood.Sampling.signed_fourier_sum line 195
13. lemma OAI.AsymptoticallyMinimalLittlewood.Sampling.block_value_bound line 204

    Source documentation

    Disjointly supported block values preserve the [-1,1] constraint.

    lemma block_value_bound {H : ℕ} (χ : Fin H → ℝ) (F : Fin H → ℂ)
        (hχ : ∀ h, 0≤χ h ∧ χ h≤1) (hF : ∀ h, ‖F h‖≤1)
        (hdisj : ∀ i j, i≠j → χ i*χ j=0) :
        ‖∑ h, (χ h : ℂ)*F h‖≤1 := by
    …

14. theorem OAI.AsymptoticallyMinimalLittlewood.Sampling.sample_packed line 231

    Source documentation

    Exact fixed-block sampler for a packed real trigonometric polynomial.

    theorem sample_packed {I J : Type} [Fintype I] [Fintype J]
        (a : I → J → ℤ) (c : I → ℂ) (v : J → ℝ) {H : ℕ} (hH : 1≤H)
        (θ : Fin H → J → ℝ)
        (hreal : ∀ y : J → UnitAddCircle, (∑ i, c i*mFourier (a i) y).im=0)
        (hbound : ∀ y : J → UnitAddCircle, ‖∑ i, c i*mFourier (a i) y‖≤1)
        (hlam : ∀ i, (∑ j, (a i j : ℝ)*v j)≠0)
        (hwidth : ∀ i, |∑ j, (a i j : ℝ)*v j|/(H : ℝ)<1)
        (hpack : ∀ h h' : Fin H, ∀ i i' : I, (h,i)≠(h',i') →
          Disjoint (circleInterval (((∑ j, (a i j : ℝ)*θ h j : ℝ)) : UnitAddCircle)
            (|∑ j, (a i j : ℝ)*v j|/H))
          (circleInterval (((∑ j, (a i' j : ℝ)*θ h' j : ℝ)) : UnitAddCircle)
            (|∑ j, (a i' j : ℝ)*v j|/H)))
    …