OAI/Combinatorics/UniformKServer/TreeRounding.lean

GitHub source file

51 declarations, 0 contain sorry, 0 declared as axioms

1. structure OAI.UniformKServer.TreeRounding.Shape line 11
2. abbrev OAI.UniformKServer.TreeRounding.Vertex line 15
3. def OAI.UniformKServer.TreeRounding.Children line 17
4. instance OAI.UniformKServer.TreeRounding.(instance at line 20) line 20
5. def OAI.UniformKServer.TreeRounding.park line 26
6. def OAI.UniformKServer.TreeRounding.intPark line 29
7. structure OAI.UniformKServer.TreeRounding.Allocation line 32
8. def OAI.UniformKServer.TreeRounding.Rounded line 38
9. structure OAI.UniformKServer.TreeRounding.Law line 43
10. def OAI.UniformKServer.TreeRounding.mean line 52
11. structure OAI.UniformKServer.TreeRounding.Extension line 54
12. def OAI.UniformKServer.TreeRounding.movement line 60
13. def OAI.UniformKServer.TreeRounding.variation line 65
14. abbrev OAI.UniformKServer.TreeRounding.Local line 71
15. def OAI.UniformKServer.TreeRounding.localReal line 73
16. def OAI.UniformKServer.TreeRounding.localInt line 77
17. theorem OAI.UniformKServer.TreeRounding.sum_localReal line 81
18. theorem OAI.UniformKServer.TreeRounding.sum_localInt line 86
19. theorem OAI.UniformKServer.TreeRounding.cast_intPark line 91
20. theorem OAI.UniformKServer.TreeRounding.mean_sub line 95
21. theorem OAI.UniformKServer.TreeRounding.mean_sum line 99
22. theorem OAI.UniformKServer.TreeRounding.mean_congr line 104
23. theorem OAI.UniformKServer.TreeRounding.mean_const line 108
24. theorem OAI.UniformKServer.TreeRounding.mean_mono line 111
25. theorem OAI.UniformKServer.TreeRounding.mean_nonneg line 115
26. theorem OAI.UniformKServer.TreeRounding.star_kernel line 120

    Source documentation

    Make the kernel valid even at probability-zero states.

    theorem star_kernel {Ω ι : Type} [Fintype Ω] [Fintype ι]
        (I : BalancedStar.Input Ω ι) :
        ∃ (g : Ω × Finset ι → ℝ) (y : Ω × Finset ι → ι → ℤ),
          (∀ z, 0 ≤ g z) ∧ (∀ ω, ∑ A, g (ω,A) = I.μ ω) ∧
          (∀ z i, Balanced (I.b i) (y z i)) ∧
          (∀ z, ∑ i, y z i = I.N z.1) ∧
          (∀ i, ∑ z, g z * (y z i : ℝ) = I.b i) ∧
          (∑ z, g z * ∑ i, |(y z i : ℝ) - (I.X z.1 i : ℝ)|) ≤
            32*BalancedStar.T I + 11*BalancedStar.imbalance I := by
    …

    Mentions: OAI.UniformKServer.BalancedStar.Input, OAI.UniformKServer.BalancedStar.T, OAI.UniformKServer.BalancedStar.imbalance

