OAI/Dynamics/ThreeTorus/StationaryPhase.lean

GitHub source file

76 declarations, 0 contain sorry, 0 declared as axioms

Uniform signed stationary phase, oscillatory integral estimates, and summed coefficient-mass control.

  1. lemma OAI.ThreeTorus.quadratic_gaussian_pairing line 14
  2. lemma OAI.ThreeTorus.norm_quadratic_exp_le_one line 38
  3. lemma OAI.ThreeTorus.quadratic_boundary_pairing line 50

    Source documentation

    The Gaussian identity extends to the imaginary boundary after pairing with an integrable Schwartz amplitude. This uses dominated convergence, never a non-absolutely convergent Bochner integral for a bare Fresnel kernel.

    lemma quadratic_boundary_pairing (f : 𝓒(ℝ, β„‚)) {b : β„‚}
    (hb : 0 ≀ b.re) (hbslit : b ∈ Complex.slitPlane) :
    (∫ x : ℝ, f x * Complex.exp (-Real.pi * b * x ^ 2)) =
      (1 / b ^ (1 / 2 : β„‚)) * (∫ ΞΎ : ℝ, (𝓕⁻ f) ΞΎ *
        Complex.exp (-Real.pi / b * ΞΎ ^ 2)) := by
…
  4. lemma OAI.ThreeTorus.cpow_pos_mul line 103
  5. lemma OAI.ThreeTorus.quadratic_factor line 110
  6. lemma OAI.ThreeTorus.integral_fourierInv line 123
  7. lemma OAI.ThreeTorus.quadratic_stationary_identity line 128
  8. lemma OAI.ThreeTorus.quadratic_stationary_error line 155
  9. lemma OAI.ThreeTorus.quadratic_stationary_limit line 195
  10. lemma OAI.ThreeTorus.quadratic_stationary_uniform line 209
  11. lemma OAI.ThreeTorus.quadratic_stationary_compact line 224
  12. lemma OAI.ThreeTorus.continuous_stationary_constant line 231
  13. lemma OAI.ThreeTorus.quadratic_stationary_uniform_compact line 244
  14. lemma OAI.ThreeTorus.quadratic_stationary_limit_neg line 256
  15. lemma OAI.ThreeTorus.quadratic_stationary_compact_neg line 279
  16. lemma OAI.ThreeTorus.oscillatory_integral_parts line 286
  17. lemma OAI.ThreeTorus.oscillatory_integral_bound line 320
  18. lemma OAI.ThreeTorus.reciprocal_variation line 350
  19. lemma OAI.ThreeTorus.nonstationary_monotone_bound line 386
  20. lemma OAI.ThreeTorus.cubic_taylor_estimate line 478
  21. lemma OAI.ThreeTorus.norm_exp_imag_sub_le line 505
  22. lemma OAI.ThreeTorus.local_stationary_comparison line 516
  23. lemma OAI.ThreeTorus.derivative_coercive line 582
  24. lemma OAI.ThreeTorus.normalized_phase_tail line 601
  25. lemma OAI.ThreeTorus.quadratic_phase_deriv line 636
  26. lemma OAI.ThreeTorus.quadratic_phase_second line 640
  27. lemma OAI.ThreeTorus.interval_three_parts line 645
  28. lemma OAI.ThreeTorus.stationary_interval_comparison line 651
  29. lemma OAI.ThreeTorus.stationary_interval_scaled_comparison line 719
  30. lemma OAI.ThreeTorus.stationary_interval_comparison_uniform line 744
  31. lemma OAI.ThreeTorus.quadratic_phase_third line 784
  32. lemma OAI.ThreeTorus.quadratic_interval_limit line 789
  33. lemma OAI.ThreeTorus.stationary_normalized_uniform line 844
  34. lemma OAI.ThreeTorus.uniform_rescale line 895
  35. lemma OAI.ThreeTorus.stationary_positive_uniform line 921
  36. lemma OAI.ThreeTorus.stationary_positive_error_uniform line 972
  37. lemma OAI.ThreeTorus.deriv_conj_real line 1031
  38. lemma OAI.ThreeTorus.intervalIntegral_conj line 1036
  39. lemma OAI.ThreeTorus.stationary_negative_error_uniform line 1040
  40. lemma OAI.ThreeTorus.nonstationary_scaled_uniform line 1085
  41. lemma OAI.ThreeTorus.derivative_coercive_center line 1132
  42. lemma OAI.ThreeTorus.stationary_positive_moving_uniform line 1150
  43. lemma OAI.ThreeTorus.stationary_negative_moving_uniform line 1233
  44. lemma OAI.ThreeTorus.stationary_positive_moving_of_bounds line 1280

    Source documentation

    Uniform stationary phase with ordinary lower and upper curvature bounds.

    lemma stationary_positive_moving_of_bounds {Ξ± : Type*} {Ο† : Ξ± β†’ ℝ β†’ ℝ} {A : Ξ± β†’ ℝ β†’ β„‚}
    {v : Ξ± β†’ ℝ} (hΟ† : βˆ€ a, ContDiff ℝ 3 (Ο† a)) (hA : βˆ€ a, ContDiff ℝ 2 (A a))
    {l u R d D Cβ‚€ C₁ M : ℝ} (hR : 0 < R) (hd : 0 < d) (hdD : d ≀ D)
    (hCβ‚€ : 0 ≀ Cβ‚€) (hC₁ : 0 ≀ C₁) (hMβ‚€ : 0 ≀ M)
    (hv : βˆ€ a, l+R ≀ v a ∧ v a ≀ u-R)
    (hcrit : βˆ€ a, deriv (Ο† a) (v a) = 0)
    (hsecond : βˆ€ a x, x ∈ Icc l u β†’ d ≀ iteratedDeriv 2 (Ο† a) x)
    (hupper : βˆ€ a x, x ∈ Icc l u β†’ iteratedDeriv 2 (Ο† a) x ≀ D)
    (hM : βˆ€ a x, x ∈ Icc l u β†’ |iteratedDeriv 3 (Ο† a) x| ≀ M)
    (hAb : βˆ€ a x, x ∈ Icc l u β†’ β€–A a xβ€– ≀ Cβ‚€)
    (hA'b : βˆ€ a x, x ∈ Icc l u β†’ β€–deriv (A a) xβ€– ≀ C₁) :
    TendstoUniformly (fun t : ℝ => fun a => (Real.sqrt t : β„‚) *
…
  45. lemma OAI.ThreeTorus.deriv_sub_linear_phase line 1324
  46. lemma OAI.ThreeTorus.iteratedDeriv_sub_linear_phase line 1329
  47. def OAI.ThreeTorus.stationaryLeading line 1340

    Source documentation

    Actual stationary leading term: zero outside the derivative branch.

    def stationaryLeading (Ξ¦ : ℝ β†’ ℝ) (A : ℝ β†’ β„‚) (l u s t : ℝ) : β„‚ :=
…
  48. lemma OAI.ThreeTorus.stationary_branch_center line 1348
  49. lemma OAI.ThreeTorus.intervalIntegral_phase_of_support line 1355
  50. lemma OAI.ThreeTorus.phase_nonstationary_off_branch line 1364
  51. lemma OAI.ThreeTorus.phase_stationary_on_branch line 1420
  52. lemma OAI.ThreeTorus.compact_support_stationary_uniform line 1467

    Source documentation

    Compactly supported, parameter-uniform stationary phase, including the noncritical region and zero amplitudes. No weak-convergence replacement is used.

    lemma compact_support_stationary_uniform {Ξ± : Type*} {Ξ¦ : ℝ β†’ ℝ} {A : Ξ± β†’ ℝ β†’ β„‚}
    (hΞ¦ : ContDiff ℝ 3 Ξ¦) (hA : βˆ€ a, ContDiff ℝ 2 (A a))
    {a b R d D Cβ‚€ C₁ M : ℝ} (hab : a ≀ b) (hR : 0 < R) (hd : 0 < d) (hdD : d ≀ D)
    (hCβ‚€ : 0 ≀ Cβ‚€) (hC₁ : 0 ≀ C₁) (hMβ‚€ : 0 ≀ M)
    (hsecond : βˆ€ x ∈ Icc (a-2*R) (b+2*R), d ≀ iteratedDeriv 2 Ξ¦ x)
    (hupper : βˆ€ x ∈ Icc (a-2*R) (b+2*R), iteratedDeriv 2 Ξ¦ x ≀ D)
    (hM : βˆ€ x ∈ Icc (a-2*R) (b+2*R), |iteratedDeriv 3 Ξ¦ x| ≀ M)
    (hAb : βˆ€ z x, x ∈ Icc (a-2*R) (b+2*R) β†’ β€–A z xβ€– ≀ Cβ‚€)
    (hA'b : βˆ€ z x, x ∈ Icc (a-2*R) (b+2*R) β†’ β€–deriv (A z) xβ€– ≀ C₁)
    (hsupp : βˆ€ z, Function.support (A z) βŠ† Ioc a b) :
    TendstoUniformly (fun t : ℝ => fun p : Ξ± Γ— ℝ =>
      (Real.sqrt t : β„‚) * (∫ x, A p.1 x * Complex.exp (I * (t*(Ξ¦ x-p.2*x) : ℝ))) -
…
  53. lemma OAI.ThreeTorus.compact_support_stationary_negative_uniform line 1494

    Source documentation

    Negative curvature follows by conjugation, with the same unaltered phase.

    lemma compact_support_stationary_negative_uniform {Ξ± : Type*} {Ξ¦ : ℝ β†’ ℝ} {A : Ξ± β†’ ℝ β†’ β„‚}
    (hΞ¦ : ContDiff ℝ 3 Ξ¦) (hA : βˆ€ a, ContDiff ℝ 2 (A a))
    {a b R d D Cβ‚€ C₁ M : ℝ} (hab : a ≀ b) (hR : 0 < R) (hd : 0 < d) (hdD : d ≀ D)
    (hCβ‚€ : 0 ≀ Cβ‚€) (hC₁ : 0 ≀ C₁) (hMβ‚€ : 0 ≀ M)
    (hsecond : βˆ€ x ∈ Icc (a-2*R) (b+2*R), iteratedDeriv 2 Ξ¦ x ≀ -d)
    (hupper : βˆ€ x ∈ Icc (a-2*R) (b+2*R), -D ≀ iteratedDeriv 2 Ξ¦ x)
    (hM : βˆ€ x ∈ Icc (a-2*R) (b+2*R), |iteratedDeriv 3 Ξ¦ x| ≀ M)
    (hAb : βˆ€ z x, x ∈ Icc (a-2*R) (b+2*R) β†’ β€–A z xβ€– ≀ Cβ‚€)
    (hA'b : βˆ€ z x, x ∈ Icc (a-2*R) (b+2*R) β†’ β€–deriv (A z) xβ€– ≀ C₁)
    (hsupp : βˆ€ z, Function.support (A z) βŠ† Ioc a b) :
    TendstoUniformly (fun t : ℝ => fun p : Ξ± Γ— ℝ =>
      (Real.sqrt t : β„‚) * (∫ x, A p.1 x * Complex.exp (I * (t*(Ξ¦ x-p.2*x) : ℝ))) -
…
  54. lemma OAI.ThreeTorus.norm_stationaryLeading line 1538
  55. lemma OAI.ThreeTorus.stationaryLeading_norm_time line 1546
  56. lemma OAI.ThreeTorus.stationaryLeading_bound line 1552
  57. lemma OAI.ThreeTorus.compact_phase_tail_bound line 1573
  58. lemma OAI.ThreeTorus.norm_sq_difference_bound line 1620
  59. lemma OAI.ThreeTorus.stationary_pointwise_mass_bound line 1634
  60. lemma OAI.ThreeTorus.stationary_integrated_mass_bound line 1648
  61. lemma OAI.ThreeTorus.integer_band_card_bound line 1659
  62. lemma OAI.ThreeTorus.stationary_band_mass_bound line 1671
  63. lemma OAI.ThreeTorus.integer_band_exhausts line 1688
  64. lemma OAI.ThreeTorus.stationary_tail_mass_tendsto line 1699
  65. lemma OAI.ThreeTorus.stationary_tail_square_bound_summable line 1721
  66. lemma OAI.ThreeTorus.stationary_band_mass_tendsto line 1726
  67. lemma OAI.ThreeTorus.tsum_band_tail_decomposition line 1758
  68. lemma OAI.ThreeTorus.tsum_tendsto_zero_of_band_and_tail line 1778
  69. lemma OAI.ThreeTorus.summed_stationary_mass line 1792

    Source documentation

    Summed LΒΉ coefficient-mass conclusion; unlike weak convergence this controls all retained index subarrays and their pushforwards.

    lemma summed_stationary_mass {Ξ© : Type*} [MeasurableSpace Ξ©]
    {ΞΌ : Measure Ξ©} [IsProbabilityMeasure ΞΌ] {C Ld : β„• β†’ β„€ β†’ Ξ© β†’ β„‚} {L D : ℝ}
    (K : β„•) (hK : 1 ≀ K) (hL : 0 ≀ L)
    (hi : βˆ€ n j, Integrable (fun x => |β€–C n j xβ€–^2-(n:ℝ)⁻¹*β€–Ld n j xβ€–^2|) ΞΌ)
    (he : TendstoUniformly (fun n : β„• => fun p : β„€ Γ— Ξ© =>
      (Real.sqrt n : β„‚)*C n p.1 p.2-Ld n p.1 p.2) (fun _ => 0) atTop)
    (hw : βˆ€ n j x, β€–Ld n j xβ€– ≀ L)
    (ht : βˆ€αΆ  n : β„• in atTop, βˆ€ j, j βˆ‰ Finset.Icc (-(K*n : β„€)) (K*n) β†’
      (∫ x, |β€–C n j xβ€–^2-(n:ℝ)⁻¹*β€–Ld n j xβ€–^2| βˆ‚ΞΌ) ≀ D^2/(j:ℝ)^2) :
    Tendsto (fun n : β„• => βˆ‘' j : β„€,
      ∫ x, |β€–C n j xβ€–^2-(n:ℝ)⁻¹*β€–Ld n j xβ€–^2| βˆ‚ΞΌ) atTop (𝓝 0) := by
…

    Mentions: OAI.ThreeTorus.ΞΌ

  70. def OAI.ThreeTorus.passageSlope line 1811

    Source documentation

    Rounding is in the slow Fourier slope, not a translation of the fast variable.

    def passageSlope (ΞΊ : ℝ) (Ξ± : β„• β†’ ℝ) (n : β„•) (j : β„€) : ℝ := ΞΊ*(j:ℝ)/(n:ℝ)-Ξ± n
  71. def OAI.ThreeTorus.passageCoefficient line 1813
  72. def OAI.ThreeTorus.passageLeading line 1817
  73. lemma OAI.ThreeTorus.passage_uniform_error line 1821
  74. lemma OAI.ThreeTorus.passageSlope_large line 1843
  75. lemma OAI.ThreeTorus.passage_arrays_tail line 1870
  76. lemma OAI.ThreeTorus.passage_summed_mass line 1909

    Source documentation

    The strong summed mass estimate used in the passage lemma.

    lemma passage_summed_mass {Ξ© : Type*} [MeasurableSpace Ξ©]
    {ΞΌ : Measure Ξ©} [IsProbabilityMeasure ΞΌ] {Ξ¦ : ℝ β†’ ℝ} {A : Ξ© β†’ ℝ β†’ β„‚}
    (hΞ¦ : ContDiff ℝ 3 Ξ¦) (hA : βˆ€ z, ContDiff ℝ 2 (A z))
    {a b R d D Cβ‚€ C₁ M M₁ C ΞΊ : ℝ} {Ξ± : β„• β†’ ℝ}
    (hab : a ≀ b) (hR : 0 < R) (hd : 0 < d) (hdD : d ≀ D)
    (hCβ‚€ : 0 ≀ Cβ‚€) (hC₁ : 0 ≀ C₁) (hMβ‚€ : 0 ≀ M) (hM₁ : 0 ≀ M₁)
    (hC : 0 ≀ C) (hΞΊ : 0 < ΞΊ) (hΞ± : βˆ€ n, |Ξ± n| ≀ C)
    (hfirst : βˆ€ x ∈ Icc (a-2*R) (b+2*R), |deriv Ξ¦ x| ≀ M₁)
    (hsecond : βˆ€ x ∈ Icc (a-2*R) (b+2*R), d ≀ iteratedDeriv 2 Ξ¦ x)
    (hupper : βˆ€ x ∈ Icc (a-2*R) (b+2*R), iteratedDeriv 2 Ξ¦ x ≀ D)
    (hM : βˆ€ x ∈ Icc (a-2*R) (b+2*R), |iteratedDeriv 3 Ξ¦ x| ≀ M)
    (hAb : βˆ€ z x, x ∈ Icc (a-2*R) (b+2*R) β†’ β€–A z xβ€– ≀ Cβ‚€)
…

    Mentions: OAI.ThreeTorus.ΞΌ