OAI/Dynamics/ThreeTorus/TrackedPackets.lean

GitHub source file

80 declarations, 0 contain sorry, 0 declared as axioms

Refresh and residue estimates, physical aggregates, tracked producers, pair/color aggregates, and colored states.

  1. lemma OAI.ThreeTorus.sum_fibers_univ line 20
  2. lemma OAI.ThreeTorus.sum_selected_fibers line 27
  3. lemma OAI.ThreeTorus.residue_total_error line 37
  4. lemma OAI.ThreeTorus.residue_selected_error line 51
  5. lemma OAI.ThreeTorus.selected_coefficient_error line 65
  6. lemma OAI.ThreeTorus.refresh_transmit_pointwise line 96

    Source documentation

    Pointwise colored version, before integrating. The exact fraction is the fraction of selected refreshed residue classes.

    lemma refresh_transmit_pointwise {ι κ : Type*} [Fintype ι] [Fintype κ] [DecidableEq κ] [Nonempty κ]
    (r : ι → κ) (H : Finset κ) (p : ι → ℝ) (c : ι → ℂ) (a e : ℂ)
    (q : ℝ) {γ ρ A : ℝ} (hγ : 0 ≤ γ) (hρ : 0 ≤ ρ)
    (hp : ∀ i, 0 ≤ p i) (he : ‖e‖ ≤ 1) (ha : ‖a‖ ≤ A)
    (hmatch : ∀ i, p i ≠ 0 → ‖c i-a‖ ≤ ρ) :
    |(∑ i, p i)+2*γ*(e*(∑ i, if r i ∈ H then (p i:ℂ)*c i else 0)).re-
      q*(1+2*(γ*(H.card:ℝ)/Fintype.card κ)*(e*a).re)| ≤
      (1+2*γ*A)*(∑ h, |(∑ i, if r i = h then p i else 0)-q/Fintype.card κ|)+
      2*γ*ρ*(∑ i, p i) := by
…

    Mentions: OAI.ThreeTorus.H

  7. def OAI.ThreeTorus.refreshResidueError line 142

    Source documentation

    Summed residue discrepancy, for one color.

    def refreshResidueError {ι κ : Type*} [Fintype ι] [Fintype κ] [DecidableEq κ]
    (r : ι → κ) (p : ι → UnitAddCircle → ℝ) (q : UnitAddCircle → ℝ) (z : UnitAddCircle) : ℝ :=
…
  8. def OAI.ThreeTorus.refreshSignalAggregate line 146
  9. lemma OAI.ThreeTorus.continuous_refreshResidueError line 151
  10. lemma OAI.ThreeTorus.continuous_refreshSignalAggregate line 163
  11. theorem OAI.ThreeTorus.refresh_transmit_L1 line 179

    Source documentation

    Exact manuscript constant, for the actual selected residue family. Here g is any final transmission density; its L1 mismatch with the explicit signal aggregate is retained as T, not silently dropped.

    theorem refresh_transmit_L1 {ι κ : Type*} [Fintype ι] [Fintype κ]
    [DecidableEq κ] [Nonempty κ]
    (r : ι → κ) (H : Finset κ) {p : ι → UnitAddCircle → ℝ} (c : ι → ℂ)
    {a e : UnitAddCircle → ℂ} {q g : UnitAddCircle → ℝ} {γ ρ A : ℝ}
    (hp : ∀ i, Continuous (p i)) (ha : Continuous a) (he : Continuous e)
    (hq : Continuous q) (hg : Continuous g)
    (hγ : 0 ≤ γ) (hρ : 0 ≤ ρ) (hp0 : ∀ i z, 0 ≤ p i z)
    (he1 : ∀ z, ‖e z‖ ≤ 1) (haA : ∀ z, ‖a z‖ ≤ A)
    (hmatch : ∀ i z, p i z ≠ 0 → ‖c i-a z‖ ≤ ρ) :
    (∫ z, |g z-q z*(1+2*(γ*(H.card:ℝ)/Fintype.card κ)*(e z*a z).re)| ∂phaseHaar) ≤
      (∫ z, |g z-refreshSignalAggregate r H p c γ e z| ∂phaseHaar)+
      (1+2*γ*A)*(∫ z, refreshResidueError r p q z ∂phaseHaar)+
