OAI/Dynamics/ThreeTorus/PositiveLaws.lean

GitHub source file

116 declarations, 0 contain sorry, 0 declared as axioms

Positive Fourier laws, compact integral differentiation, affine densities, and prime-sieve signal laws.

  1. lemma OAI.ThreeTorus.hasFDerivAt_compact_integral line 26

    Source documentation

    Compact-parameter differentiation, used by the exact passage near epsilon=0.

    lemma hasFDerivAt_compact_integral
    {E : Type} {G : Type*} [NormedAddCommGroup E] [NormedSpace ℝ E] [FiniteDimensional ℝ E]
    [NormedAddCommGroup G] [NormedSpace ℝ G] [CompleteSpace G]
    {F : E × ℝ → G} (hF : ContDiff ℝ 1 F) (a b : ℝ) (x : E) :
    HasFDerivAt (fun y => ∫ t in a..b, F (y,t))
      (∫ t in a..b, (fderiv ℝ F (x,t)).comp (ContinuousLinearMap.inl ℝ E ℝ)) x := by
…
  2. lemma OAI.ThreeTorus.contDiff_compact_integral line 51

    Source documentation

    Smooth parameter integration over a fixed compact interval.

    lemma contDiff_compact_integral
    {E : Type} {G : Type*} [NormedAddCommGroup E] [NormedSpace ℝ E] [FiniteDimensional ℝ E]
    [NormedAddCommGroup G] [NormedSpace ℝ G] [CompleteSpace G]
    (n : ℕ) {F : E × ℝ → G} (hF : ContDiff ℝ n F) (a b : ℝ) :
    ContDiff ℝ n (fun y => ∫ t in a..b, F (y,t)) := by
…
  3. lemma OAI.ThreeTorus.smooth_compact_integral line 76
  4. lemma OAI.ThreeTorus.sinc_eq_integral_cos line 90
  5. lemma OAI.ThreeTorus.smooth_sinc line 99
  6. def OAI.ThreeTorus.signalSinc line 104
  7. def OAI.ThreeTorus.signalAverageRadius line 106
  8. def OAI.ThreeTorus.signalBaseline line 108
  9. lemma OAI.ThreeTorus.signalSinc_nonneg line 112
  10. lemma OAI.ThreeTorus.smooth_signalSinc line 115
  11. lemma OAI.ThreeTorus.smooth_signalBaseline line 119
  12. lemma OAI.ThreeTorus.sinc_sq_le line 125
  13. lemma OAI.ThreeTorus.sin_sq_le_one line 129
  14. lemma OAI.ThreeTorus.sinc_sq_mul_sq_le line 133
  15. lemma OAI.ThreeTorus.signalSinc_decay line 140
  16. lemma OAI.ThreeTorus.integrable_signalSinc line 155
  17. lemma OAI.ThreeTorus.signalAverageRadius_pos line 162
  18. lemma OAI.ThreeTorus.signalSinc_denominator line 166
  19. lemma OAI.ThreeTorus.integral_sin_sq_pi line 174
  20. lemma OAI.ThreeTorus.signal_sin_sq_average line 179
  21. lemma OAI.ThreeTorus.signalBaseline_nonneg line 194
  22. lemma OAI.ThreeTorus.signalBaseline_lower line 203

    Source documentation

    The averaging interval has exactly one sine-square period. In fact the manuscript's lower tail estimate holds at every point, including the origin.

    lemma signalBaseline_lower {α : ℝ} (hα : 0 < α) (R : ℝ) :
    1 / (2*Real.pi^2*α*(|R|+signalAverageRadius α)^2) ≤ signalBaseline α R := by
