OAI/Combinatorics/TreewidthL1/ReservedCoupling.lean

GitHub source file

28 declarations, 0 contain sorry, 0 declared as axioms

1. structure OAI.BoundedTreewidthL1.ReservationCoupling.IsCoupling line 12
2. def OAI.BoundedTreewidthL1.ReservationCoupling.action line 17
3. def OAI.BoundedTreewidthL1.ReservationCoupling.total line 20
4. def OAI.BoundedTreewidthL1.ReservationCoupling.defect line 21
5. lemma OAI.BoundedTreewidthL1.ReservationCoupling.IsCoupling.symm line 24
6. lemma OAI.BoundedTreewidthL1.ReservationCoupling.IsCoupling.left_nonneg line 28
7. lemma OAI.BoundedTreewidthL1.ReservationCoupling.IsCoupling.right_nonneg line 33
8. lemma OAI.BoundedTreewidthL1.ReservationCoupling.IsCoupling.row_zero line 36
9. lemma OAI.BoundedTreewidthL1.ReservationCoupling.weighted_action line 42
10. lemma OAI.BoundedTreewidthL1.ReservationCoupling.action_bounds line 50
11. lemma OAI.BoundedTreewidthL1.ReservationCoupling.action_total line 65
12. lemma OAI.BoundedTreewidthL1.ReservationCoupling.action_adjoint line 72
13. lemma OAI.BoundedTreewidthL1.ReservationCoupling.defect_form line 90
14. lemma OAI.BoundedTreewidthL1.ReservationCoupling.defect_nonneg line 98
15. theorem OAI.BoundedTreewidthL1.ReservationCoupling.transfer_defect line 110

    Source documentation

    Move one true finite Markov transition from the endpoint response to the past predictor. This does not lose any mass, even with zero-probability states.

    theorem transfer_defect {μ : A → ℝ} {ν : B → ℝ} {Q : A → B → ℝ}
        (h : IsCoupling μ ν Q) (f : B → ℝ) (p : A → ℝ) :
        defect μ (action μ Q f) p = defect ν f (action ν (fun b a => Q a b) p) := by
    …

    Mentions: OAI.BoundedTreewidthL1.ReservationCoupling.IsCoupling, OAI.BoundedTreewidthL1.ReservationCoupling.defect, OAI.BoundedTreewidthL1.ReservationCoupling.action

16. def OAI.BoundedTreewidthL1.ReservationCoupling.response line 123

    Source documentation

    Responses through a constant finite state space, with time-dependent laws.

    noncomputable def response (μ : ℕ → A → ℝ) (Q : ℕ → A → A → ℝ)
        (t : ℕ) : ℕ → (A → ℝ) → (A → ℝ)
      | 0, f => f
      | n+1, f => action (μ t) (Q t) (response μ Q (t+1) n f)

    Mentions: OAI.BoundedTreewidthL1.ReservationCoupling.action

17. lemma OAI.BoundedTreewidthL1.ReservationCoupling.response_bounds line 128
18. lemma OAI.BoundedTreewidthL1.ReservationCoupling.response_total line 136
19. def OAI.BoundedTreewidthL1.ReservedKernel.lift line 154
20. lemma OAI.BoundedTreewidthL1.ReservedKernel.glue_action line 157
21. lemma OAI.BoundedTreewidthL1.ReservedKernel.old_key line 176
22. lemma OAI.BoundedTreewidthL1.ReservedKernel.sum_old_key line 186
23. lemma OAI.BoundedTreewidthL1.ReservedKernel.positive_trace_sum line 194
24. lemma OAI.BoundedTreewidthL1.ReservedKernel.departure_old_numerator line 213
25. theorem OAI.BoundedTreewidthL1.ReservedKernel.departure_action_old line 235

    Source documentation

    Restrict the ACTUAL departure kernel to an old retained particle: it is exactly the monotone interval heat bath, not an arbitrary common submeasure.

    theorem departure_action_old (M : ℝ) (F : ι → V → ℝ) (P : Finset V) (i j r : ι)
        (hir : r ≠ i) (hjr : r ≠ j) (a : OrderedReservation.Carrier M (F r))
        (f : State ι V → ℝ) :
        action (weight M F) (departure M F P i j) f (lift M (F r) r a) =
          OrderedSweepFlow.bath (OrderedReservation.weight M (F r))
            (OrderedReservation.traceRank M (F r) P) (fun b => f (lift M (F r) r b)) a := by
    …

    Mentions: OAI.BoundedTreewidthL1.OrderedReservation.Carrier, OAI.BoundedTreewidthL1.ReservedKernel.lift, OAI.BoundedTreewidthL1.OrderedSweepFlow.bath, OAI.BoundedTreewidthL1.OrderedReservation.weight, OAI.BoundedTreewidthL1.OrderedReservation.traceRank

26. lemma OAI.BoundedTreewidthL1.ReservedKernel.incoming_action_retained line 273

    Source documentation

    A retained incoming particle is copied exactly, as a whole global cut.

    lemma incoming_action_retained (M : ℝ) (F H : ι → V → ℝ) (P : Finset V) (C : Finset ι)
        (hret : ∀ i ∈ C, F i = H i) (htrace : particleTrace M F P = particleTrace M H P)
        (a : State ι V) (ha : a.1 ∈ C) (hpos : weight M F a ≠ 0) (f : State ι V → ℝ) :
        action (weight M F) (incoming M F H P C) f a = f a := by
    …

    Mentions: OAI.BoundedTreewidthL1.particleTrace

27. lemma OAI.BoundedTreewidthL1.ReservedKernel.action_compose line 288
28. lemma OAI.BoundedTreewidthL1.ReservedKernel.departure_symmetric line 304

    Source documentation

    Departure is symmetric: predictors are reheated by the same kernel.

    lemma departure_symmetric (M : ℝ) (F : ι → V → ℝ) (P : Finset V) (i j : ι) :
        ∀ a b, departure M F P i j a b = departure M F P i j b a := by
    …