OAI/Dynamics/ThreeTorus/PassageDensity.lean

GitHub source file

127 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.ThreeTorus.circleDensityLift line 20

   Source documentation

   The usual interval representative of a circle weight, with zero extension.

   def circleDensityLift (o : ℝ) (q : UnitAddCircle → ℝ) : ℝ → ℝ :=
   …

2. lemma OAI.ThreeTorus.circle_integral_lift line 23
3. lemma OAI.ThreeTorus.integrable_circleDensityLift line 29
4. lemma OAI.ThreeTorus.circleDensityLift_pushforward line 41

   Source documentation

   Lifting a circle density on one period commutes with every measurable spectral pushforward. This includes the actual jitter, not just polynomial tests.

   lemma circleDensityLift_pushforward {Y : Type*} [MeasurableSpace Y]
       {q : UnitAddCircle → ℝ} (hq : Integrable q AddCircle.haarAddCircle)
       {T : UnitAddCircle → Y} (hT : Measurable T) (o : ℝ) :
       ((volume : Measure ℝ).withDensityᵥ (circleDensityLift o q)).map
         (fun x : ℝ => T (x : UnitAddCircle)) =
       (AddCircle.haarAddCircle.withDensityᵥ q).map T := by
   …

   Mentions: OAI.ThreeTorus.circleDensityLift

5. lemma OAI.ThreeTorus.circleDensityLift_eq line 59
6. lemma OAI.ThreeTorus.integrable_branchDensity line 68
7. lemma OAI.ThreeTorus.branchDensity_pushforward line 87

   Source documentation

   Exact pushforward of the old squared coefficient on a branch. The only inverse assumptions are the ordinary left-inverse identities on that branch.

   lemma branchDensity_pushforward {I : Set ℝ} {J g D q : ℝ → ℝ}
       (hI : MeasurableSet I) (himage : MeasurableSet (J '' I)) (hJm : Measurable J)
       (hJ : ∀ x ∈ I, HasDerivWithinAt J (D x) I x) (hinj : InjOn J I)
       (hg : ∀ x ∈ I, g (J x) = x) (hD : ∀ x ∈ I, D x ≠ 0)
       (hq : Integrable q) (hqs : Function.support q ⊆ I) :
       ((volume : Measure ℝ).withDensityᵥ q).map J =
         (volume : Measure ℝ).withDensityᵥ (branchDensity I J g D q) := by
   …

   Mentions: OAI.ThreeTorus.branchDensity

8. lemma OAI.ThreeTorus.density_map_congr_support line 122
9. lemma OAI.ThreeTorus.circle_branch_pushforward line 141

   Source documentation

   The branch-Jacobian formula on the actual circle. The global periodic jitter need not be injective; only the good arc bearing the weight is used.

   lemma circle_branch_pushforward {q : UnitAddCircle → ℝ} {q₀ J₀ g D : ℝ → ℝ}
       {J : UnitAddCircle → ℝ} {o : ℝ} {I : Set ℝ}
       (hq : Integrable q AddCircle.haarAddCircle)
       (hq₀ : ∀ x ∈ Ioc o (o+1), q (x : UnitAddCircle) = q₀ x)
       (hq₀s : Function.support q₀ ⊆ Ioc o (o+1)) (hqs : Function.support q₀ ⊆ I)
       (hj : Measurable J) (hj₀ : Measurable J₀)
       (hJe : ∀ x ∈ I, J (x : UnitAddCircle) = J₀ x)
       (hI : MeasurableSet I) (himage : MeasurableSet (J₀ '' I))
       (hJ : ∀ x ∈ I, HasDerivWithinAt J₀ (D x) I x) (hinj : InjOn J₀ I)
       (hg : ∀ x ∈ I, g (J₀ x) = x) (hD : ∀ x ∈ I, D x ≠ 0) :
       (AddCircle.haarAddCircle.withDensityᵥ q).map J =
         (volume : Measure ℝ).withDensityᵥ (branchDensity I J₀ g D q₀) := by
   …

   Mentions: OAI.ThreeTorus.branchDensity

10. lemma OAI.ThreeTorus.l1_pushforward_contraction line 162

    Source documentation

    Total variation contracts under the actual temporal-frequency pushforward. The real L¹ normalization has no factor 1/2.

    lemma l1_pushforward_contraction {X Y : Type*} [MeasurableSpace X] [MeasurableSpace Y]
        {μ : Measure X} {ν : Measure Y} {f : X → ℝ} {g : Y → ℝ} {T : X → Y}
        (hf : Integrable f μ) (hg : Integrable g ν) (hT : Measurable T)
        (hmap : (μ.withDensityᵥ f).map T = ν.withDensityᵥ g) :
        (∫ y, |g y| ∂ν) ≤ ∫ x, |f x| ∂μ := by
    …

    Mentions: OAI.ThreeTorus.μ

11. lemma OAI.ThreeTorus.l1_pushforward_difference line 178
12. lemma OAI.ThreeTorus.temporalFrequency_pushforward line 193

    Source documentation

    Exact Jacobian cancellation in the unfolded output frequency t=(j+y)/N.

    lemma temporalFrequency_pushforward {q : ℝ → ℝ} (hq : Integrable q)
        {n : ℝ} (hn : 0 < n) (j : ℝ) :
        ((volume : Measure ℝ).withDensityᵥ (fun y => n⁻¹*q y)).map (fun y => (j+y)/n) =
          (volume : Measure ℝ).withDensityᵥ (fun t => q (n*t-j)) := by
    …

