OAI/Analysis/Littlewood/SamplingEnergy.lean

GitHub source file

15 declarations, 0 contain sorry, 0 declared as axioms

1. theorem OAI.AsymptoticallyMinimalLittlewood.Sampling.curved_average_zero line 12

   Source documentation

   The off-diagonal average with nonzero curvature, used in the sampled energy calculation. The amplitude bound is later applied to the squared cutoff.

   theorem curved_average_zero {g : ℝ → ℂ} (hg : HasCompactSupport g)
       (hgs : ContDiff ℝ ∞ g) {A D β : ℝ} (hA : 0≤A) (hD : 0≤D)
       (hsupp : tsupport g⊆Set.Icc (-A) A) (hbound : ∀ x, ‖g x‖≤D)
       (hβ : β≠0) (b : ℝ) :
       Tendsto (fun N : ℕ ↦ ‖(1/(N : ℂ))*(∑' k : ℤ,
         g ((k : ℝ)/N)*phase (β/N) (-b) k)‖) atTop (𝓝 0) := by
   …

2. theorem OAI.AsymptoticallyMinimalLittlewood.Sampling.linear_integral_decay line 55

   Source documentation

   The linear (equal-curvature) case of the same off-diagonal calculation.

   theorem linear_integral_decay {g : ℝ → ℂ} (hg : HasCompactSupport g)
       (hgs : ContDiff ℝ ∞ g) {b : ℝ} {l : ℤ} (hl : (l : ℝ)≠b) :
       ∃ C : ℝ, 0≤C ∧ ∀ N : ℝ, 0<N →
         N^2*‖∫ x : ℝ, g x*phase 0 (N*((l : ℝ)-b)) x‖≤C := by
   …

3. theorem OAI.AsymptoticallyMinimalLittlewood.Sampling.linear_average_error line 72

   Source documentation

   Averaged Poisson summation after removing a finite resonant set. This single estimate handles both the diagonal Riemann sum and equal-curvature cross terms without any uniformity in the packing data.

   theorem linear_average_error {g : ℝ → ℂ} (hg : HasCompactSupport g)
       (hgs : ContDiff ℝ ∞ g) {A : ℝ} (hA : 0≤A)
       (hsupp : tsupport g⊆Set.Icc (-A) A) (b : ℝ) (S : Finset ℤ)
       (hres : ∀ l∉S, (l : ℝ)≠b) :
       ∃ C : ℝ, 0≤C ∧ ∀ N : ℝ, 0<N →
         ‖(1/(N : ℂ))*(∑' k : ℤ, g ((k : ℝ)/N)*phase 0 (-b) k)-
           ∑ l∈S, ∫ x : ℝ, g x*phase 0 (N*((l : ℝ)-b)) x‖≤C/N^2 := by
   …

4. lemma OAI.AsymptoticallyMinimalLittlewood.Sampling.linear_average_zero line 136
5. lemma OAI.AsymptoticallyMinimalLittlewood.Sampling.phase_zero line 153
6. lemma OAI.AsymptoticallyMinimalLittlewood.Sampling.unphased_average line 155
7. lemma OAI.AsymptoticallyMinimalLittlewood.Sampling.tsum_eq_sum_fin line 174
8. lemma OAI.AsymptoticallyMinimalLittlewood.Sampling.sampled_support_zero line 195
9. def OAI.AsymptoticallyMinimalLittlewood.Sampling.finiteAverage line 210
10. lemma OAI.AsymptoticallyMinimalLittlewood.Sampling.finiteAverage_eq line 213
11. lemma OAI.AsymptoticallyMinimalLittlewood.Sampling.finiteAverage_zero line 219
12. lemma OAI.AsymptoticallyMinimalLittlewood.Sampling.finiteAverage_diagonal line 237
13. lemma OAI.AsymptoticallyMinimalLittlewood.Sampling.phase_mul line 247
14. lemma OAI.AsymptoticallyMinimalLittlewood.Sampling.phase_conj line 253
15. lemma OAI.AsymptoticallyMinimalLittlewood.Sampling.phase_mul_conj line 260