…

    Mentions: OAI.ThreeTorus.H, OAI.ThreeTorus.phaseHaar, OAI.ThreeTorus.refreshSignalAggregate, OAI.ThreeTorus.refreshResidueError

  12. def OAI.ThreeTorus.signalResidue line 243
  13. lemma OAI.ThreeTorus.signalResidue_eq_iff line 246
  14. def OAI.ThreeTorus.signalUnitResidues line 260
  15. lemma OAI.ThreeTorus.mem_signalUnitResidues line 264
  16. lemma OAI.ThreeTorus.signalResidue_mem_units line 269
  17. lemma OAI.ThreeTorus.signalUnitResidues_card_pos line 275
  18. lemma OAI.ThreeTorus.signalUnitResidues_card line 283

    Source documentation

    The selected finite residue classes are exactly the source unit group.

    lemma signalUnitResidues_card (P : ℕ) [NeZero P] :
    (signalUnitResidues P).card = Fintype.card (ZMod P)ˣ := by
…

    Mentions: OAI.ThreeTorus.signalUnitResidues

  19. def OAI.ThreeTorus.refreshedStrength line 304

    Source documentation

    The source's exact positive strength after residue refresh.

    def refreshedStrength (P : ℕ) [NeZero P] (γ : ℝ) : ℝ :=
…
  20. lemma OAI.ThreeTorus.refreshedStrength_eq_unit_fraction line 307
  21. lemma OAI.ThreeTorus.refreshedStrength_pos line 311
  22. lemma OAI.ThreeTorus.refreshedStrength_le line 317
  23. lemma OAI.ThreeTorus.signal_sum_aggregate line 325
  24. def OAI.ThreeTorus.outputVector line 361
  25. def OAI.ThreeTorus.outputDensity line 365
  26. lemma OAI.ThreeTorus.continuous_outputDensity line 369
  27. lemma OAI.ThreeTorus.outputDensity_nonneg line 373
  28. lemma OAI.ThreeTorus.continuous_outputVector line 377
  29. lemma OAI.ThreeTorus.outputVector_eq_retained line 383
  30. lemma OAI.ThreeTorus.outputVector_spectral_moment line 398
  31. lemma OAI.ThreeTorus.integral_abs_sum_sub_le line 424

    Source documentation

    L1 error of a finite sum, with continuity discharging integrability.

    lemma integral_abs_sum_sub_le {ι : Type*} [Fintype ι]
    {p q : ι → UnitAddCircle → ℝ} (hp : ∀ i, Continuous (p i)) (hq : ∀ i, Continuous (q i)) :
    (∫ z, |(∑ i, p i z)-(∑ i, q i z)| ∂phaseHaar) ≤
      ∑ i, ∫ z, |p i z-q i z| ∂phaseHaar := by
…

    Mentions: OAI.ThreeTorus.phaseHaar

  32. theorem OAI.ThreeTorus.exists_signal_tracked_family line 454
  33. theorem OAI.ThreeTorus.exists_neutral_tracked_family line 565
  34. theorem OAI.ThreeTorus.exists_neutral_geometry_state line 664
  35. theorem OAI.ThreeTorus.exists_signal_geometry_state line 687
  36. lemma OAI.ThreeTorus.normalized_band_under_drift line 736
  37. theorem OAI.ThreeTorus.coefficient_match_drift_budget line 743
  38. def OAI.ThreeTorus.pairOutputVector line 789
  39. def OAI.ThreeTorus.pairOutputDensity line 794
  40. lemma OAI.ThreeTorus.continuous_pairOutputVector line 799
  41. lemma OAI.ThreeTorus.continuous_pairOutputDensity line 804
  42. lemma OAI.ThreeTorus.transmission_sum_budget line 809
  43. lemma OAI.ThreeTorus.transmission_pair_physical line 826
  44. lemma OAI.ThreeTorus.transmission_pair_density line 847
  45. lemma OAI.ThreeTorus.refresh_pair_error_budgets line 862

    Source documentation

    Budget choice independent of passage integers and all future packet lists.

    lemma refresh_pair_error_budgets {γ ω A M ε : ℝ}
    (hγ : 0 ≤ γ) (hω : 0 ≤ ω) (hA : 0 ≤ A) (_hM : 0 ≤ M) (hε : 0 < ε) :
    ∃ κ r t : ℝ, 0 < κ ∧ 0 < r ∧ 0 < t ∧ 2*r+2*t < ε ∧
      ∀ m E T : ℝ, 0 ≤ m → m ≤ M → 0 ≤ E → E < r → T < t →
        T+(1+2*γ*A)*E+2*γ*(ω+κ)*(m+E) < 2*γ*ω*m+ε := by
