OAI/Combinatorics/TreewidthL1/Particles.lean

GitHub source file

76 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.BoundedTreewidthL1.pairUpdate line 13
2. inductive OAI.BoundedTreewidthL1.ParticleReachable line 18

   Source documentation

   Finite update histories; there is no bound on the number of updates.

   inductive ParticleReachable : (ι → ℝ) → Prop
     | zero : ParticleReachable (fun _ => 0)
     | step {a : ι → ℝ} (ha : ParticleReachable a)
         (i j : ι) (hij : i ≠ j) (e : ℝ) (he : |e| ≤ 1) :
         ParticleReachable (pairUpdate a i j e)
   
   /-- The quadratic subset-sum invariant controlling particle bounds.
   Subtractions are real. In particular the bound at the full set is exactly zero. -/

   Mentions: OAI.BoundedTreewidthL1.pairUpdate

3. def OAI.BoundedTreewidthL1.ParticleInvariant line 26

   Source documentation

   The quadratic subset-sum invariant controlling particle bounds. Subtractions are real. In particular the bound at the full set is exactly zero.

   def ParticleInvariant (a : ι → ℝ) : Prop :=
   …

4. lemma OAI.BoundedTreewidthL1.sum_pairUpdate line 40
5. lemma OAI.BoundedTreewidthL1.pairUpdate_swap line 49
6. lemma OAI.BoundedTreewidthL1.ParticleInvariant.zero line 57
7. lemma OAI.BoundedTreewidthL1.ParticleInvariant.update_one line 66
8. lemma OAI.BoundedTreewidthL1.ParticleInvariant.update line 87
9. theorem OAI.BoundedTreewidthL1.particle_reachable_invariant line 106
10. theorem OAI.BoundedTreewidthL1.particle_reachable_abs_le line 113

    Source documentation

    Exact scalar bound used for the slopes AND absolute heights of particles.

    theorem particle_reachable_abs_le {a : ι → ℝ} (ha : ParticleReachable a) (i : ι) :
        |a i| ≤ (Fintype.card ι : ℝ) - 1 := by
    …

    Mentions: OAI.BoundedTreewidthL1.ParticleReachable

11. def OAI.BoundedTreewidthL1.functionPairUpdate line 140
12. inductive OAI.BoundedTreewidthL1.FunctionParticleReachable line 144
13. lemma OAI.BoundedTreewidthL1.functionPairUpdate_left line 153
14. lemma OAI.BoundedTreewidthL1.functionPairUpdate_right line 160
15. lemma OAI.BoundedTreewidthL1.functionPairUpdate_other line 167
16. lemma OAI.BoundedTreewidthL1.functionPairUpdate_value_normalized line 174
17. lemma OAI.BoundedTreewidthL1.functionPairUpdate_difference_normalized line 184
18. lemma OAI.BoundedTreewidthL1.function_particles_normalized_values line 195
19. lemma OAI.BoundedTreewidthL1.function_particles_normalized_differences line 206
20. theorem OAI.BoundedTreewidthL1.function_particles_height_bound line 218
21. theorem OAI.BoundedTreewidthL1.function_particles_difference_bound line 225
22. theorem OAI.BoundedTreewidthL1.function_particles_metric_bound line 234
23. def OAI.BoundedTreewidthL1.particleTrace line 252

    Source documentation

    The exact zero-error combined symmetric trace carried by a particle list.

    noncomputable def particleTrace (M : ℝ) (F : ι → V → ℝ) (P : Finset V) :
        Measure (P → Bool) := ∑ i, cutTrace (symmetrizeCut (sweep M (F i))) P

    Mentions: OAI.BoundedTreewidthL1.cutTrace, OAI.BoundedTreewidthL1.symmetrizeCut, OAI.BoundedTreewidthL1.sweep

24. lemma OAI.BoundedTreewidthL1.exists_weak_order line 259

    Source documentation

    Any reservation set of size at most 2q leaves two particles with a common weak order, and the actual affine update preserves the complete bag law and every reserved function. The pair is chosen before the perturbation; the universal quantifier on g expresses that fact.

    lemma exists_weak_order
        {V : Type treewidthLevel1} [Fintype V]
        (P : Finset V) (F : V → ℝ) :
        ∃ e : Fin P.card ≃ P, Monotone (fun i => F (e i)) := by
    …