13. lemma OAI.ThreeTorus.temporalFrequency_pushforward_comp line 215

    Source documentation

    Pushforward through a fixed smooth jitter followed by the output affine frequency. This is the exact (not weak or asymptotic) density appearing in the passage.

    lemma temporalFrequency_pushforward_comp {X : Type*} [MeasurableSpace X]
        {μ : Measure X} {W : X → ℝ} {q : ℝ → ℝ} {J : X → ℝ}
        (hW : Integrable W μ) (hq : Integrable q) (hJ : Measurable J)
        (hpush : (μ.withDensityᵥ W).map J = (volume : Measure ℝ).withDensityᵥ q)
        {n : ℝ} (hn : 0 < n) (j : ℝ) :
        (μ.withDensityᵥ (fun a => n⁻¹*W a)).map (fun a => (j+J a)/n) =
          (volume : Measure ℝ).withDensityᵥ (fun t => q (n*t-j)) := by
    …

    Mentions: OAI.ThreeTorus.μ

14. def OAI.ThreeTorus.scaledBranchKernel line 244

    Source documentation

    The manuscript kernel K(s,y), including both signs of s.

    def scaledBranchKernel (I : Set ℝ) (J g D q : ℝ → ℝ) (s y : ℝ) : ℝ :=
    …

15. lemma OAI.ThreeTorus.scaledBranchKernel_eq line 247
16. lemma OAI.ThreeTorus.integrable_scaledBranchKernel line 264
17. lemma OAI.ThreeTorus.circle_mode_pushforward line 271

    Source documentation

    The exact branch kernel in the new temporal coordinate, on the torus. Only the good arc need be injective, as in the geometric passage.

    lemma circle_mode_pushforward {q : UnitAddCircle → ℝ} {q₀ J₀ g D : ℝ → ℝ}
        {J : UnitAddCircle → ℝ} {o : ℝ} {I : Set ℝ}
        (hq : Integrable q AddCircle.haarAddCircle)
        (hq₀ : ∀ x ∈ Ioc o (o+1), q (x : UnitAddCircle) = q₀ x)
        (hq₀s : Function.support q₀ ⊆ Ioc o (o+1)) (hqs : Function.support q₀ ⊆ I)
        (hj : Measurable J) (hj₀ : Measurable J₀)
        (hJe : ∀ x ∈ I, J (x : UnitAddCircle) = J₀ x)
        (hI : MeasurableSet I) (himage : MeasurableSet (J₀ '' I))
        (hJ : ∀ x ∈ I, HasDerivWithinAt J₀ (D x) I x) (hinj : InjOn J₀ I)
        (hg : ∀ x ∈ I, g (J₀ x) = x) (hD : ∀ x ∈ I, D x ≠ 0)
        {s n : ℝ} (hs : s ≠ 0) (hn : 0 < n) (j : ℝ) :
        (AddCircle.haarAddCircle.withDensityᵥ (fun a => n⁻¹*q a)).map
    …

18. lemma OAI.ThreeTorus.integral_abs_finset_sum_le line 311
19. lemma OAI.ThreeTorus.finite_density_sum_error line 324

    Source documentation

    Summed coefficient mass error controls the full density error, not merely its moments. The maps may vary with the angular index.

    lemma finite_density_sum_error {X Y ι : Type*} [MeasurableSpace X] [MeasurableSpace Y]
        {μ : Measure X} {ν : Measure Y} {q w : ι → X → ℝ} {g h : ι → Y → ℝ}
        {T : ι → X → Y} (S : Finset ι)
        (hq : ∀ i ∈ S, Integrable (q i) μ) (hw : ∀ i ∈ S, Integrable (w i) μ)
        (hg : ∀ i ∈ S, Integrable (g i) ν) (hh : ∀ i ∈ S, Integrable (h i) ν)
        (hT : ∀ i ∈ S, Measurable (T i))
        (hqp : ∀ i ∈ S, (μ.withDensityᵥ (q i)).map (T i) = ν.withDensityᵥ (g i))
        (hwp : ∀ i ∈ S, (μ.withDensityᵥ (w i)).map (T i) = ν.withDensityᵥ (h i)) :
        (∫ y, |(∑ i ∈ S, g i y)-(∑ i ∈ S, h i y)| ∂ν) ≤
          ∑ i ∈ S, ∫ x, |q i x-w i x| ∂μ := by
    …

    Mentions: OAI.ThreeTorus.μ

