OAI/Analysis/Littlewood/QuadraticTail.lean

GitHub source file

37 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.AsymptoticallyMinimalLittlewood.QuadraticTail.phase line 13
2. def OAI.AsymptoticallyMinimalLittlewood.QuadraticTail.amp line 16
3. def OAI.AsymptoticallyMinimalLittlewood.QuadraticTail.osc line 19
4. lemma OAI.AsymptoticallyMinimalLittlewood.QuadraticTail.phase_norm line 22
5. lemma OAI.AsymptoticallyMinimalLittlewood.QuadraticTail.phase_smooth line 27
6. lemma OAI.AsymptoticallyMinimalLittlewood.QuadraticTail.phase_deriv line 32
7. lemma OAI.AsymptoticallyMinimalLittlewood.QuadraticTail.amp_smooth line 45
8. lemma OAI.AsymptoticallyMinimalLittlewood.QuadraticTail.amp_support line 61
9. lemma OAI.AsymptoticallyMinimalLittlewood.QuadraticTail.amp_compact line 70
10. lemma OAI.AsymptoticallyMinimalLittlewood.QuadraticTail.amp_deriv line 74
11. lemma OAI.AsymptoticallyMinimalLittlewood.QuadraticTail.osc_integrable line 100
12. lemma OAI.AsymptoticallyMinimalLittlewood.QuadraticTail.osc_parts line 106
13. lemma OAI.AsymptoticallyMinimalLittlewood.QuadraticTail.osc_bound_zero line 149
14. theorem OAI.AsymptoticallyMinimalLittlewood.QuadraticTail.polynomial_decay line 178

    Source documentation

    Uniform repeated nonstationary integration by parts, with the support condition on the actual amplitude. The parameters may vary, but c and B stay fixed.

    theorem polynomial_decay (l : ℕ) (c B : ℝ) (hc : 0 < c) (hB : 0 ≤ B) :
        ∀ (g : ℝ → ℂ), HasCompactSupport g → ContDiff ℝ ∞ g → ∀ k : ℕ,
        ∃ C : ℝ, 0 ≤ C ∧ ∀ (t u M : ℝ), 0 < M → |t| ≤ B*M →
          (∀ x ∈ tsupport g, c*M ≤ |t*x-u|) → M^(k+l)*‖osc g t u k‖ ≤ C := by
    …

    Mentions: OAI.AsymptoticallyMinimalLittlewood.QuadraticTail.osc