25. lemma OAI.BoundedTreewidthL1.free_common_order line 279
26. lemma OAI.BoundedTreewidthL1.cutTrace_symmetrize line 300
27. lemma OAI.BoundedTreewidthL1.symmetrize_add line 309
28. lemma OAI.BoundedTreewidthL1.sum_eq_of_pair line 315
29. lemma OAI.BoundedTreewidthL1.particleTrace_update line 329
30. theorem OAI.BoundedTreewidthL1.particle_step_realization line 350
31. structure OAI.BoundedTreewidthL1.ReservationPath line 396
32. def OAI.BoundedTreewidthL1.ReservationPath.inclusive line 405
33. def OAI.BoundedTreewidthL1.ParticleSchedule.before line 415
34. def OAI.BoundedTreewidthL1.ParticleSchedule.occupied line 418
35. def OAI.BoundedTreewidthL1.ParticleSchedule.pickPair line 424

    Source documentation

    A deterministic pair selection using only pre-launch data. Classical choice here is a fixed function of the finite eligible-pair set, not of the fresh noise.

    noncomputable def pickPair (P : Finset V) (C : Finset ι) (F : ι → V → ℝ) : ι × ι := by
    …

36. def OAI.BoundedTreewidthL1.ParticleSchedule.RunEquations line 430
37. lemma OAI.BoundedTreewidthL1.ParticleSchedule.occupied_card line 436
38. lemma OAI.BoundedTreewidthL1.ParticleSchedule.occupied_update line 446
39. lemma OAI.BoundedTreewidthL1.ParticleSchedule.pickPair_spec line 455
40. lemma OAI.BoundedTreewidthL1.ParticleSchedule.finite_run line 466
41. theorem OAI.BoundedTreewidthL1.ParticleSchedule.scheduled_particle_realization line 499
42. lemma OAI.BoundedTreewidthL1.ParticleSchedule.measurable_weak_order line 604
43. def OAI.BoundedTreewidthL1.ParticleSchedule.selectEligible line 621
44. lemma OAI.BoundedTreewidthL1.ParticleSchedule.measurable_selectEligible line 626
45. lemma OAI.BoundedTreewidthL1.ParticleSchedule.measurable_eligibility line 631
46. lemma OAI.BoundedTreewidthL1.ParticleSchedule.pickPair_eq_selectEligible line 651
47. lemma OAI.BoundedTreewidthL1.ParticleSchedule.measurable_pickPair line 661
48. lemma OAI.BoundedTreewidthL1.ParticleSchedule.measurable_occupied line 667
49. lemma OAI.BoundedTreewidthL1.ParticleSchedule.measurable_selected line 689
50. lemma OAI.BoundedTreewidthL1.ParticleSchedule.measurable_pairUpdate line 705
51. lemma OAI.BoundedTreewidthL1.ParticleSchedule.run_measurable line 728

    Source documentation

    Measurability follows from the deterministic causal equations, for EVERY pointwise realization. There is no assertion that an arbitrary choice operator on an infinite real-valued space is measurable.

    lemma run_measurable (R : ReservationPath) (P : ℕ → Finset V)
        (g : Ω → ℕ → V → ℝ) (hg : ∀ t v, Measurable (fun ω => g ω t v)) (n : ℕ)
        (F : Ω → ℕ → ι → V → ℝ) (p : Ω → ℕ → ι × ι)
        (hrun : ∀ ω, RunEquations R P (g ω) n (F ω) (p ω)) :
        (∀ t ≤ n, ∀ i v, Measurable (fun ω => F ω t i v)) ∧
        (∀ t < n, Measurable (fun ω => p ω t)) := by
    …

    Mentions: OAI.BoundedTreewidthL1.ReservationPath, OAI.BoundedTreewidthL1.ParticleSchedule.RunEquations

52. theorem OAI.BoundedTreewidthL1.ParticleSchedule.measurable_particle_run line 779
53. lemma OAI.BoundedTreewidthL1.ParticleSchedule.measurable_threshold_joint line 795
54. lemma OAI.BoundedTreewidthL1.ParticleSchedule.measurable_sweep_real line 810
55. lemma OAI.BoundedTreewidthL1.ParticleSchedule.measurable_symmetrize_sweep_real line 821
56. instance OAI.BoundedTreewidthL1.ParticleSchedule.finite_cutTrace line 835
57. instance OAI.BoundedTreewidthL1.ParticleSchedule.finite_particleTrace line 840
58. lemma OAI.BoundedTreewidthL1.ParticleSchedule.particle_real_sum line 845
59. lemma OAI.BoundedTreewidthL1.ParticleSchedule.measurable_particleTrace_real line 854
60. lemma OAI.BoundedTreewidthL1.ParticleSchedule.symmetrize_sweep_mass line 870
61. lemma OAI.BoundedTreewidthL1.ParticleSchedule.particleTrace_mass line 879
62. lemma OAI.BoundedTreewidthL1.ParticleSchedule.integrable_particleTrace_real line 889
63. theorem OAI.BoundedTreewidthL1.ParticleSchedule.measurable_branch_cut_laws line 900
64. def OAI.BoundedTreewidthL1.ParticleSchedule.restrictBagCut line 926

    Source documentation

    Literal restriction of a bag assignment to a smaller bag.

    def restrictBagCut (P Q : Finset V) (h : Q ⊆ P) (a : P → Bool) : Q → Bool :=
    …