…
  46. lemma OAI.ThreeTorus.finite_circle_coefficients_bound line 900
  47. lemma OAI.ThreeTorus.refresh_residue_integral_eq line 908
  48. theorem OAI.ThreeTorus.exists_refresh_transmit_state line 932

    Source documentation

    Actual refresh/transmit state, with the exact positive strength fixed before all data and error budgets. Each input packet can carry its original color's continuous coefficient; finite color grouping is by summation.

    theorem exists_refresh_transmit_state
    {b D : ℝ} (hb : 0 < b) (hbD : b < D)
    {d : ℝ → ℂ} (hd : ContDiff ℝ ((⊤ : ℕ∞) : WithTop ℕ∞) d)
    (hdc : HasCompactSupport d) (hdr : ∀ v, d (-v) = starRingEnd ℂ (d v))
    (hd0 : d 0 = 0) (hds : support d ⊆ Icc (-D) D) :
    ∃ L : ℕ, ∃ γ₀ : ℝ, 2 ≤ L ∧ D/b < L ∧ 0 < γ₀ ∧
      ∀ γ : ℝ, 0 < γ → γ ≤ γ₀ →
      (∀ v, 2*γ*‖d v‖ ≤ 1/2) ∧
      ∀ (ι : Type u) [Fintype ι], ∀ (F : PassagePackets ι),
      Injective F.m → F.SpareIndependent → ∀ B : ℝ, 0 < B →
      ∀ margin : ℝ, 0 < margin →
      (∀ i, b+margin ≤ |(F.m i:ℝ)/B| ∧ |(F.m i:ℝ)/B| ≤ D-margin) →
