OAI/Dynamics/ThreeTorus/PacketStates.lean

GitHub source file

86 declarations, 0 contain sorry, 0 declared as axioms

Closed finite packet states, canonical densities, residue reindexing, anchors, reflection, clipping, and state tracking.

  1. def OAI.ThreeTorus.PassagePackets.core line 19
  2. lemma OAI.ThreeTorus.PassagePackets.core_subset line 21
  3. lemma OAI.ThreeTorus.PassagePackets.core_compact line 24
  4. lemma OAI.ThreeTorus.PassagePackets.support_subset_core line 27
  5. lemma OAI.ThreeTorus.PassagePackets.amplitude_bound line 36
  6. def OAI.ThreeTorus.PassagePackets.carrier line 47

    Source documentation

    Adding an integral carrier changes no temporal eigenfrequency modulo one.

    def carrier (c : ℤ) : PassagePackets ι := { F with
…

    Mentions: OAI.ThreeTorus.PassagePackets

  7. lemma OAI.ThreeTorus.PassagePackets.carrier_spare line 54
  8. lemma OAI.ThreeTorus.PassagePackets.carrier_circle line 57
  9. theorem OAI.ThreeTorus.PassagePackets.tracked_cutoffs line 68

    Source documentation

    Scalar cutoffs with arbitrarily small support tracking error exist for EVERY sufficiently large carrier. Choosing the carrier is therefore still compatible with the signal-law and normalized-index error bounds.

    theorem tracked_cutoffs [Finite ι] (hi : Injective F.m)
    (hmod : F.SpareIndependent) {η : ℝ} (hη : 0 < η) :
    ∀ᶠ c : ℕ in atTop, 0 < c ∧ ∃ χ : ι → ℝ → ℝ,
      (∀ i, ContDiff ℝ ((⊤ : ℕ∞) : WithTop ℕ∞) (χ i) ∧ HasCompactSupport (χ i) ∧
        χ i 0 = 0 ∧ (∀ s, 0 ≤ χ i s ∧ χ i s ≤ 1) ∧
        (∀ s ∈ tsupport (χ i), ∃ x ∈ F.core i, |s-(F.m i:ℝ)*((c:ℝ)+F.V x)| < η) ∧
        ∀ (C : Set ℝ) a s, stationaryWeight C
          (fun x => (F.m i:ℝ)*((c:ℝ)+F.V x)) (F.A₀ i a) s ≠ 0 → χ i s = 1) ∧
      Pairwise (fun i j => Disjoint (tsupport (χ i)) (tsupport (χ j))) := by
…

    Mentions: OAI.ThreeTorus.stationaryWeight

  10. lemma OAI.ThreeTorus.continuous_density_unique line 111
  11. lemma OAI.ThreeTorus.fold_density_nonzero line 122
  12. lemma OAI.ThreeTorus.foldCircleDensity_finsetSum_eq line 136
  13. def OAI.ThreeTorus.PassagePackets.weight line 157
  14. def OAI.ThreeTorus.PassagePackets.density line 160
  15. lemma OAI.ThreeTorus.PassagePackets.weight_nonneg line 162
  16. lemma OAI.ThreeTorus.PassagePackets.density_nonneg line 165
  17. lemma OAI.ThreeTorus.PassagePackets.smooth_zero_lift line 168
  18. lemma OAI.ThreeTorus.PassagePackets.weight_regular line 173
  19. lemma OAI.ThreeTorus.PassagePackets.density_smooth line 198
  20. lemma OAI.ThreeTorus.PassagePackets.density_continuous line 202
  21. lemma OAI.ThreeTorus.PassagePackets.speed_continuous line 205
  22. theorem OAI.ThreeTorus.PassagePackets.density_spectral line 210

    Source documentation

    The canonical density is the spectral measure of the actual angular packet.

    theorem density_spectral (hmod : F.SpareIndependent) (i : ι) :
    packetSpectralMeasure (fun u => (F.periodic.lift u:UnitAddCircle)) (F.m i) (F.A i) =
      AddCircle.haarAddCircle.withDensity (fun z => ENNReal.ofReal (F.density i z)) := by
…

    Mentions: OAI.ThreeTorus.packetSpectralMeasure

  23. lemma OAI.ThreeTorus.PassagePackets.density_marginal line 226
  24. lemma OAI.ThreeTorus.PassagePackets.density_carrier line 233
  25. lemma OAI.ThreeTorus.PassagePackets.density_support line 245

    Source documentation

    A nonzero density value is realized on the true old amplitude support, not merely in the convex hull of its frequency range.

    lemma density_support (i : ι) {z : UnitAddCircle} (hz : F.density i z ≠ 0) :
    ∃ x ∈ support (F.A₀ i 0), ((F.m i:ℝ)*F.V x:UnitAddCircle) = z := by
…
  26. lemma OAI.ThreeTorus.exactRetainedPacketDensity_nonneg line 274
  27. lemma OAI.ThreeTorus.exactRetainedPacketDensity_singleton line 285
  28. lemma OAI.ThreeTorus.exactRetainedPacketDensity_sum_singletons line 294
  29. lemma OAI.ThreeTorus.exactRetainedPacketDensity_filtered_singletons line 325
  30. theorem OAI.ThreeTorus.literal_packet_canonical_density line 353

    Source documentation

    Pointwise, not just a.e., identity of a literal output packet's canonical density. The hypotheses below are only smooth lifts and the displayed literal coefficient/speed identities; no new spectral law is assumed.

    theorem literal_packet_canonical_density {ι : Type*} (F : PassagePackets ι)
    (hmod : F.SpareIndependent) (i : ι)
    {I : Set ℝ} {J : UnitAddCircle → ℝ} {J₀ : ℝ → ℝ}
    {ψ : UnitAddCircle → ℝ} {ψ₀ : ℝ → ℝ} {χ : ℝ → UnitAddCircle → ℝ}
    {m j : ℤ} {n : ℕ} {H : ℕ → UnitAddCircle → UnitAddCircle} {Hl : ℕ → ℝ → ℝ}
    {A : UnitAddCircle × UnitAddCircle → ℂ}
    (hm : F.m i = j) (hamp : F.A i = retainedAmplitude ψ χ m H A n j)
    (hspeed : ∀ a, (F.periodic.lift a:UnitAddCircle) = (((1+J a/n)/n:ℝ):UnitAddCircle))
    (hJc : Continuous 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)
    (hψc : Continuous ψ) (hψ : ContDiff ℝ ((⊤ : ℕ∞) : WithTop ℕ∞) ψ₀)
…

    Mentions: OAI.ThreeTorus.PassagePackets, OAI.ThreeTorus.H, OAI.ThreeTorus.retainedAmplitude

  31. lemma OAI.ThreeTorus.sum_residue_rename line 403
  32. lemma OAI.ThreeTorus.exactRetainedPacketDensity_residue_rename line 433
  33. lemma OAI.ThreeTorus.foldCircleDensity_const_mul line 475
  34. theorem OAI.ThreeTorus.exact_neutral_residue_refresh line 481
  35. theorem OAI.ThreeTorus.exists_simultaneous_neutral_residue_passage line 658

    Source documentation

    The jitter, all packet lists and all cutoffs are fixed before the final passage integer. No primitive, convergence, or spectral data are assumed.

    theorem exists_simultaneous_neutral_residue_passage {ι : Type*} [Fintype ι]
    {A : ι → UnitAddCircle × UnitAddCircle → ℂ} {A₀ : ι → UnitAddCircle → ℝ → ℂ}
    {V : ℝ → ℝ} {m : ι → ℤ} {o l u R : ℝ}
    (hm : ∀ i, m i ≠ 0)
    (hA : ∀ i a x, x ∈ Ioc o (o+1) → A i ((x : UnitAddCircle),a) = A₀ i a x)
    (hA₀ : ∀ i a, ContDiff ℝ 2 (A₀ i a)) (hAc : ∀ i, Continuous (A₀ i).uncurry)
    (hAd : ∀ i, Continuous (fun p : UnitAddCircle × ℝ => deriv (A₀ i p.1) p.2))
    (hAr : ∀ i, ContDiff ℝ ((⊤ : ℕ∞) : WithTop ℕ∞)
      (fun p : ℝ × ℝ => A₀ i (p.2 : UnitAddCircle) p.1))
    (hsupp : ∀ i a, support (A₀ i a) ⊆ Ioc l u)
    (hlo : o ≤ l) (huo : u ≤ o+1) (hlu : l ≤ u) (hR : 0 < R)
    (hp : Periodic V 1) (hV : ContDiff ℝ ((⊤ : ℕ∞) : WithTop ℕ∞) V)
…
  36. theorem OAI.ThreeTorus.eventually_neutral_state_family line 791

    Source documentation

    Full neutral state producer. Both approximation errors may be arbitrarily small. The same output state has all actual spectral moments, exactly disjoint angular indices, and the residue refresh statement.

    theorem eventually_neutral_state_family {ι : Type*} [Fintype ι]
    (F : PassagePackets ι) (hi : Injective F.m) (hmod : F.SpareIndependent)
    {Q : ℕ} (hQ : 0 < Q) {ε τ : ℝ} (hε : 0 < ε) (hτ : 0 < τ) :
    ∀ᶠ c : ℕ in atTop, 0 < c ∧ ∃ δ : ℝ, ∃ cut : LawCutoffs δ, ∃ L : ℝ,
      ∃ χ : ι → ℝ → ℝ, ∃ Δ : ℕ → ℝ, ∃ H : ℕ → UnitAddCircle → UnitAddCircle,
      0 < δ ∧ δ < 1/8 ∧ 0 < L ∧
      (∀ i, ContDiff ℝ ((⊤ : ℕ∞) : WithTop ℕ∞) (χ i) ∧ HasCompactSupport (χ i) ∧
        χ i 0 = 0 ∧ (∀ s, 0 ≤ χ i s ∧ χ i s ≤ 1) ∧
        ∀ s ∈ tsupport (χ i), ∃ x ∈ F.core i,
          |s-(F.m i:ℝ)*((c:ℝ)+F.V x)| < τ) ∧
      Pairwise (fun i j => Disjoint (tsupport (χ i)) (tsupport (χ j))) ∧
      (∀ n, 0 < n → |Δ n| ≤ (n:ℝ)⁻¹) ∧ Tendsto Δ atTop (𝓝 0) ∧
…

    Mentions: OAI.ThreeTorus.PassagePackets, OAI.ThreeTorus.LawCutoffs, OAI.ThreeTorus.H

  37. lemma OAI.ThreeTorus.tracked_cutoffs_fixed_carrier line 979
  38. theorem OAI.ThreeTorus.eventually_neutral_anchor_family line 1009
  39. def OAI.ThreeTorus.pairedCylinderCutoff line 1202
  40. lemma OAI.ThreeTorus.pairedCylinderCutoff_reflect line 1206
  41. lemma OAI.ThreeTorus.pairedCylinderCutoff_smooth line 1211
  42. lemma OAI.ThreeTorus.pairedCylinderCutoff_tsupport line 1218
  43. lemma OAI.ThreeTorus.pairedCylinderCutoff_compact line 1223
  44. lemma OAI.ThreeTorus.pairedCylinderCutoff_disjoint line 1228
  45. lemma OAI.ThreeTorus.pairedCylinderCutoff_bounds line 1236
  46. lemma OAI.ThreeTorus.pairedCylinderCutoff_one line 1244
  47. lemma OAI.ThreeTorus.symmetric_exact_indices line 1259
  48. lemma OAI.ThreeTorus.retainedAmplitude_reflect line 1273
  49. lemma OAI.ThreeTorus.packet_reflect line 1281
  50. lemma OAI.ThreeTorus.retainedPassage_reflect line 1285
  51. def OAI.ThreeTorus.PassagePackets.GoodArc line 1328

    Source documentation

    The entire increasing good arc, including its relation to the lifted support interval. The excluded length is exactly 2*δ.

    def GoodArc (δ : ℝ) : Prop :=
…
  52. structure OAI.ThreeTorus.PassagePackets.Reflection line 1332
  53. lemma OAI.ThreeTorus.PassagePackets.Reflection.involutive line 1339
  54. lemma OAI.ThreeTorus.PassagePackets.Reflection.core line 1342
  55. lemma OAI.ThreeTorus.PassagePackets.Reflection.weight line 1349
  56. lemma OAI.ThreeTorus.foldCircleDensity_reflect line 1358
  57. lemma OAI.ThreeTorus.PassagePackets.Reflection.density line 1371
  58. theorem OAI.ThreeTorus.tracked_symmetric_cutoffs_fixed_carrier line 1380

    Source documentation

    Reflection-compatible, exactly disjoint cutoffs with the full tracking and stationary identity used by the actual neutral and signal producers.

    theorem tracked_symmetric_cutoffs_fixed_carrier {ι : Type*} [Finite ι]
    (F : PassagePackets ι) (hi : Injective F.m) (hmod : F.SpareIndependent)
    {τ : ι → ι} (hr : F.Reflection τ) {c : ℕ}
    (hc : 0 < c ∧ (∀ i x, (F.m i:ℝ)*((c:ℝ)+F.periodic.lift x) ≠ 0) ∧
      ∀ i j x y, (F.m i:ℝ)*((c:ℝ)+F.periodic.lift x) =
        (F.m j:ℝ)*((c:ℝ)+F.periodic.lift y) → F.m i = F.m j)
    {η : ℝ} (hη : 0 < η) :
    0 < c ∧ ∃ χ : ι → ℝ → ℝ,
      (∀ i, ContDiff ℝ ((⊤ : ℕ∞) : WithTop ℕ∞) (χ i) ∧ HasCompactSupport (χ i) ∧
        χ i 0 = 0 ∧ (∀ s, 0 ≤ χ i s ∧ χ i s ≤ 1) ∧
        (∀ s ∈ tsupport (χ i), ∃ x ∈ F.core i, |s-(F.m i:ℝ)*((c:ℝ)+F.V x)| < η) ∧
        ∀ (C : Set ℝ) a s, stationaryWeight C
…

    Mentions: OAI.ThreeTorus.PassagePackets, OAI.ThreeTorus.stationaryWeight

  59. def OAI.ThreeTorus.PassagePackets.cylinderCore line 1446
  60. lemma OAI.ThreeTorus.PassagePackets.cylinderCore_subset line 1449
  61. lemma OAI.ThreeTorus.PassagePackets.cylinderCore_compact line 1455
  62. lemma OAI.ThreeTorus.PassagePackets.support_subset_cylinderCore line 1458
  63. lemma OAI.ThreeTorus.PassagePackets.reflection_cylinderCore line 1461
  64. def OAI.ThreeTorus.PassagePackets.clipped line 1470

    Source documentation

    Multiply the literal torus amplitudes by smooth disjoint cylinder cutoffs and retain their actual lifts. All passage regularity is derived.

    def clipped (q : κ → ι) (χ : κ → ℝ × UnitAddCircle → ℝ)
    (hχ : ∀ k, CylinderSmooth (χ k)) (hc : ∀ k, HasCompactSupport (χ k))
    (hs : ∀ k, support (χ k) ⊆ Ioo F.o (F.o+1) ×ˢ univ) : PassagePackets κ where
…

    Mentions: OAI.ThreeTorus.CylinderSmooth, OAI.ThreeTorus.PassagePackets

  65. lemma OAI.ThreeTorus.PassagePackets.clipped_core_subset line 1528
  66. theorem OAI.ThreeTorus.first_separation_cutoffs line 1554

    Source documentation

    First of the two neutral separations: equal angular modes are separated using the ACTUAL two-dimensional compact coefficient supports. In particular no spare-independence or injectivity of the old mode list is assumed.

    theorem first_separation_cutoffs {ι : Type*} [Finite ι]
    (F : PassagePackets ι)
    (hd : ∀ i j, i ≠ j → F.m i = F.m j → Disjoint (F.cylinderCore i) (F.cylinderCore j))
    (τ : ι → ι) (hτ : Involutive τ) (hr : F.Reflection τ) :
    ∃ c : ℕ, 0 < c ∧ (∀ x : ℝ, (c:ℝ)+F.V x ≠ 0) ∧
      ∃ χ : ι → ℝ → UnitAddCircle → ℝ,
        (∀ i, CylinderSmooth (χ i).uncurry ∧ HasCompactSupport (χ i).uncurry ∧
          (∀ a, χ i 0 a = 0) ∧ (∀ s a, 0 ≤ χ i s a ∧ χ i s a ≤ 1) ∧
          ∀ (C : Set ℝ) a s, stationaryWeight C
            (fun x => (F.m i:ℝ)*((c:ℝ)+F.V x)) (F.A₀ i a) s ≠ 0 → χ i s a = 1) ∧
        Pairwise (fun i j => Disjoint (tsupport (χ i).uncurry) (tsupport (χ j).uncurry)) ∧
        (∀ i s a, χ (τ i) s a = χ i (-s) a) := by
…

    Mentions: OAI.ThreeTorus.PassagePackets, OAI.ThreeTorus.CylinderSmooth, OAI.ThreeTorus.stationaryWeight

  67. def OAI.ThreeTorus.PassagePackets.marginalWeight line 1659
  68. def OAI.ThreeTorus.PassagePackets.marginalDensity line 1663
  69. lemma OAI.ThreeTorus.PassagePackets.marginalWeight_regular line 1665
  70. lemma OAI.ThreeTorus.PassagePackets.marginalDensity_nonneg line 1689
  71. lemma OAI.ThreeTorus.PassagePackets.marginalDensity_measurable line 1693
  72. lemma OAI.ThreeTorus.PassagePackets.marginalDensity_integrable line 1696
  73. theorem OAI.ThreeTorus.PassagePackets.marginalDensity_spectral line 1701

    Source documentation

    The actual old packet spectrum, without spare independence.

    theorem marginalDensity_spectral (i : ι) :
    packetSpectralMeasure (fun u => (F.periodic.lift u:UnitAddCircle)) (F.m i) (F.A i) =
      AddCircle.haarAddCircle.withDensity (fun z => ENNReal.ofReal (F.marginalDensity i z)) := by
…

    Mentions: OAI.ThreeTorus.packetSpectralMeasure

  74. lemma OAI.ThreeTorus.PassagePackets.marginalDensity_carrier line 1719
  75. lemma OAI.ThreeTorus.PassagePackets.marginalDensity_eq line 1736
  76. lemma OAI.ThreeTorus.PassagePackets.weight_integrable line 1753
  77. lemma OAI.ThreeTorus.PassagePackets.density_mass line 1756
  78. lemma OAI.ThreeTorus.PassagePackets.weight_mass_carrier line 1760
  79. lemma OAI.ThreeTorus.PassagePackets.weight_mass_bound line 1764
  80. theorem OAI.ThreeTorus.exists_signal_state_family line 1785
  81. lemma OAI.ThreeTorus.PassagePackets.speed_bound line 2003
  82. lemma OAI.ThreeTorus.PassagePackets.angular_bound line 2008
  83. lemma OAI.ThreeTorus.periodic_real_bound line 2014
  84. theorem OAI.ThreeTorus.literal_output_tracking line 2025

    Source documentation

    The tracked frequency cutoff already controls every retained index, including zero-amplitude packets. The temporal inequality holds for every new speed point.

    theorem literal_output_tracking {ι : Type*} {F : PassagePackets ι}
    {S : ι → Finset ℤ} {G : PassagePackets (PassageOutputIndex S)}
    {χ : ι → ℝ → ℝ} {c n : ℕ} {B D P M Q τ : ℝ} {J : ℝ → ℝ}
    (hc : 0 < c) (hn : 0 < n) (hB : 0 < B)
    (hD : ∀ i, |(F.m i:ℝ)/B| ≤ D) (hP : ∀ x, |F.V x| ≤ P)
    (hM : ∀ i, |(F.m i:ℝ)| ≤ M) (hQ : ∀ x, |J x| ≤ Q)
    (hS : ∀ i j, j ∈ S i → χ i ((j:ℝ)/n) ≠ 0)
    (hχ : ∀ i s, s ∈ tsupport (χ i) → ∃ x ∈ F.core i,
      |s-(F.m i:ℝ)*((c:ℝ)+F.V x)| < τ)
    (hm : ∀ i, G.m i = i.2.val) (hV : G.V = fun x => (1+J x/n)/n) :
    ∀ i, ∃ x ∈ F.core i.1,
      |(G.m i:ℝ)/((n:ℝ)*c*B)-(F.m i.1:ℝ)/B| ≤ D*P/c+τ/((c:ℝ)*B) ∧
…

    Mentions: OAI.ThreeTorus.PassagePackets, OAI.ThreeTorus.PassageOutputIndex

  85. theorem OAI.ThreeTorus.canonical_output_tracking line 2065

    Source documentation

    Every nonzero output density is close to an OLD support point. This uses literal angular indices and speed, not weak convergence of the densities.

    theorem canonical_output_tracking {ι : Type*} {F : PassagePackets ι}
    {S : ι → Finset ℤ} {G : PassagePackets (PassageOutputIndex S)}
    {χ : ι → ℝ → ℝ} {c n : ℕ} {B D P M Q τ : ℝ} {J : ℝ → ℝ}
    (hc : 0 < c) (hn : 0 < n) (hB : 0 < B)
    (hD : ∀ i, |(F.m i:ℝ)/B| ≤ D) (hP : ∀ x, |F.V x| ≤ P)
    (hM : ∀ i, |(F.m i:ℝ)| ≤ M) (hQ : ∀ x, |J x| ≤ Q)
    (hS : ∀ i j, j ∈ S i → χ i ((j:ℝ)/n) ≠ 0)
    (hχ : ∀ i s, s ∈ tsupport (χ i) → ∃ x ∈ F.core i,
      |s-(F.m i:ℝ)*((c:ℝ)+F.V x)| < τ)
    (hm : ∀ i, G.m i = i.2.val) (hV : G.V = fun x => (1+J x/n)/n) :
    ∀ i z, G.density i z ≠ 0 → ∃ x ∈ F.core i.1,
      |(G.m i:ℝ)/((n:ℝ)*c*B)-(F.m i.1:ℝ)/B| ≤ D*P/c+τ/((c:ℝ)*B) ∧
…

    Mentions: OAI.ThreeTorus.PassagePackets, OAI.ThreeTorus.PassageOutputIndex

  86. lemma OAI.ThreeTorus.support_drift_budgets line 2085

    Source documentation

    Large carrier first, small cutoff enlargement second, and final integer last. The bounded jitter only affects this LAST choice.

    lemma support_drift_budgets {D P M B e : ℝ} (hB : 0 < B) (he : 0 < e) :
    ∀ᶠ c : ℕ in atTop, 0 < c ∧ ∀ τ : ℝ, 0 < τ → τ < e/2 →
      D*P/c+τ/((c:ℝ)*B) < e ∧
      ∀ Q : ℝ, ∀ᶠ n : ℕ in atTop, 0 < n ∧ τ+(M*((c:ℝ)+P)+τ)*Q/n < e := by
…