OAI/Analysis/Littlewood/ModeSampling.lean

GitHub source file

13 declarations, 0 contain sorry, 0 declared as axioms

1. lemma OAI.AsymptoticallyMinimalLittlewood.Sampling.realPhase_mul_conj line 12
2. lemma OAI.AsymptoticallyMinimalLittlewood.Sampling.realPhase_zero line 19
3. def OAI.AsymptoticallyMinimalLittlewood.Sampling.modeSum line 21
4. lemma OAI.AsymptoticallyMinimalLittlewood.Sampling.norm_sq_modeSum line 25
5. lemma OAI.AsymptoticallyMinimalLittlewood.Sampling.amplitude_pair_compact line 57
6. lemma OAI.AsymptoticallyMinimalLittlewood.Sampling.amplitude_pair_smooth line 60
7. lemma OAI.AsymptoticallyMinimalLittlewood.Sampling.amplitude_pair_support line 64
8. lemma OAI.AsymptoticallyMinimalLittlewood.Sampling.diagonal_integral line 68
9. theorem OAI.AsymptoticallyMinimalLittlewood.Sampling.mode_energy line 75

   Source documentation

   Fixed-data mean square sampling, including the equal-curvature case. Separated blocks may be handled by the zero-product alternative.

   theorem mode_energy {P : Type uP} [Fintype P] (g : P → ℝ → ℂ) (c : P → ℂ)
       (lam b d : P → ℝ) (hgc : ∀ i, HasCompactSupport (g i))
       (hgs : ∀ i, ContDiff ℝ ∞ (g i)) (hgi : ∀ i, tsupport (g i)⊆Set.Ioo (0:ℝ) 1)
       (hgb : ∀ i x, ‖g i x‖≤1)
       (hfreq : ∀ i j, i≠j → (lam i≠lam j ∨ ∀ l : ℤ, (l : ℝ)≠b i-b j) ∨
         ∀ x, g i x*conj (g j x)=0) :
       Tendsto (fun N : ℕ ↦ (∑ k : Fin N, ‖modeSum g c lam b d N k‖^2)/(N : ℝ))
         atTop (𝓝 (∑ i, ‖c i‖^2*(∫ x : ℝ, ‖g i x‖^2))) := by
   …

   Mentions: OAI.AsymptoticallyMinimalLittlewood.Sampling.modeSum

10. lemma OAI.AsymptoticallyMinimalLittlewood.Sampling.norm_sum_sparse line 135
11. lemma OAI.AsymptoticallyMinimalLittlewood.Sampling.phase_modulate line 150
12. lemma OAI.AsymptoticallyMinimalLittlewood.Sampling.mode_modulate line 157
13. theorem OAI.AsymptoticallyMinimalLittlewood.Sampling.mode_maximum line 175

    Source documentation

    The fixed-data uniform circle estimate; the sparse-stationary hypothesis will be discharged by the signed interval packing.

    theorem mode_maximum {P : Type uP} [Fintype P] (g : P → ℝ → ℂ) (c : P → ℂ)
        (lam b d : P → ℝ) (hgc : ∀ i, HasCompactSupport (g i))
        (hgs : ∀ i, ContDiff ℝ ∞ (g i)) (hgi : ∀ i, tsupport (g i)⊆Set.Ioo (0:ℝ) 1)
        (hgb : ∀ i x, ‖g i x‖≤1) (hlam : ∀ i, lam i≠0)
        {K : ℝ} (hK : 0≤K) (hc : ∀ i, ‖c i‖/Real.sqrt |lam i|≤K)
        (hsparse : ∀ t : ℝ, ∀ i j : P, ∀ l m : ℤ,
          g i (((l : ℝ)-(b i+t))/lam i)≠0 → g j (((m : ℝ)-(b j+t))/lam j)≠0 →
          i=j ∧ l=m) :
        ∃ C : ℝ, 0≤C ∧ ∀ N : ℕ, 1≤N → ∀ t∈Set.Icc (0:ℝ) 1,
          ‖(1/(Real.sqrt N : ℂ))*∑ k : Fin N,
            modeSum g c lam b d N k*realPhase (2*Real.pi*t*k)‖≤K+C/N := by
    …

    Mentions: OAI.AsymptoticallyMinimalLittlewood.Sampling.modeSum, OAI.AsymptoticallyMinimalLittlewood.realPhase