27. theorem OAI.UniformKServer.TreeRounding.extended_star line 167

    Source documentation

    An extension of an already generated joint state preserves every old observable and permits completely correlated prescribed parent totals.

    theorem extended_star (L : Law) {ι : Type} [Fintype ι]
        (a b : ι → ℝ) (ha : ∀ i, 0 ≤ a i) (hb : ∀ i, 0 ≤ b i)
        (X : L.State → ι → ℤ) (N : L.State → ℤ)
        (hX : ∀ s i, Balanced (a i) (X s i))
        (hN : ∀ s, Balanced (∑ i, b i) (N s))
        (hXm : ∀ i, mean L (fun s => (X s i : ℝ)) = a i)
        (hNm : mean L (fun s => (N s : ℝ)) = ∑ i, b i) :
        ∃ (L' : Law) (π : L'.State → L.State) (Y : L'.State → ι → ℤ),
          (∀ f : L.State → ℝ, mean L' (f ∘ π) = mean L f) ∧
          (∀ s i, Balanced (b i) (Y s i)) ∧
          (∀ s, ∑ i, Y s i = N (π s)) ∧
          (∀ i, mean L' (fun s => (Y s i : ℝ)) = b i) ∧
    …

    Mentions: OAI.UniformKServer.TreeRounding.Law, OAI.UniformKServer.TreeRounding.mean

28. def OAI.UniformKServer.TreeRounding.assigned line 197
29. def OAI.UniformKServer.TreeRounding.localMovement line 200
30. def OAI.UniformKServer.TreeRounding.nodeMovement line 205
31. def OAI.UniformKServer.TreeRounding.localVariation line 209
32. structure OAI.UniformKServer.TreeRounding.Good line 212
33. def OAI.UniformKServer.TreeRounding.assignChildren line 222
34. theorem OAI.UniformKServer.TreeRounding.parent_ne_self line 227
35. theorem OAI.UniformKServer.TreeRounding.assigned_current line 234
36. theorem OAI.UniformKServer.TreeRounding.assign_child line 239
37. theorem OAI.UniformKServer.TreeRounding.assign_unchanged line 246
38. theorem OAI.UniformKServer.TreeRounding.assign_earlier line 254
39. theorem OAI.UniformKServer.TreeRounding.assign_local line 266
40. theorem OAI.UniformKServer.TreeRounding.assign_old_local line 283
41. theorem OAI.UniformKServer.TreeRounding.old_local_mean line 294
42. theorem OAI.UniformKServer.TreeRounding.good_step line 309
43. theorem OAI.UniformKServer.TreeRounding.good_zero line 427
44. theorem OAI.UniformKServer.TreeRounding.good_all line 451
45. theorem OAI.UniformKServer.TreeRounding.sum_children line 465
46. theorem OAI.UniformKServer.TreeRounding.weighted_children line 471
47. theorem OAI.UniformKServer.TreeRounding.weight_separation line 489
48. theorem OAI.UniformKServer.TreeRounding.localVariation_le line 502
49. theorem OAI.UniformKServer.TreeRounding.childMovement_le line 526
50. theorem OAI.UniformKServer.TreeRounding.tree_rounding line 540

    Source documentation

    Exact companion proposition rounding-global for one conditional finite update. Geometric separation tau ≥22 is stated as 22*w_child ≤ w_parent, which includes the exact source weights r_j. No local kernels are assumed.

    theorem tree_rounding {n k : ℕ} (S : Shape n) (w : Vertex n → ℝ)
        (hw : ∀ v, 0 ≤ w v)
        (hsep : ∀ v, v ≠ 0 → 22*w v ≤ w (S.parent v))
        (a b : Allocation S k) (L : Law) (X : L.State → Vertex n → ℤ)
        (hX : ∀ s, Rounded a (X s))
        (hmean : ∀ v, mean L (fun s => (X s v : ℝ)) = a.amount v) :
        ∃ E : Extension L n,
          (∀ s, Rounded b (E.value s)) ∧
          (∀ v, mean E.law (fun s => (E.value s v : ℝ)) = b.amount v) ∧
          movement S w L X E ≤ 132 * variation w a b := by
    …

    Mentions: OAI.UniformKServer.TreeRounding.Shape, OAI.UniformKServer.TreeRounding.Vertex, OAI.UniformKServer.TreeRounding.Allocation, OAI.UniformKServer.TreeRounding.Law, OAI.UniformKServer.TreeRounding.Rounded, OAI.UniformKServer.TreeRounding.mean, OAI.UniformKServer.TreeRounding.Extension, OAI.UniformKServer.TreeRounding.movement, OAI.UniformKServer.TreeRounding.variation

51. theorem OAI.UniformKServer.TreeRounding.tree_initialization line 613

    Source documentation

    The independent BalancedRepair.initial rounding: no movement is charged for selecting it.

    theorem tree_initialization {n k : ℕ} (S : Shape n) (a : Allocation S k) :
        ∃ (L : Law) (X : L.State → Vertex n → ℤ),
          (∀ s, Rounded a (X s)) ∧
          (∀ v, mean L (fun s => (X s v : ℝ)) = a.amount v) := by
    …

    Mentions: OAI.UniformKServer.TreeRounding.Shape, OAI.UniformKServer.TreeRounding.Allocation, OAI.UniformKServer.TreeRounding.Law, OAI.UniformKServer.TreeRounding.Vertex, OAI.UniformKServer.TreeRounding.Rounded, OAI.UniformKServer.TreeRounding.mean