15. theorem OAI.AsymptoticallyMinimalLittlewood.QuadraticTail.offbox_decay line 232

    Source documentation

    Off-box decay in precisely the regime used to truncate the spread spectrum.

    theorem offbox_decay {g : ℝ → ℂ} (hg : HasCompactSupport g) (hgs : ContDiff ℝ ∞ g)
        {α β : ℝ} (hα : 0 ≤ α) (hα' : α < 1/2) (hβ : β ≠ 0)
        (hsupp : tsupport g ⊆ Set.Icc (-α) α) (l : ℕ) :
        ∃ C : ℝ, 0 ≤ C ∧ ∀ T w : ℝ, 0 < T → T*|β|/2 < |w| →
          (T+|w|)^l * ‖∫ x : ℝ, g x*phase (T*β) w x‖ ≤ C := by
    …

    Mentions: OAI.AsymptoticallyMinimalLittlewood.QuadraticTail.phase

16. lemma OAI.AsymptoticallyMinimalLittlewood.QuadraticTail.phase_fourier line 269
17. lemma OAI.AsymptoticallyMinimalLittlewood.QuadraticTail.cutoff_zero line 276
18. def OAI.AsymptoticallyMinimalLittlewood.QuadraticTail.circleChirp line 280
19. lemma OAI.AsymptoticallyMinimalLittlewood.QuadraticTail.circleChirp_continuous line 283
20. lemma OAI.AsymptoticallyMinimalLittlewood.QuadraticTail.circleChirp_coefficient line 292
21. def OAI.AsymptoticallyMinimalLittlewood.QuadraticTail.latticeWeight line 316
22. lemma OAI.AsymptoticallyMinimalLittlewood.QuadraticTail.latticeWeight_pos line 318
23. lemma OAI.AsymptoticallyMinimalLittlewood.QuadraticTail.latticeWeight_summable line 322
24. def OAI.AsymptoticallyMinimalLittlewood.QuadraticTail.box line 335
25. lemma OAI.AsymptoticallyMinimalLittlewood.QuadraticTail.mem_box line 338
26. lemma OAI.AsymptoticallyMinimalLittlewood.QuadraticTail.box_card_le line 342
27. theorem OAI.AsymptoticallyMinimalLittlewood.QuadraticTail.offbox_weighted line 356

    Source documentation

    A summable majorant for the discarded one-dimensional Fourier tail. This uses three integrations by parts (or n+2 for the stronger form), and avoids an unjustified summation of stationary-phase errors.

    theorem offbox_weighted {g : ℝ → ℂ} (hg : HasCompactSupport g)
        (hgs : ContDiff ℝ ∞ g) {α : ℝ} (hα0 : 0≤α) (hα : α<1/2)
        (hs : tsupport g ⊆ Set.Icc (-α) α) {β : ℝ} (hβ : β ≠ 0) (n : ℕ) :
        ∃ C : ℝ, 0≤C ∧ ∀ T : ℝ, 1≤T → ∀ w : ℤ, w ∉ box T β →
          ‖∫ x : ℝ, g x*phase (T*β) w x‖ ≤ C / T^n * latticeWeight w := by
    …

    Mentions: OAI.AsymptoticallyMinimalLittlewood.QuadraticTail.box, OAI.AsymptoticallyMinimalLittlewood.QuadraticTail.phase, OAI.AsymptoticallyMinimalLittlewood.QuadraticTail.latticeWeight

28. lemma OAI.AsymptoticallyMinimalLittlewood.QuadraticTail.circle_fourier_norm line 381
29. lemma OAI.AsymptoticallyMinimalLittlewood.QuadraticTail.fourier_truncation_error line 385

    Source documentation

    Uniform truncation from a summable majorant outside one finite box.

    lemma fourier_truncation_error (f : C(UnitAddCircle,ℂ)) (S : Finset ℤ)
        (b : ℤ → ℝ) (hb : Summable b) (hb0 : ∀ w, 0≤b w)
        (hbound : ∀ w, w ∉ S → ‖fourierCoeff f w‖ ≤ b w) (z : UnitAddCircle) :
        ‖(∑ w ∈ S, fourierCoeff f w*fourier w z)-f z‖ ≤ ∑' w, b w := by
    …

30. def OAI.AsymptoticallyMinimalLittlewood.QuadraticTail.rowTrunc line 416
31. theorem OAI.AsymptoticallyMinimalLittlewood.QuadraticTail.rowTrunc_error line 419
32. lemma OAI.AsymptoticallyMinimalLittlewood.QuadraticTail.circleChirp_norm line 439
33. lemma OAI.AsymptoticallyMinimalLittlewood.QuadraticTail.circleChirp_mass line 445
34. lemma OAI.AsymptoticallyMinimalLittlewood.QuadraticTail.circle_parseval line 467
35. lemma OAI.AsymptoticallyMinimalLittlewood.QuadraticTail.coefficient_norm_le_one line 477
36. theorem OAI.AsymptoticallyMinimalLittlewood.QuadraticTail.row_mass_error line 494

    Source documentation

    Retained squared Fourier mass loses only O(1/T), uniformly in the quadratic modulation. This is the scalar Parseval ingredient for spreading.

    theorem row_mass_error {g : ℝ → ℂ} (hg : HasCompactSupport g)
        (hgs : ContDiff ℝ ∞ g) (hg1 : ∀ x, ‖g x‖≤1) {α : ℝ}
        (hα0 : 0≤α) (hα : α<1/2) (hs : tsupport g ⊆ Set.Icc (-α) α)
        {β : ℝ} (hβ : β ≠ 0) :
        ∃ C : ℝ, 0≤C ∧ ∀ T : ℝ, 1≤T →
          (∫ x : ℝ, ‖g x‖^2) - C/T ≤
            ∑ w ∈ box T β, ‖∫ x : ℝ, g x*phase (T*β) w x‖^2 := by
    …

    Mentions: OAI.AsymptoticallyMinimalLittlewood.QuadraticTail.box, OAI.AsymptoticallyMinimalLittlewood.QuadraticTail.phase

37. lemma OAI.AsymptoticallyMinimalLittlewood.QuadraticTail.finite_product_error line 542

    Source documentation

    Tensoring finitely many uniformly bounded approximations preserves a uniform O(1/T) error; both target functions may depend on T.

    lemma finite_product_error {I : Type uI} {Z : Type uZ} (S : Finset I)
        (f h : I → ℝ → Z → ℂ)
        (hh : ∀ i ∈ S, ∀ T z, ‖h i T z‖≤1)
        (hf : ∀ i ∈ S, ∃ C : ℝ, 0≤C ∧ ∀ T, 1≤T → ∀ z, ‖f i T z-h i T z‖≤C/T) :
        ∃ C : ℝ, 0≤C ∧ ∀ T, 1≤T → ∀ z,
          ‖(∏ i ∈ S, f i T z)-(∏ i ∈ S, h i T z)‖ ≤ C/T := by
    …