…

    Mentions: OAI.ThreeTorus.signalAverageRadius, OAI.ThreeTorus.signalBaseline

  23. lemma OAI.ThreeTorus.shifted_quadratic_bound line 234
  24. lemma OAI.ThreeTorus.signalBaseline_upper line 240
  25. lemma OAI.ThreeTorus.integrable_signalBaseline line 270
  26. def OAI.ThreeTorus.signalBox line 279
  27. def OAI.ThreeTorus.signalTriangle line 281
  28. lemma OAI.ThreeTorus.integrable_signalBox line 283
  29. lemma OAI.ThreeTorus.fourier_const_mul line 287
  30. lemma OAI.ThreeTorus.fourier_signalBox line 295
  31. lemma OAI.ThreeTorus.signalBox_convolution line 326
  32. lemma OAI.ThreeTorus.signalTriangle_eq_convolution line 359
  33. lemma OAI.ThreeTorus.integrable_signalTriangle line 366
  34. lemma OAI.ThreeTorus.continuous_signalTriangle line 371
  35. lemma OAI.ThreeTorus.fourier_signalTriangle line 374
  36. lemma OAI.ThreeTorus.fourierInv_signalSinc line 383
  37. lemma OAI.ThreeTorus.fourier_signalSinc line 391
  38. lemma OAI.ThreeTorus.signalBaseline_eq_convolution line 397
  39. lemma OAI.ThreeTorus.fourier_signalBaseline line 418
  40. lemma OAI.ThreeTorus.integral_signalBaseline line 436
  41. lemma OAI.ThreeTorus.signalBaseline_fourier_support line 446
  42. lemma OAI.ThreeTorus.signalBaseline_pos line 451
  43. theorem OAI.ThreeTorus.signalBaseline_quadratic_tails line 455
  44. lemma OAI.ThreeTorus.fourier_hermitian_real line 477
  45. def OAI.ThreeTorus.signalInverse line 495
  46. lemma OAI.ThreeTorus.signalInverse_complex line 497
  47. lemma OAI.ThreeTorus.signalInverse_contDiff line 501
  48. lemma OAI.ThreeTorus.signalInverse_integrable line 506
  49. lemma OAI.ThreeTorus.signalInverse_inversion line 511
  50. lemma OAI.ThreeTorus.integral_signalInverse line 520
  51. lemma OAI.ThreeTorus.signalInverse_quadratic_bound line 532
  52. lemma OAI.ThreeTorus.conj_stdAddChar line 544
  53. def OAI.ThreeTorus.signalRamanujanC line 550

    Source documentation

    The exact Ramanujan coefficient in the joint law of Section 3.

    def signalRamanujanC (P : ℕ) [NeZero P] (h : ZMod P) : ℂ :=
…
  54. def OAI.ThreeTorus.signalRamanujan line 553
  55. lemma OAI.ThreeTorus.conj_signalRamanujanC line 556
  56. lemma OAI.ThreeTorus.signalRamanujan_complex line 564
  57. lemma OAI.ThreeTorus.signalRamanujan_bound line 568
  58. lemma OAI.ThreeTorus.sum_stdAddChar_mul line 576
  59. lemma OAI.ThreeTorus.signalRamanujan_selector line 583
  60. def OAI.ThreeTorus.signalJoint line 612

    Source documentation

    Joint law; its marginal over the residue coordinate has total mass one.

    def signalJoint (α γ : ℝ) (d : ℝ → ℂ) (P : ℕ) [NeZero P] (h : ZMod P) (R : ℝ) : ℝ :=
…
  61. lemma OAI.ThreeTorus.signalJoint_smooth line 615
  62. lemma OAI.ThreeTorus.signalJoint_integrable line 622
  63. lemma OAI.ThreeTorus.integral_signalJoint line 628
  64. lemma OAI.ThreeTorus.fourier_add_integrable line 638
  65. lemma OAI.ThreeTorus.fourierInv_add_integrable line 644
  66. lemma OAI.ThreeTorus.fourierInv_const_mul line 648
  67. lemma OAI.ThreeTorus.fourierInv_signalJoint line 652
  68. theorem OAI.ThreeTorus.signalJoint_fourier line 672

    Source documentation

    Exact positive-exponent joint Fourier transform, not a conditional moment assumption.

    theorem signalJoint_fourier {α : ℝ} (hα : 0 < α) (γ : ℝ) {d : ℝ → ℂ}
    (hd : ContDiff ℝ ((⊤ : ℕ∞) : WithTop ℕ∞) d) (hc : HasCompactSupport d)
    (hr : ∀ v, d (-v) = conj (d v)) (P : ℕ) [NeZero P] (v : ℝ) (k : ZMod P) :
    ∑ h : ZMod P, (𝓕⁻ (fun R => (signalJoint α γ d P h R : ℂ)) v)*
      ZMod.stdAddChar (k*h) =
      (if k = 0 then 𝓕⁻ (fun R => (signalBaseline α R : ℂ)) v else 0)+
      (if IsUnit k then (γ : ℂ)*d v else 0) := by