…

    Mentions: OAI.ThreeTorus.PassagePackets

  49. def OAI.ThreeTorus.colorVector line 1076
  50. def OAI.ThreeTorus.colorDensity line 1079
  51. lemma OAI.ThreeTorus.continuous_colorVector line 1082
  52. lemma OAI.ThreeTorus.continuous_colorDensity line 1088
  53. lemma OAI.ThreeTorus.colorDensity_nonneg line 1094
  54. lemma OAI.ThreeTorus.colorDensity_mass line 1100
  55. lemma OAI.ThreeTorus.colorVector_pair line 1111
  56. lemma OAI.ThreeTorus.colorDensity_pair line 1124
  57. lemma OAI.ThreeTorus.colored_physical_bound line 1137
  58. lemma OAI.ThreeTorus.colored_density_bound line 1158
  59. theorem OAI.ThreeTorus.color_pair_errors line 1178

    Source documentation

    Aggregate the SAME literal two-passage output state, without changing its colors or choosing spectral densities independently.

    theorem color_pair_errors {S : ι → Finset ℤ} {T : PassageOutputIndex S → Finset ℤ}
    (F : PassagePackets ι) (K : PassagePackets (PassageOutputIndex T))
    (c : ι → R) (a : R → UnitAddCircle → ℂ) (ha : ∀ r, Continuous (a r))
    {H H' : UnitAddCircle → UnitAddCircle} (hH : Continuous H) (hH' : Continuous H')
    (N : ℕ) (ell : ℝ) {γ ω e ε : ℝ} (he : 0 < e)
    (hε : (Fintype.card ι:ℝ)*e < ε) (hε' : (Fintype.card ι:ℝ)^2*e < ε)
    (h : ∀ i,
      physicalError (packet (F.m i) (F.A i))
        (pairOutputVector K i ∘ passageChart H' ∘ passageChart H) < e ∧
      (∫ z, |pairOutputDensity K i z-F.density i z*
        (1+2*ell*(fourier (-1) ((N:ℤ) • z)*a (c i) z).re)| ∂phaseHaar) <
          2*γ*ω*(∫ z, |F.density i z| ∂phaseHaar)+e) :
…

    Mentions: OAI.ThreeTorus.PassageOutputIndex, OAI.ThreeTorus.PassagePackets, OAI.ThreeTorus.H, OAI.ThreeTorus.physicalError, OAI.ThreeTorus.packet, OAI.ThreeTorus.pairOutputVector, OAI.ThreeTorus.passageChart, OAI.ThreeTorus.pairOutputDensity, OAI.ThreeTorus.phaseHaar

  60. theorem OAI.ThreeTorus.core_coefficient_drift_budget line 1243

    Source documentation

    Uniform continuity controls the entire next packet core, so this estimate can be used as the input hypothesis of a subsequent actual passage.

    theorem core_coefficient_drift_budget {ι : Type*} [Fintype ι]
    (F : PassagePackets ι) {d : ℝ → ℂ} (hd : Continuous d) (hdc : HasCompactSupport d)
    (a : ι → UnitAddCircle → ℂ) (ha : ∀ i, Continuous (a i))
    {B ω e : ℝ} (he : 0 < e)
    (hmatch : ∀ i x, x ∈ F.core i →
      ‖d ((F.m i:ℝ)/B)-a i ((F.m i:ℝ)*F.V x:UnitAddCircle)‖ ≤ ω) :
    ∃ η : ℝ, 0 < η ∧ ∀ (κ : Type*) (G : PassagePackets κ) (parent : κ → ι) (B' : ℝ),
      StateTracks F G parent B B' η →
      ∀ j y, ‖d ((G.m j:ℝ)/B')-a (parent j) ((G.m j:ℝ)*G.V y:UnitAddCircle)‖ ≤ ω+e := by
…

    Mentions: OAI.ThreeTorus.PassagePackets, OAI.ThreeTorus.StateTracks

  61. lemma OAI.ThreeTorus.StateTracks.band_margin line 1276
  62. structure OAI.ThreeTorus.ColoredState line 1301
  63. def OAI.ThreeTorus.ColoredState.density line 1315
  64. def OAI.ThreeTorus.ColoredState.vector line 1316
  65. lemma OAI.ThreeTorus.ColoredState.density_continuous line 1317
  66. lemma OAI.ThreeTorus.ColoredState.vector_continuous line 1319
  67. lemma OAI.ThreeTorus.ColoredState.density_nonneg line 1321
  68. def OAI.ThreeTorus.ColoredState.InBand line 1324
  69. def OAI.ThreeTorus.ColoredState.Matches line 1328
  70. structure OAI.ThreeTorus.ColoredPair line 1335

    Source documentation

    A pair retaining real passage geometry, not merely a density transition.

    structure ColoredPair {R : Type} (C : ColoredState R) (N : ℕ) where
…

    Mentions: OAI.ThreeTorus.ColoredState

  71. def OAI.ThreeTorus.ColoredPair.output line 1356
  72. def OAI.ThreeTorus.ColoredPair.chart line 1366
  73. lemma OAI.ThreeTorus.ColoredPair.chart_apply line 1368
  74. lemma OAI.ThreeTorus.ColoredPair.chart_continuous line 1370
  75. lemma OAI.ThreeTorus.ColoredPair.chart_preserves line 1373
  76. def OAI.ThreeTorus.ColoredPair.Tracks line 1377
  77. def OAI.ThreeTorus.colorFactor line 1381
  78. lemma OAI.ThreeTorus.continuous_colorFactor line 1385
  79. lemma OAI.ThreeTorus.finite_card_error_budget line 1391
  80. theorem OAI.ThreeTorus.exists_colored_signal line 1404

    Source documentation

    Color errors are as small as desired apart from the explicit coefficient mismatch. Every sufficiently large transmission integer is still available.

    theorem exists_colored_signal {b D : ℝ} (hb : 0 < b) (hbD : b < D)
    {d : ℝ → ℂ} (hd : ContDiff ℝ ((⊤ : ℕ∞) : WithTop ℕ∞) d)
    (hdc : HasCompactSupport d) (hdr : ∀ v, d (-v) = starRingEnd ℂ (d v))
    (hd0 : d 0 = 0) (hds : support d ⊆ Icc (-D) D) :
    ∃ L : ℕ, ∃ γ₀ : ℝ, 2 ≤ L ∧ D/b < L ∧ 0 < γ₀ ∧
      ∀ γ : ℝ, 0 < γ → γ ≤ γ₀ →
      (∀ v, 2*γ*‖d v‖ ≤ 1/2) ∧
      ∀ (R : Type) [DecidableEq R], ∀ (C : ColoredState R),
      ∀ margin : ℝ, 0 < margin → C.InBand b D margin →
      ∀ (a : R → UnitAddCircle → ℂ), (∀ r, Continuous (a r)) →
      ∀ ω : ℝ, 0 ≤ ω → C.Matches d a ω →
      ∀ ε η : ℝ, 0 < ε → 0 < η →
…

    Mentions: OAI.ThreeTorus.ColoredState