OAI/Combinatorics/TreewidthL1/ReservedTests.lean

GitHub source file

23 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.BoundedTreewidthL1.ReservedTests.part line 13
2. lemma OAI.BoundedTreewidthL1.ReservedTests.part_nonneg line 18
3. lemma OAI.BoundedTreewidthL1.ReservedTests.sum_part line 28
4. lemma OAI.BoundedTreewidthL1.ReservedTests.part_le line 32
5. lemma OAI.BoundedTreewidthL1.ReservedTests.pair_part_le line 40
6. lemma OAI.BoundedTreewidthL1.ReservedTests.part_eq line 54
7. lemma OAI.BoundedTreewidthL1.ReservedTests.departure_isCoupling line 74
8. theorem OAI.BoundedTreewidthL1.ReservedTests.height_test line 81

   Source documentation

   The exact single OLD-particle height test for the real expanded departure coupling. The suffix is the proved interval-resampling response.

   theorem height_test (M : ℝ) (hM : 0 ≤ M) (F : ι → V → ℝ) (P : Finset V)
       (i j r : ι) (hir : r ≠ i) (hjr : r ≠ j)
       (hF : ∀ v, -M ≤ F r v ∧ F r v ≤ M) (z : V) (bags : List (Finset V))
       (f p : State ι V → ℝ) (hf : ∀ a, 0 ≤ f a ∧ f a ≤ 1) (hp : ∀ a, 0 ≤ p a ∧ p a ≤ 1)
       (hresponse : ∀ a : OrderedReservation.Carrier M (F r),
         f (lift M (F r) r a) = OrderedSweepFlow.execute (OrderedReservation.weight M (F r))
           (bags.map (OrderedReservation.traceRank M (F r)))
           (OrderedSweepFlow.labelReal (fun a => a.val z)) a)
       (t : ℝ) (hlo : t ≤ F r z + M) (hhi : t ≤ M - F r z)
       (hgap : ∀ v ∈ P, t ≤ |F r z - F r v|) :
       t/2 ≤ defect (weight M F) (action (weight M F) (departure M F P i j) f) p := by
   …

   Mentions: OAI.BoundedTreewidthL1.OrderedReservation.Carrier, OAI.BoundedTreewidthL1.OrderedSweepFlow.execute, OAI.BoundedTreewidthL1.OrderedReservation.weight, OAI.BoundedTreewidthL1.OrderedReservation.traceRank, OAI.BoundedTreewidthL1.OrderedSweepFlow.labelReal

9. lemma OAI.BoundedTreewidthL1.ReservedTests.sum_marginal_eval line 117
10. lemma OAI.BoundedTreewidthL1.ReservedTests.sweep_trace_marginal_eq line 127
11. def OAI.BoundedTreewidthL1.ReservedTests.traceAverage line 143
12. lemma OAI.BoundedTreewidthL1.ReservedTests.action_average line 148
13. lemma OAI.BoundedTreewidthL1.ReservedTests.fresh_keys line 160
14. lemma OAI.BoundedTreewidthL1.ReservedTests.fresh_predictor_mean line 166
15. lemma OAI.BoundedTreewidthL1.ReservedTests.part_mean_bound line 204
16. theorem OAI.BoundedTreewidthL1.ReservedTests.launch_test line 228

    Source documentation

    EXACT fresh pair departure test. Only equal bag values, distinct reserved indices and the true per-particle suffix means are required.

    theorem launch_test (M : ℝ) (F : ι → V → ℝ) (P : Finset V) (i j : ι)
        (hij : i ≠ j) (hbag : ∀ v ∈ P, F i v = F j v) (z : V)
        (f p : State ι V → ℝ) (hf : ∀ a, 0 ≤ f a ∧ f a ≤ 1) (hp : ∀ a, 0 ≤ p a ∧ p a ≤ 1)
        (hi : (∑ ω : V → Bool, weight M F (i,false,ω)*f (i,false,ω)) = (F i z + M)/2)
        (hj : (∑ ω : V → Bool, weight M F (j,false,ω)*f (j,false,ω)) = (F j z + M)/2) :
        |F i z - F j z|/2 ≤ defect (weight M F) (action (weight M F) (departure M F P i j) f) p := by
    …

17. def OAI.BoundedTreewidthL1.ReservedSuffix.edge line 268

    Source documentation

    The actual parent departure followed by the actual child incoming update.

    noncomputable def edge (M : ℝ) (F H : ι → V → ℝ) (P Q : Finset V)
        (i j : ι) (C : Finset ι) : State ι V → State ι V → ℝ :=
    …

18. lemma OAI.BoundedTreewidthL1.ReservedSuffix.edge_coupling line 272
19. lemma OAI.BoundedTreewidthL1.ReservedSuffix.edge_restrict line 282
20. def OAI.BoundedTreewidthL1.ReservedSuffix.kernels line 295
21. def OAI.BoundedTreewidthL1.ReservedSuffix.bags line 299
22. lemma OAI.BoundedTreewidthL1.ReservedSuffix.bags_succ line 302
23. theorem OAI.BoundedTreewidthL1.ReservedSuffix.response_restrict line 315

    Source documentation

    A reserved old particle's true suffix response is exactly a sequence of ordered interval heat baths. All transitions are the expanded preparation ones.

    theorem response_restrict (M : ℝ) (F : ℕ → ι → V → ℝ) (P : ℕ → Finset V)
        (fresh₁ fresh₂ : ℕ → ι) (C : ℕ → Finset ι)
        (hret : ∀ s r, r ∈ C s → F s r = F (s+1) r)
        (htrace : ∀ s, particleTrace M (F s) (P (s+1)) = particleTrace M (F (s+1)) (P (s+1)))
        (t n : ℕ) (r : ι) (G : V → ℝ)
        (hfixed : ∀ s, t ≤ s → s ≤ t+n → F s r = G)
        (hkeep : ∀ s, t ≤ s → s < t+n → r ∈ C s ∧ r ≠ fresh₁ s ∧ r ≠ fresh₂ s)
        (z : V) (a : OrderedReservation.Carrier M G) :
        response (fun s => weight M (F s)) (kernels M F P fresh₁ fresh₂ C) t n
          (fun b => if label b z then 1 else 0) (lift M G r a) =
          OrderedSweepFlow.execute (OrderedReservation.weight M G)
            ((bags P t n).map (OrderedReservation.traceRank M G))
    …

    Mentions: OAI.BoundedTreewidthL1.particleTrace, OAI.BoundedTreewidthL1.OrderedReservation.Carrier, OAI.BoundedTreewidthL1.ReservedSuffix.kernels, OAI.BoundedTreewidthL1.OrderedSweepFlow.execute, OAI.BoundedTreewidthL1.OrderedReservation.weight, OAI.BoundedTreewidthL1.ReservedSuffix.bags, OAI.BoundedTreewidthL1.OrderedReservation.traceRank