65. lemma OAI.BoundedTreewidthL1.ParticleSchedule.particleTrace_restrict line 929
66. theorem OAI.BoundedTreewidthL1.ParticleSchedule.compatible_measurable_branch line 943
67. def OAI.BoundedTreewidthL1.ParticleBatch.usedPairs line 1004
68. def OAI.BoundedTreewidthL1.ParticleBatch.launchBatch line 1009

    Source documentation

    Launch all new active keys at one interface, reserving a pair immediately before proceeding to the next key. Retained keys are supplied in C.

    noncomputable def launchBatch (P : Finset V) : (l : List J) → (C : Finset J) →
        (F : ι → V → ℝ) → (p : J → ι × ι) → (g : J → V → ℝ) →
        (ι → V → ℝ) × (J → ι × ι)
      | [], _, F, p, _ => (F,p)
      | a :: l, C, F, p, g =>
        let z := pickPair P (usedPairs C p) F
    …

    Mentions: OAI.BoundedTreewidthL1.ParticleBatch.usedPairs

69. lemma OAI.BoundedTreewidthL1.ParticleBatch.usedPairs_card line 1018
70. lemma OAI.BoundedTreewidthL1.ParticleBatch.usedPairs_mono line 1029
71. lemma OAI.BoundedTreewidthL1.ParticleBatch.usedPairs_update line 1036
72. lemma OAI.BoundedTreewidthL1.ParticleBatch.first_mem_used line 1045
73. lemma OAI.BoundedTreewidthL1.ParticleBatch.second_mem_used line 1051
74. theorem OAI.BoundedTreewidthL1.ParticleBatch.launchBatch_correct line 1060

    Source documentation

    The reservation-preserving finite batch required by the co-bag active-scale construction. No bound on the total number of updates is imposed.

    theorem launchBatch_correct (k q : ℕ)
        (hN : Fintype.card ι = 2*q + k.factorial + 2)
        (P : Finset V) (hP : P.card ≤ k) (l : List J) (C : Finset J)
        (hl : l.Nodup) (hfresh : ∀ a ∈ l, a ∉ C)
        (hcount : (C ∪ l.toFinset).card ≤ q)
        (d : V → V → ℝ) (L H Δ : ℝ) (hH : 0 < H) (hΔ : 0 < Δ)
        (F : ι → V → ℝ) (p : J → ι × ι)
        (hF : FunctionParticleReachable d L H F) (g : J → V → ℝ)
        (hLip : ∀ a ∈ l, ∀ u v, |g a u - g a v| ≤ L*d u v)
        (hHeight : ∀ a ∈ l, ∀ v, |g a v| ≤ H)
        (hzero : ∀ a ∈ l, ∀ v ∈ P, g a v = 0) :
        let out := launchBatch P l C F p g
    …

    Mentions: OAI.BoundedTreewidthL1.FunctionParticleReachable, OAI.BoundedTreewidthL1.ParticleBatch.launchBatch

75. lemma OAI.BoundedTreewidthL1.ParticleBatch.measurable_usedPairs line 1171
76. theorem OAI.BoundedTreewidthL1.ParticleBatch.measurable_launchBatch line 1183

    Source documentation

    The exact finite multi-launch scheduler is measurable; all pair choice is finite deterministic selection, not choice on the real sample space.

    theorem measurable_launchBatch (P : Finset V) (l : List J) (C : Finset J)
        (F : Ω → ι → V → ℝ) (p : Ω → J → ι × ι) (g : Ω → J → V → ℝ)
        (hF : ∀ i v, Measurable (fun ω => F ω i v))
        (hp : ∀ a, Measurable (fun ω => p ω a))
        (hg : ∀ a v, Measurable (fun ω => g ω a v)) :
        Measurable (fun ω => launchBatch P l C (F ω) (p ω) (g ω)) := by
    …

    Mentions: OAI.BoundedTreewidthL1.ParticleBatch.launchBatch