…

    Mentions: OAI.ThreeTorus.signalJoint, OAI.ThreeTorus.signalBaseline

  69. theorem OAI.ThreeTorus.signalJoint_positive_strength line 695

    Source documentation

    Small strengths give the actual positive law, with the source's quantitative two-sided domination. The choice is independent of the angular scale B.

    theorem signalJoint_positive_strength {α : ℝ} (hα : 0 < α) {d : ℝ → ℂ}
    (hd : ContDiff ℝ ((⊤ : ℕ∞) : WithTop ℕ∞) d) (hc : HasCompactSupport d)
    (P : ℕ) [NeZero P] :
    ∃ γ₀ : ℝ, 0 < γ₀ ∧ ∀ γ : ℝ, 0 ≤ γ → γ ≤ γ₀ →
      (∀ h : ZMod P, ∀ R : ℝ, signalBaseline α R/(2*P) ≤ signalJoint α γ d P h R ∧
        signalJoint α γ d P h R ≤ 3*signalBaseline α R/(2*P)) ∧
      ∀ v : ℝ, 2*γ*‖d v‖ ≤ 1/2 := by
…

    Mentions: OAI.ThreeTorus.signalBaseline, OAI.ThreeTorus.signalJoint

  70. def OAI.ThreeTorus.signalPrimeProduct line 745

    Source documentation

    The manuscript's finite sieve modulus, unchanged (not a factorial proxy).

    def signalPrimeProduct (L : ℕ) : ℕ :=
…
  71. lemma OAI.ThreeTorus.signalPrimeProduct_pos line 748
  72. instance OAI.ThreeTorus.(instance at line 753) line 753
  73. lemma OAI.ThreeTorus.dvd_signalPrimeProduct line 755
  74. lemma OAI.ThreeTorus.signalPrimeProduct_ge_two line 760
  75. lemma OAI.ThreeTorus.signal_sieve_no_unit line 763
  76. theorem OAI.ThreeTorus.signalJoint_sieved_moments line 773

    Source documentation

    The exact ideal integer moments, with only the first nonzero harmonic.

    theorem signalJoint_sieved_moments {α b D x : ℝ} (hα : 0 < α) (hαb : α < b)
    (hb : 0 < b) (hx : b ≤ |x|) {L : ℕ} (hL : D/b < L)
    {d : ℝ → ℂ} (hd : ContDiff ℝ ((⊤ : ℕ∞) : WithTop ℕ∞) d)
    (hc : HasCompactSupport d) (hr : ∀ v, d (-v) = conj (d v))
    (hs : Function.support d ⊆ Icc (-D) D) (γ : ℝ)
    (m : ZMod (signalPrimeProduct L)) (ℓ : ℕ) (hℓ : 1 ≤ ℓ) :
    ∑ h : ZMod (signalPrimeProduct L),
      (𝓕⁻ (fun R => (signalJoint α γ d (signalPrimeProduct L) h R : ℂ))) (ℓ*x)*
        ZMod.stdAddChar (((ℓ : ZMod (signalPrimeProduct L))*m)*h) =
      if ℓ = 1 ∧ IsUnit m then (γ : ℂ)*d x else 0 := by