20. lemma OAI.ThreeTorus.cutoff_mass_pointwise line 342
21. lemma OAI.ThreeTorus.retained_density_sum_error line 360

    Source documentation

    The actual retained cutoffs cost no additional error in the stationary mass estimate. The coefficient array may have both positive and negative indices.

    lemma retained_density_sum_error {X Y : Type*} [MeasurableSpace X] [MeasurableSpace Y]
        {μ : Measure X} {ν : Measure Y} {c : ℤ → X → ℂ} {w χ : ℤ → X → ℝ}
        {ψ : X → ℝ} {g h : ℤ → Y → ℝ} {T : ℤ → X → Y} (S : Finset ℤ)
        (hq : ∀ i ∈ S, Integrable (fun x => ψ x^2*χ i x^2*‖c i x‖^2) μ)
        (hw : ∀ i ∈ S, Integrable (fun x => ψ x^2*w i x) μ)
        (hE : ∀ i, Integrable (fun x => |‖c i x‖^2-w i x|) μ)
        (hEs : Summable (fun i => ∫ x, |‖c i x‖^2-w i x| ∂μ))
        (hχ : ∀ i x, 0 ≤ χ i x ∧ χ i x ≤ 1) (hχw : ∀ i x, w i x ≠ 0 → χ i x = 1)
        (hψ : ∀ x, 0 ≤ ψ x ∧ ψ x ≤ 1)
        (hg : ∀ i ∈ S, Integrable (g i) ν) (hh : ∀ i ∈ S, Integrable (h i) ν)
        (hT : ∀ i ∈ S, Measurable (T i))
        (hqp : ∀ i ∈ S, (μ.withDensityᵥ (fun x => ψ x^2*χ i x^2*‖c i x‖^2)).map (T i) =
    …

    Mentions: OAI.ThreeTorus.μ

22. def OAI.ThreeTorus.unfoldedModeDensity line 390

    Source documentation

    The actual unfolded spectral density of a retained angular mode, of mass q da. The argument q₀ is its zero-extended representative in the jitter good arc.

    def unfoldedModeDensity (I : Set ℝ) (J g D q₀ : ℝ → ℝ) (n j t : ℝ) : ℝ :=
    …

23. lemma OAI.ThreeTorus.integrable_unfoldedModeDensity line 393
24. lemma OAI.ThreeTorus.unfoldedModeDensity_pushforward line 409

    Source documentation

    Exact density of an actual circle mode before any stationary approximation.

    lemma unfoldedModeDensity_pushforward {q : UnitAddCircle → ℝ} {q₀ J₀ g D : ℝ → ℝ}
        {J : UnitAddCircle → ℝ} {o : ℝ} {I : Set ℝ}
        (hq : Integrable q AddCircle.haarAddCircle)
        (hq₀ : ∀ x ∈ Ioc o (o+1), q (x : UnitAddCircle) = q₀ x)
        (hq₀s : Function.support q₀ ⊆ Ioc o (o+1)) (hqs : Function.support q₀ ⊆ I)
        (hj : Measurable J) (hj₀ : Measurable J₀)
        (hJe : ∀ x ∈ I, J (x : UnitAddCircle) = J₀ x)
        (hI : MeasurableSet I) (himage : MeasurableSet (J₀ '' I))
        (hJ : ∀ x ∈ I, HasDerivWithinAt J₀ (D x) I x) (hinj : InjOn J₀ I)
        (hg : ∀ x ∈ I, g (J₀ x) = x) (hD : ∀ x ∈ I, D x ≠ 0)
        {n j : ℝ} (hn : 0 < n) (hjn : j ≠ 0) :
        (AddCircle.haarAddCircle.withDensityᵥ q).map
    …

25. lemma OAI.ThreeTorus.finite_unfolded_density_error line 439

    Source documentation

    Finite actual retained mode density versus finite leading sampled mass. Every density here is explicit; none of the pushforward identities is assumed.

    lemma finite_unfolded_density_error {I : Set ℝ} {J₀ g D : ℝ → ℝ}
        {J : UnitAddCircle → ℝ} {o n : ℝ} (hn : 0 < n)
        (S : Finset ℤ) (hS : ∀ j ∈ S, j ≠ 0)
        {q w : ℤ → UnitAddCircle → ℝ} {q₀ w₀ : ℤ → ℝ → ℝ}
        (hq : ∀ j ∈ S, Integrable (q j) AddCircle.haarAddCircle)
        (hw : ∀ j ∈ S, Integrable (w j) AddCircle.haarAddCircle)
        (hq₀ : ∀ j ∈ S, ∀ x ∈ Ioc o (o+1), q j (x : UnitAddCircle) = q₀ j x)
        (hw₀ : ∀ j ∈ S, ∀ x ∈ Ioc o (o+1), w j (x : UnitAddCircle) = w₀ j x)
        (hqs : ∀ j ∈ S, Function.support (q₀ j) ⊆ Ioc o (o+1) ∩ I)
        (hws : ∀ j ∈ S, Function.support (w₀ j) ⊆ Ioc o (o+1) ∩ I)
        (hj : Measurable J) (hj₀ : Measurable J₀)
        (hJe : ∀ x ∈ I, J (x : UnitAddCircle) = J₀ x)
    …

26. def OAI.ThreeTorus.branchKernel line 488

    Source documentation

    Parametrized old-frequency Jacobian density, extended by zero off its branch.

    def branchKernel (I : Set ℝ) (J : ℝ → ℝ) (F : ℝ × ℝ → ℝ) (p : ℝ × ℝ) : ℝ := by
    …

27. lemma OAI.ThreeTorus.support_branchKernel_subset line 492
28. lemma OAI.ThreeTorus.branchKernel_compact line 504
29. lemma OAI.ThreeTorus.branchKernel_smooth line 511
30. lemma OAI.ThreeTorus.branchKernel_bounds line 557
31. def OAI.ThreeTorus.affineKernel line 579

    Source documentation

    The exact Jacobian kernel for the affine-on-the-good-arc neutral jitter.

    def affineKernel (F : ℝ × ℝ → ℝ) (L β s y : ℝ) : ℝ :=
    …

32. lemma OAI.ThreeTorus.affineKernel_eq_zero_s line 582
33. lemma OAI.ThreeTorus.affineKernel_eq_zero_y line 586
34. lemma OAI.ThreeTorus.affineKernel_hasCompactSupport line 609
35. lemma OAI.ThreeTorus.affineKernel_smooth line 623
36. lemma OAI.ThreeTorus.compact_smooth_lipschitz line 652

    Source documentation

    A compact smooth kernel has a single global Lipschitz bound.

    lemma compact_smooth_lipschitz {F : ℝ × ℝ → ℝ}
        (hF : ContDiff ℝ ((⊤ : ℕ∞) : WithTop ℕ∞) F)
        (hc : HasCompactSupport F) : ∃ C : ℝ≥0, LipschitzWith C F := by
    …

37. lemma OAI.ThreeTorus.compact_smooth_kernel_lipschitz line 662
38. def OAI.ThreeTorus.samplingWindow line 678
39. lemma OAI.ThreeTorus.mem_samplingWindow line 681
40. lemma OAI.ThreeTorus.samplingWindow_card line 693
41. def OAI.ThreeTorus.sampledKernel line 700

    Source documentation

    Before freezing the slow coordinate, the exact rescaled kernel density.

    def sampledKernel (K : ℝ → ℝ → ℝ) (n : ℕ) (t : ℝ) : ℝ :=
    …

42. def OAI.ThreeTorus.fineKernel line 704

    Source documentation

    The fine density has the same fast argument and the slow argument frozen at t.

    def fineKernel (K : ℝ → ℝ → ℝ) (n : ℕ) (t : ℝ) : ℝ :=
    …

43. lemma OAI.ThreeTorus.sampledKernel_error line 707
44. lemma OAI.ThreeTorus.fineKernel_eq_zero line 742
45. lemma OAI.ThreeTorus.sampledKernel_eq_zero line 748
46. lemma OAI.ThreeTorus.sampledKernel_integral_error line 772

    Source documentation

    Strong L¹ replacement of the slow variable, rather than weak convergence.

    lemma sampledKernel_integral_error {K : ℝ → ℝ → ℝ} {C : ℝ≥0} {A : ℝ} {M n : ℕ}
        (hA : 0 ≤ A) (hK : ∀ y, LipschitzWith C (fun s => K s y))
        (hKs : ∀ s y, A < |s| → K s y = 0)
        (hKy : ∀ s y, (M:ℝ) < |y| → K s y = 0)
        (hn : 0 < n)
        (hi : Integrable (fun t => |sampledKernel K n t-fineKernel K n t|)) :
        (∫ t, |sampledKernel K n t-fineKernel K n t|) ≤
          (2*(A+M))*((2*(M:ℝ)+3)*C*M/n) := by
    …

    Mentions: OAI.ThreeTorus.sampledKernel, OAI.ThreeTorus.fineKernel

47. lemma OAI.ThreeTorus.continuous_sampledKernel line 802
48. lemma OAI.ThreeTorus.continuous_fineKernel line 825
49. lemma OAI.ThreeTorus.integrable_sampledKernel_error line 853
50. lemma OAI.ThreeTorus.tendsto_sampledKernel_error line 866
51. def OAI.ThreeTorus.sampledResidueKernel line 883

    Source documentation

    Exact progression j=h+kP; no divisibility restriction on the passage integer.

    def sampledResidueKernel (K : ℝ → ℝ → ℝ) (P : ℕ) (h : ℤ) (n : ℕ) (t : ℝ) : ℝ :=
    …

52. def OAI.ThreeTorus.fineResidueKernel line 886
53. lemma OAI.ThreeTorus.residue_window_mem line 889
54. lemma OAI.ThreeTorus.sampledResidueKernel_error line 900
55. lemma OAI.ThreeTorus.fineResidueKernel_eq_zero line 939
56. lemma OAI.ThreeTorus.sampledResidueKernel_eq_zero line 945
57. lemma OAI.ThreeTorus.residue_abs_bound line 975
58. lemma OAI.ThreeTorus.continuous_sampledResidueKernel line 983
59. lemma OAI.ThreeTorus.continuous_fineResidueKernel line 1009
60. lemma OAI.ThreeTorus.integrable_sampledResidueKernel_error line 1039
61. lemma OAI.ThreeTorus.sampledResidueKernel_integral_error line 1053
62. lemma OAI.ThreeTorus.tendsto_sampledResidueKernel_error line 1085
63. lemma OAI.ThreeTorus.affineKernel_fine_density line 1103

    Source documentation

    Fine-density freezing for the actual neutral affine jitter kernel. All regularity hypotheses are derived from the smooth compact old coefficient.

    lemma affineKernel_fine_density {F : ℝ × ℝ → ℝ} {L β A D ε : ℝ}
        (hF : ContDiff ℝ ((⊤ : ℕ∞) : WithTop ℕ∞) F)
        (hL : 0 < L) (hA : 0 ≤ A) (hD : 0 ≤ D) (hε : 0 < ε)
        (hz : ∀ s a, |s| < ε → F (s,a) = 0)
        (hFs : ∀ s a, A < |s| → F (s,a) = 0)
        (hFa : ∀ s a, D < |a| → F (s,a) = 0)
        {P : ℕ} (hP : 0 < P) (h : ℤ) :
        Tendsto (fun n : ℕ => ∫ t,
          |sampledResidueKernel (affineKernel F L β) P h n t -
            fineResidueKernel (affineKernel F L β) P h n t|) atTop (𝓝 0) := by
    …

    Mentions: OAI.ThreeTorus.sampledResidueKernel, OAI.ThreeTorus.affineKernel, OAI.ThreeTorus.fineResidueKernel

64. def OAI.ThreeTorus.signalKernel line 1124

    Source documentation

    The transmitting kernel when the old coefficient modulus is independent of the spare coordinate and its jitter law has density rho.

    def signalKernel (W ρ : ℝ → ℝ) (s y : ℝ) : ℝ := W s / |s| * ρ (y/s)

65. lemma OAI.ThreeTorus.signalKernel_as_affine line 1126
66. lemma OAI.ThreeTorus.signalKernel_fine_density line 1132
67. def OAI.ThreeTorus.passageBranchKernel line 1152

    Source documentation

    General smooth jitter kernel. The source's old-frequency variable is the second coordinate of F; the first is the new slow-coordinate good arc.

    def passageBranchKernel (I : Set ℝ) (J : ℝ → ℝ) (F : ℝ × ℝ → ℝ) : ℝ → ℝ → ℝ :=
    …

68. lemma OAI.ThreeTorus.passageBranchKernel_formula line 1155
69. lemma OAI.ThreeTorus.passageBranchKernel_fine_density line 1161

    Source documentation

    Fine temporal sampling on any smooth monotone good arc, both signs, all residue classes and all positive passage integers; no divisibility pin.

    lemma passageBranchKernel_fine_density {J : ℝ → ℝ} {I : Set ℝ} {F : ℝ × ℝ → ℝ}
        (hJ : ContDiff ℝ ((⊤ : ℕ∞) : WithTop ℕ∞) J) (hIo : IsOpen I)
        (hinj : InjOn J I) (hd : ∀ x ∈ I, deriv J x ≠ 0)
        (hF : ContDiff ℝ ((⊤ : ℕ∞) : WithTop ℕ∞) F) (hc : HasCompactSupport F)
        (hs : tsupport F ⊆ I ×ˢ univ) {ε : ℝ} (hε : 0 < ε)
        (hz : ∀ a s, |s| < ε → F (a,s) = 0) {P : ℕ} (hP : 0 < P) (h : ℤ) :
        Tendsto (fun n : ℕ => ∫ t,
          |sampledResidueKernel (passageBranchKernel I J F) P h n t-
            fineResidueKernel (passageBranchKernel I J F) P h n t|) atTop (𝓝 0) := by
    …

    Mentions: OAI.ThreeTorus.sampledResidueKernel, OAI.ThreeTorus.passageBranchKernel, OAI.ThreeTorus.fineResidueKernel

70. lemma OAI.ThreeTorus.unfoldedModeDensity_stationary line 1187

    Source documentation

    The exact sampled leading density is the good-arc Jacobian kernel. This identifies the coefficient-level approximation with the fine-density calculation; it is an equality, not a new spectral hypothesis.

    lemma unfoldedModeDensity_stationary (I : Set ℝ) (J : ℝ → ℝ)
        (F : ℝ × ℝ → ℝ) {n : ℝ} (hn : n ≠ 0) (j t : ℝ) :
        unfoldedModeDensity I J (invFunOn J I) (deriv J)
          (fun a => n⁻¹*F (a,j/n)) n j t =
          passageBranchKernel I J F (j/n) (n*t-j) := by
    …

    Mentions: OAI.ThreeTorus.unfoldedModeDensity, OAI.ThreeTorus.passageBranchKernel

71. lemma OAI.ThreeTorus.finite_unfolded_index_error line 1205
72. lemma OAI.ThreeTorus.leading_unfolded_residue_eq_sampled line 1247
73. lemma OAI.ThreeTorus.integral_abs_triangle line 1267
74. lemma OAI.ThreeTorus.passageBranchKernel_integrable_error line 1280
75. lemma OAI.ThreeTorus.sum_residue_le_tsum line 1310
76. lemma OAI.ThreeTorus.unfolded_residue_density_error line 1323

    Source documentation

    Full finite retained residue density estimate, at the actual spectral pushforwards. The right-hand side consists only of coefficient mass error and the already proved explicit slow-variable freezing error.

    lemma unfolded_residue_density_error
        {I : Set ℝ} {J₀ : ℝ → ℝ} {J : UnitAddCircle → ℝ} {o : ℝ}
        {F : ℝ × ℝ → ℝ}
        (hJ : ContDiff ℝ ((⊤ : ℕ∞) : WithTop ℕ∞) J₀) (hIo : IsOpen I)
        (hinj : InjOn J₀ I) (hd : ∀ x ∈ I, deriv J₀ x ≠ 0)
        (hF : ContDiff ℝ ((⊤ : ℕ∞) : WithTop ℕ∞) F) (hc : HasCompactSupport F)
        (hs : tsupport F ⊆ I ×ˢ univ) {ε : ℝ} (hε : 0 < ε)
        (hz : ∀ a s, |s| < ε → F (a,s) = 0)
        (hj : Measurable J) (hJe : ∀ x ∈ I, J (x : UnitAddCircle) = J₀ x)
        {n P : ℕ} (hn : 0 < n) (hP : 0 < P) (h : ℤ) (S : Finset ℤ)
        (hSN : ∀ k ∈ S, h+k*(P:ℤ) ≠ 0)
        (hST : ∀ k ∉ S, ∀ a, F (a,((h+k*(P:ℤ):ℤ):ℝ)/n) = 0)
    …

77. lemma OAI.ThreeTorus.stationaryWeight_family_of_branch line 1402
78. lemma OAI.ThreeTorus.stationaryWeight_signed_compact_continuous line 1421
79. lemma OAI.ThreeTorus.stationaryWeight_smooth_lift line 1450

    Source documentation

    Smoothness of the actual old-frequency Jacobian, with a compactly supported real lift of the old amplitude (including the new good-arc cutoff). Both positive and negative angular indices are allowed by the injective branch.

    lemma stationaryWeight_smooth_lift {C I : Set ℝ} {J : ℝ → ℝ} {B : ℝ × ℝ → ℂ}
        (hIC : I ⊆ C) (hi : InjOn J C)
        (hJ : ContDiff ℝ ((⊤ : ℕ∞) : WithTop ℕ∞) J) (hIo : IsOpen I)
        (hd : ∀ x ∈ I, deriv J x ≠ 0)
        (hB : ContDiff ℝ ((⊤ : ℕ∞) : WithTop ℕ∞) B) (hc : HasCompactSupport B)
        (hs : tsupport B ⊆ I ×ˢ univ) :
        ContDiff ℝ ((⊤ : ℕ∞) : WithTop ℕ∞)
          (fun p : ℝ × ℝ => stationaryWeight C J (fun x => B (x,p.2)) p.1) ∧
        HasCompactSupport (fun p : ℝ × ℝ => stationaryWeight C J (fun x => B (x,p.2)) p.1) := by
    …

    Mentions: OAI.ThreeTorus.stationaryWeight

80. lemma OAI.ThreeTorus.exists_retained_residue_indices line 1484

    Source documentation

    A finite retained residue index set exists for every positive passage integer. Its zero mode is excluded by the cutoff support, not by a limit.

    lemma exists_retained_residue_indices {χ : ℝ → UnitAddCircle → ℝ}
        (hc : HasCompactSupport χ.uncurry) (hz : ∀ a, χ 0 a = 0)
        {n P : ℕ} (hn : 0 < n) (hP : 0 < P) (h : ℤ) :
        ∃ S : Finset ℤ, (∀ k ∈ S, h+k*(P:ℤ) ≠ 0) ∧
          ∀ k ∉ S, ∀ a, χ (((h+k*(P:ℤ):ℤ):ℝ)/n) a = 0 := by
    …

81. def OAI.ThreeTorus.retainedCircleWeight line 1507

    Source documentation

    The exact circle weights of one retained passage mode.

    noncomputable def retainedCircleWeight (ψ : UnitAddCircle → ℝ) (χ : ℝ → UnitAddCircle → ℝ)
        (c : ℕ → ℤ → UnitAddCircle → ℂ) (n : ℕ) (j : ℤ) (a : UnitAddCircle) : ℝ :=
    …

82. lemma OAI.ThreeTorus.retainedCircleWeight_integrable line 1511
83. lemma OAI.ThreeTorus.retainedCircleWeight_error line 1520
84. lemma OAI.ThreeTorus.retained_unfolded_residue_error line 1547

    Source documentation

    Full L1 unfolded fine-density convergence for actual retained mode weights. The only asymptotic input is the summed Fourier coefficient mass theorem; all pushforward identities, integrability, cutoffs and residue freezing are proved here, for both signs and without any divisibility constraint on n.

    lemma retained_unfolded_residue_error
        {I : Set ℝ} {J₀ : ℝ → ℝ} {J : UnitAddCircle → ℝ} {o : ℝ}
        {F : ℝ × ℝ → ℝ} {W χ : ℝ → UnitAddCircle → ℝ}
        {ψ : UnitAddCircle → ℝ} {c : ℕ → ℤ → UnitAddCircle → ℂ}
        (hJ : ContDiff ℝ ((⊤ : ℕ∞) : WithTop ℕ∞) J₀) (hIo : IsOpen I)
        (hinj : InjOn J₀ I) (hd : ∀ x ∈ I, deriv J₀ x ≠ 0)
        (hF : ContDiff ℝ ((⊤ : ℕ∞) : WithTop ℕ∞) F) (hcF : HasCompactSupport F)
        (hsF : tsupport F ⊆ (Ioc o (o+1) ∩ I) ×ˢ univ)
        {ε : ℝ} (hε : 0 < ε) (hz : ∀ a s, |s| < ε → F (a,s) = 0)
        (hj : Measurable J) (hJe : ∀ x ∈ I, J (x : UnitAddCircle) = J₀ x)
        (hW : Continuous W.uncurry) (hcW : HasCompactSupport W.uncurry)
        (hcc : ∀ n j, Continuous (c n j))
    …

85. lemma OAI.ThreeTorus.retained_unfolded_residue_tendsto line 1626
86. lemma OAI.ThreeTorus.scaled_speed_good_branch line 1671
87. lemma OAI.ThreeTorus.exact_retained_unfolded_residue_tendsto line 1696

    Source documentation

    The fine temporal density assertion of the Passage Lemma for one actual old packet. There are no asymptotic or numerical stationary-phase estimates among the hypotheses: the exact signed Fourier mass theorem supplies them. The smooth real lift F is the cutoff old-frequency Jacobian, with its precise identity stated below.

    lemma exact_retained_unfolded_residue_tendsto
        {A : UnitAddCircle × UnitAddCircle → ℂ} {A₀ : UnitAddCircle → ℝ → ℂ}
        {Pr V : ℝ → ℝ} {m : ℤ} {δ : ℕ → ℝ} {H : ℕ → UnitAddCircle → UnitAddCircle}
        {o l u R : ℝ}
        (hm : m ≠ 0)
        (hH : ∀ n (x : ℝ), H n (x : UnitAddCircle) = ((n:ℝ)*(Pr x+δ n*x) : UnitAddCircle))
        (hA : ∀ a x, x ∈ Ioc o (o+1) → A ((x : UnitAddCircle),a) = A₀ a x)
        (hA₀ : ∀ a, ContDiff ℝ 2 (A₀ a)) (hAc : Continuous A₀.uncurry)
        (hAd : Continuous (fun p : UnitAddCircle × ℝ => deriv (A₀ p.1) p.2))
        (hsupp : ∀ a, support (A₀ a) ⊆ Ioc l u)
        (hlo : o ≤ l) (huo : u ≤ o+1) (hlu : l ≤ u) (hR : 0 < R)
        (hPr : ContDiff ℝ ((⊤ : ℕ∞) : WithTop ℕ∞) Pr)
    …

    Mentions: OAI.ThreeTorus.H

88. lemma OAI.ThreeTorus.stationaryWeight_mul line 1755
89. def OAI.ThreeTorus.stationaryCutoffLift line 1764

    Source documentation

    The actual cutoff old-frequency Jacobian in real coordinates. The first coordinate is the new slow coordinate; the second is the old frequency.

    noncomputable def stationaryCutoffLift (C : Set ℝ) (J : ℝ → ℝ)
        (A : ℝ × ℝ → ℂ) (ψ : ℝ → ℝ) (p : ℝ × ℝ) : ℝ :=
    …

90. lemma OAI.ThreeTorus.stationaryCutoffLift_eq line 1768
91. lemma OAI.ThreeTorus.cutoff_amplitude_regular line 1776
92. lemma OAI.ThreeTorus.stationaryCutoffLift_regular line 1796
93. lemma OAI.ThreeTorus.stationaryWeight_support_subset line 1821
94. lemma OAI.ThreeTorus.stationaryCutoffLift_support line 1833
95. lemma OAI.ThreeTorus.stationaryCutoffLift_zero_near_zero line 1845
96. lemma OAI.ThreeTorus.exists_retained_residue_sequence line 1863
97. lemma OAI.ThreeTorus.exact_cutoff_weight_regular line 1883

    Source documentation

    The cutoff old-frequency Jacobian used in the Passage Lemma has all required regularity, including the frequency gap. These conclusions are derived from the actual smooth amplitude and compact cutoffs.

    lemma exact_cutoff_weight_regular
        {V : ℝ → ℝ} {m : ℤ} {l u R : ℝ} {A₀ : UnitAddCircle → ℝ → ℂ} {ψ₀ : ℝ → ℝ}
        (hm : m ≠ 0) (hR : 0 < R)
        (hV : ContDiff ℝ ((⊤ : ℕ∞) : WithTop ℕ∞) V)
        (hdV : ∀ x ∈ Icc (l-2*R) (u+2*R), 0 < deriv V x)
        (hAr : ContDiff ℝ ((⊤ : ℕ∞) : WithTop ℕ∞)
          (fun p : ℝ × ℝ => A₀ (p.2 : UnitAddCircle) p.1))
        (hsupp : ∀ a, support (A₀ a) ⊆ Icc l u)
        (hψ₀ : ContDiff ℝ ((⊤ : ℕ∞) : WithTop ℕ∞) ψ₀) (hcψ₀ : HasCompactSupport ψ₀)
        (h0 : 0 ∉ (fun x => (m:ℝ)*V x) '' Icc l u) :
        let F := stationaryCutoffLift (Icc (l-R) (u+R)) (fun x => (m:ℝ)*V x)
    …

    Mentions: OAI.ThreeTorus.stationaryCutoffLift

98. lemma OAI.ThreeTorus.exact_passage_unfolded_spectral_limit line 1914

    Source documentation

    Source Passage Lemma, exact unfolded spectral conclusion for any residue of one signed packet. The Fourier coefficients, cutoff weight and fine kernel are all the displayed source objects. Smooth compact lift, finite retention and frequency-gap obligations are produced here, not postulated as analytic estimates. Geometry and physical Fourier transport are separate proved lemmas.

    lemma exact_passage_unfolded_spectral_limit
        {A : UnitAddCircle × UnitAddCircle → ℂ} {A₀ : UnitAddCircle → ℝ → ℂ}
        {Pr V : ℝ → ℝ} {m : ℤ} {δ : ℕ → ℝ} {H : ℕ → UnitAddCircle → UnitAddCircle}
        {o l u R : ℝ}
        (hm : m ≠ 0)
        (hH : ∀ n (x : ℝ), H n (x : UnitAddCircle) = ((n:ℝ)*(Pr x+δ n*x) : UnitAddCircle))
        (hA : ∀ a x, x ∈ Ioc o (o+1) → A ((x : UnitAddCircle),a) = A₀ a x)
        (hA₀ : ∀ a, ContDiff ℝ 2 (A₀ a)) (hAc : Continuous A₀.uncurry)
        (hAd : Continuous (fun p : UnitAddCircle × ℝ => deriv (A₀ p.1) p.2))
        (hAr : ContDiff ℝ ((⊤ : ℕ∞) : WithTop ℕ∞)
          (fun p : ℝ × ℝ => A₀ (p.2 : UnitAddCircle) p.1))
        (hsupp : ∀ a, support (A₀ a) ⊆ Ioc l u)
    …

    Mentions: OAI.ThreeTorus.H

99. def OAI.ThreeTorus.periodizedReal line 1989

    Source documentation

    The actual period-one lattice sum used to fold an unfolded temporal density.

    def periodizedReal (q : ℝ → ℝ) (x : ℝ) : ℝ := ∑' k : ℤ, q (x+k)

100. def OAI.ThreeTorus.foldCircleDensity line 1991
101. lemma OAI.ThreeTorus.measurable_periodizedReal line 1994
102. lemma OAI.ThreeTorus.measurable_foldCircleDensity line 1998
103. lemma OAI.ThreeTorus.foldCircleDensity_coe line 2003
104. def OAI.ThreeTorus.intUnitEquiv line 2007
105. lemma OAI.ThreeTorus.integral_real_eq_lattice line 2010
106. lemma OAI.ThreeTorus.lintegral_real_eq_lattice line 2019
107. lemma OAI.ThreeTorus.integrableOn_periodizedReal line 2028
108. lemma OAI.ThreeTorus.integral_periodizedReal line 2041
109. lemma OAI.ThreeTorus.integrable_foldCircleDensity line 2050
110. lemma OAI.ThreeTorus.integral_foldCircleDensity line 2059
111. lemma OAI.ThreeTorus.quotient_add_int line 2068
112. lemma OAI.ThreeTorus.foldCircleDensity_indicator line 2073
113. lemma OAI.ThreeTorus.foldCircleDensity_pushforward line 2093

     Source documentation

     Folding is exactly pushforward under the quotient, not a replacement kernel.

     lemma foldCircleDensity_pushforward {q : ℝ → ℝ} (hm : Measurable q) (hq : Integrable q) :
         ((volume : Measure ℝ).withDensityᵥ q).map (fun x : ℝ => (x:UnitAddCircle)) =
           AddCircle.haarAddCircle.withDensityᵥ (foldCircleDensity q) := by
     …

     Mentions: OAI.ThreeTorus.foldCircleDensity

114. lemma OAI.ThreeTorus.foldCircleDensity_l1_difference line 2105
115. lemma OAI.ThreeTorus.foldCircleDensity_l1_tendsto line 2113
116. lemma OAI.ThreeTorus.periodizedReal_add_int line 2123
117. lemma OAI.ThreeTorus.foldCircleDensity_coe_all line 2135

     Source documentation

     The displayed lattice formula holds for every real representative.

     lemma foldCircleDensity_coe_all (q : ℝ → ℝ) (x : ℝ) :
         foldCircleDensity q (x:UnitAddCircle) = ∑' k : ℤ, q (x+k) := by
     …

     Mentions: OAI.ThreeTorus.foldCircleDensity

118. lemma OAI.ThreeTorus.measurable_branchDensity_smooth line 2153
119. lemma OAI.ThreeTorus.measurable_circleDensityLift line 2178
120. lemma OAI.ThreeTorus.measurable_unfoldedModeDensity line 2182
121. lemma OAI.ThreeTorus.passageBranchKernel_regular line 2190
122. lemma OAI.ThreeTorus.fineResidueKernel_regular line 2214
123. lemma OAI.ThreeTorus.retained_unfolded_regular line 2234
124. lemma OAI.ThreeTorus.retained_circle_of_unfolded_limit line 2259

     Source documentation

     Exact contraction of the retained unfolded residue limit to the temporal circle. In particular the quotient's offsets are not discarded.

     lemma retained_circle_of_unfolded_limit
         {J : ℝ → ℝ} {I : Set ℝ} {F : ℝ × ℝ → ℝ}
         (hJ : ContDiff ℝ ((⊤ : ℕ∞) : WithTop ℕ∞) J) (hIo : IsOpen I)
         (hinj : InjOn J I) (hd : ∀ x ∈ I, deriv J x ≠ 0)
         (hF : ContDiff ℝ ((⊤ : ℕ∞) : WithTop ℕ∞) F) (hcF : HasCompactSupport F)
         (hsF : tsupport F ⊆ I ×ˢ univ) {ε : ℝ} (hε : 0 < ε)
         (hz : ∀ a s, |s| < ε → F (a,s) = 0)
         {ψ : UnitAddCircle → ℝ} {χ : ℝ → UnitAddCircle → ℝ}
         {c : ℕ → ℤ → UnitAddCircle → ℂ}
         (hψ : Continuous ψ) (hχ : Continuous χ.uncurry) (hc : ∀ n j, Continuous (c n j))
         (o : ℝ) {P : ℕ} (hP : 0 < P) (h : ℤ) (S : ℕ → Finset ℤ)
         (hSN : ∀ n, 0 < n → ∀ k ∈ S n, h+k*(P:ℤ) ≠ 0)
     …

125. lemma OAI.ThreeTorus.vectorMeasure_map_comp line 2296
126. lemma OAI.ThreeTorus.foldedModeDensity_pushforward line 2307

     Source documentation

     The folded expression is the density of the actual mode spectral map j(1+J/n)/n modulo one. Thus the circle limit is a spectral-density statement.

     lemma foldedModeDensity_pushforward {q : UnitAddCircle → ℝ} {q₀ J₀ : ℝ → ℝ}
         {J : UnitAddCircle → ℝ} {o : ℝ} {I : Set ℝ}
         (hq : Integrable q AddCircle.haarAddCircle) (hqm : Measurable q₀)
         (hq₀ : ∀ x ∈ Ioc o (o+1), q (x : UnitAddCircle) = q₀ x)
         (hq₀s : support q₀ ⊆ Ioc o (o+1)) (hqs : support q₀ ⊆ I)
         (hj : Measurable J) (hJ : ContDiff ℝ ((⊤ : ℕ∞) : WithTop ℕ∞) J₀)
         (hJe : ∀ x ∈ I, J (x : UnitAddCircle) = J₀ x)
         (hIo : IsOpen I) (hinj : InjOn J₀ I) (hd : ∀ x ∈ I, deriv J₀ x ≠ 0)
         {n j : ℝ} (hn : 0 < n) (hjn : j ≠ 0) :
         (AddCircle.haarAddCircle.withDensityᵥ q).map
             (fun a => (((j+(j/n)*J a)/n : ℝ) : UnitAddCircle)) =
           AddCircle.haarAddCircle.withDensityᵥ
     …

127. lemma OAI.ThreeTorus.exact_passage_circle_spectral_limit line 2350

     Source documentation

     Source Passage Lemma, exact unfolded spectral conclusion for any residue of one signed packet. The Fourier coefficients, cutoff weight and fine kernel are all the displayed source objects. Smooth compact lift, finite retention and frequency-gap obligations are produced here, not postulated as analytic estimates. Geometry and physical Fourier transport are separate proved lemmas.

     lemma exact_passage_circle_spectral_limit
         {A : UnitAddCircle × UnitAddCircle → ℂ} {A₀ : UnitAddCircle → ℝ → ℂ}
         {Pr V : ℝ → ℝ} {m : ℤ} {δ : ℕ → ℝ} {H : ℕ → UnitAddCircle → UnitAddCircle}
         {o l u R : ℝ}
         (hm : m ≠ 0)
         (hH : ∀ n (x : ℝ), H n (x : UnitAddCircle) = ((n:ℝ)*(Pr x+δ n*x) : UnitAddCircle))
         (hA : ∀ a x, x ∈ Ioc o (o+1) → A ((x : UnitAddCircle),a) = A₀ a x)
         (hA₀ : ∀ a, ContDiff ℝ 2 (A₀ a)) (hAc : Continuous A₀.uncurry)
         (hAd : Continuous (fun p : UnitAddCircle × ℝ => deriv (A₀ p.1) p.2))
         (hAr : ContDiff ℝ ((⊤ : ℕ∞) : WithTop ℕ∞)
           (fun p : ℝ × ℝ => A₀ (p.2 : UnitAddCircle) p.1))
         (hsupp : ∀ a, support (A₀ a) ⊆ Ioc l u)
     …

     Mentions: OAI.ThreeTorus.H