…

    Mentions: OAI.ThreeTorus.signalPrimeProduct, OAI.ThreeTorus.signalJoint

  77. theorem OAI.ThreeTorus.exists_signal_positive_law line 810

    Source documentation

    All choices of the positive-law construction precede the angular scale. The interval support used below is the exact compact support condition on d.

    theorem exists_signal_positive_law {b D : ℝ} (hb : 0 < b)
    {d : ℝ → ℂ} (hd : ContDiff ℝ ((⊤ : ℕ∞) : WithTop ℕ∞) d)
    (hc : HasCompactSupport d) (hr : ∀ v, d (-v) = conj (d v))
    (h0 : d 0 = 0) (hs : Function.support d ⊆ Icc (-D) D) :
    ∃ α : ℝ, ∃ L : ℕ, ∃ γ₀ : ℝ,
      0 < α ∧ α < b/2 ∧ 2 ≤ L ∧ D/b < L ∧ 0 < γ₀ ∧
      ∀ γ : ℝ, 0 < γ → γ ≤ γ₀ →
        (∀ h : ZMod (signalPrimeProduct L),
          ContDiff ℝ ((⊤ : ℕ∞) : WithTop ℕ∞) (signalJoint α γ d (signalPrimeProduct L) h) ∧
          Integrable (signalJoint α γ d (signalPrimeProduct L) h) ∧
          (∫ R, signalJoint α γ d (signalPrimeProduct L) h R) = 1/(signalPrimeProduct L) ∧
          ∀ R, signalBaseline α R/(2*(signalPrimeProduct L)) ≤
…

    Mentions: OAI.ThreeTorus.signalPrimeProduct, OAI.ThreeTorus.signalJoint, OAI.ThreeTorus.signalBaseline

  78. def OAI.ThreeTorus.affineDensity line 855
  79. lemma OAI.ThreeTorus.integrable_affineDensity line 857
  80. lemma OAI.ThreeTorus.integral_affineDensity line 862
  81. lemma OAI.ThreeTorus.fourierInv_affineDensity line 870
  82. lemma OAI.ThreeTorus.affine_square_bound line 904
  83. lemma OAI.ThreeTorus.affineDensity_quadratic_tails line 909
  84. lemma OAI.ThreeTorus.finite_sum_quadratic_tails line 945
  85. def OAI.ThreeTorus.signalJitter line 964

    Source documentation

    Density of J_*=(R/B+h/P)/c; the finite representatives are h.val.

    def signalJitter (α γ : ℝ) (d : ℝ → ℂ) (P : ℕ) [NeZero P]
    (B c y : ℝ) : ℝ :=
…
  86. lemma OAI.ThreeTorus.signalJitter_affine line 968
  87. lemma OAI.ThreeTorus.signalJitter_smooth line 979
  88. lemma OAI.ThreeTorus.signalJitter_integrable line 989
  89. lemma OAI.ThreeTorus.integral_signalJitter line 999
  90. lemma OAI.ThreeTorus.signalJitter_quadratic_tails line 1010
  91. lemma OAI.ThreeTorus.signalJitter_pos line 1037
  92. lemma OAI.ThreeTorus.fourierInv_finsetSum line 1045
  93. lemma OAI.ThreeTorus.signalJitter_fourierInv line 1051
  94. lemma OAI.ThreeTorus.signal_character line 1074
  95. lemma OAI.ThreeTorus.signalJitter_integer_moments line 1084
  96. lemma OAI.ThreeTorus.signalJitter_sieved_moments line 1099
  97. def OAI.ThreeTorus.scaledDensity line 1127

    Source documentation

    Density under multiplication by a nonzero real scale, including negative scales.

    def scaledDensity (q : ℝ → ℝ) (s y : ℝ) : ℝ := |s|⁻¹*q (y/s)
  98. lemma OAI.ThreeTorus.integrable_scaledDensity line 1129
  99. lemma OAI.ThreeTorus.integral_scaledDensity line 1135
  100. lemma OAI.ThreeTorus.fourierInv_scaledDensity line 1142
  101. lemma OAI.ThreeTorus.fourier_scaledDensity line 1170
  102. lemma OAI.ThreeTorus.scaledDensity_quadratic_bound line 1175
  103. lemma OAI.ThreeTorus.quadratic_norm_isBigO line 1193
  104. lemma OAI.ThreeTorus.summable_lattice_of_bounded_support line 1205
  105. theorem OAI.ThreeTorus.periodization_fourier line 1216

    Source documentation

    Exact Poisson expansion for every continuously bandlimited quadratic-tail law.

    theorem periodization_fourier {q : ℝ → ℝ} (hq : Continuous q) {C : ℝ} (hC : 0 ≤ C)
    (hbnd : ∀ y, |q y| ≤ C/(1+y^2)) {D : ℝ}
    (hF : ∀ v, D < |v| → 𝓕 (fun y => (q y : ℂ)) v = 0) (x : ℝ) :
    ∑' n : ℤ, (q (x+n) : ℂ) =
      ∑' n : ℤ, 𝓕 (fun y => (q y : ℂ)) (n:ℝ)*fourier n (x : UnitAddCircle) := by
…
  106. lemma OAI.ThreeTorus.fourierInv_real_neg line 1226
  107. lemma OAI.ThreeTorus.periodization_three_modes line 1237
  108. lemma OAI.ThreeTorus.periodization_scaled_finite line 1283

    Source documentation

    A compact Fourier bandwidth supplies a shared finite series near any nonzero scale.

    lemma periodization_scaled_finite {q : ℝ → ℝ} (hq : Continuous q)
    {C : ℝ} (hC : 0 ≤ C) (hbnd : ∀ y, |q y| ≤ C/(1+y^2))
    {D ε : ℝ} (hε : 0 < ε) (hF : ∀ v, D < |v| → 𝓕 (fun y => (q y : ℂ)) v = 0)
    {N : ℕ} (hN : D < N*ε) {s : ℝ} (hs : ε ≤ |s|) (x : ℝ) :
    ∑' n : ℤ, (scaledDensity q s (x+n) : ℂ) =
      ∑ n ∈ Finset.Icc (-(N:ℤ)) N,
        𝓕 (fun y => (q y : ℂ)) ((n:ℝ)*s)*fourier n (x : UnitAddCircle) := by
…

    Mentions: OAI.ThreeTorus.scaledDensity

  109. lemma OAI.ThreeTorus.periodization_scaled_tendstoUniformly line 1318
  110. lemma OAI.ThreeTorus.fourierInv_real_zero line 1353
  111. lemma OAI.ThreeTorus.fourierInv_real_int_moments line 1359
  112. lemma OAI.ThreeTorus.signalJitter_fourierInv_support line 1392
  113. lemma OAI.ThreeTorus.signalJitter_scale_cancel line 1416
  114. lemma OAI.ThreeTorus.signalJitter_periodic_ideal line 1427
  115. lemma OAI.ThreeTorus.periodization_scaled_uniform_perturbation line 1468

    Source documentation

    The finite-c approximation is uniform on every fixed old speed range. The exact ideal law is independent of c after scaling, as required in section 3.

    lemma periodization_scaled_uniform_perturbation {q : ℝ → ℝ} (hq : Continuous q)
    (hqi : Integrable q) {C : ℝ} (hC : 0 ≤ C) (hbnd : ∀ y, |q y| ≤ C/(1+y^2))
    {D : ℝ} (hF : ∀ v, D < |v| → 𝓕 (fun y => (q y : ℂ)) v = 0)
    {s₀ : ℝ} (hs₀ : s₀ ≠ 0) (V : ℝ) :
    ∀ ε > 0, ∀ᶠ c : ℝ in atTop, ∀ v : ℝ, |v| ≤ V → ∀ y : ℝ,
      dist (∑' n : ℤ, (scaledDensity q (s₀*(1+v/c)) (y+n) : ℂ))
        (∑' n : ℤ, (scaledDensity q s₀ (y+n) : ℂ)) < ε := by
…

    Mentions: OAI.ThreeTorus.scaledDensity

  116. lemma OAI.ThreeTorus.signalJitter_periodic_approximation line 1499

    Source documentation

    The actual finite-c signal law, uniform in the bounded old speed and in all phases. The modulus and strength are the exact fixed ones of the manuscript.

    lemma signalJitter_periodic_approximation {α B b D : ℝ}
    (hα : 0 < α) (hαb : α < b) (hαD : α ≤ D) (hB : 0 < B) (hb : 0 < b)
    {L : ℕ} (hL : D/b < L) (γ : ℝ) {d : ℝ → ℂ}
    (hd : ContDiff ℝ ((⊤ : ℕ∞) : WithTop ℕ∞) d) (hcomp : HasCompactSupport d)
    (hr : ∀ v, d (-v) = starRingEnd ℂ (d v)) (h0 : d 0 = 0)
    (hs : Function.support d ⊆ Icc (-D) D) (m : ℤ) (hm : b ≤ |(m:ℝ)/B|)
    (hbound : ∀ h R, signalBaseline α R/(2*signalPrimeProduct L) ≤
        signalJoint α γ d (signalPrimeProduct L) h R ∧
      signalJoint α γ d (signalPrimeProduct L) h R ≤
        3*signalBaseline α R/(2*signalPrimeProduct L)) (V : ℝ) :
    ∀ ε > 0, ∀ᶠ c : ℝ in atTop, ∀ v : ℝ, |v| ≤ V → ∀ y : ℝ,
      dist (∑' k : ℤ, (scaledDensity (signalJitter α γ d (signalPrimeProduct L) B c)
…

    Mentions: OAI.ThreeTorus.signalBaseline, OAI.ThreeTorus.signalPrimeProduct, OAI.ThreeTorus.signalJoint, OAI.ThreeTorus.scaledDensity, OAI.ThreeTorus.signalJitter