OAI/Combinatorics/KServer/Amplification.lean

GitHub source file

93 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.KServer.Episode.traceCost line 15
2. lemma OAI.KServer.Episode.traceCost_nonneg line 19
3. lemma OAI.KServer.Episode.configurationAfter_nil line 26
4. lemma OAI.KServer.Episode.configurationAfter_cons line 28
5. lemma OAI.KServer.Episode.traceCost_append line 32
6. lemma OAI.KServer.Episode.configurationAfter_append' line 42
7. lemma OAI.KServer.Episode.serve_undo line 47
8. def OAI.KServer.Episode.reverseTrace line 52
9. lemma OAI.KServer.Episode.reverse_restores line 58

   Source documentation

   The literal reverse word returns the labeled tuple, not just its multiset.

   lemma reverse_restores (s : Configuration k X) (h : List (X × Fin k)) :
       configurationAfter (configurationAfter s h) (reverseTrace s h) = s := by
   …

   Mentions: OAI.KServer.Configuration, OAI.KServer.configurationAfter, OAI.KServer.Episode.reverseTrace

10. lemma OAI.KServer.Episode.reverse_cost line 67
11. lemma OAI.KServer.Episode.reverse_length line 79
12. def OAI.KServer.Episode.serviceTrace line 85
13. lemma OAI.KServer.Episode.serviceTrace_cost line 89
14. lemma OAI.KServer.Episode.serviceTrace_requests line 96
15. lemma OAI.KServer.Episode.exists_labelString line 104

    Source documentation

    Every legal designated trace gives a label string in the source lazy model.

    lemma exists_labelString (h : List (X × Fin k)) :
        ∃ j : Fin (h.map Prod.fst).length → Fin k,
          serviceTrace (h.map Prod.fst) j = h := by
    …

    Mentions: OAI.KServer.Episode.serviceTrace

16. lemma OAI.KServer.Episode.optimalCost_le_trace line 116
17. lemma OAI.KServer.Episode.cheap_closed_episode line 124
18. def OAI.KServer.Episode.LazyTrace line 143

    Source documentation

    Pathwise strong laziness, imposed only on the trace actually selected.

    def LazyTrace (s : Configuration k X) : List (X × Fin k) → Prop
      | [] => True
      | (r,i)::h => ((∃ j, s j=r) → s i=r) ∧ LazyTrace (serve s i r) h
    
    omit [MetricSpace X] in

    Mentions: OAI.KServer.Configuration

19. lemma OAI.KServer.Episode.serve_same line 148
20. lemma OAI.KServer.Episode.zero_trace_unchanged line 153
21. lemma OAI.KServer.Episode.lazy_covered_trace line 175
22. lemma OAI.KServer.Episode.matching_zero_of_covers line 189
23. lemma OAI.KServer.Episode.zero_cycle_finishes_reset line 210

    Source documentation

    A zero-cost reset cycle covers all k distinct starting points; strong laziness then keeps that multiset fixed through all following reset requests.

    lemma zero_cycle_finishes_reset (s A : Configuration k X) (hs : Function.Injective s)
        (h g : List (X × Fin k))
        (hcycle : h.map Prod.fst = List.ofFn s) (hz : traceCost A h=0)
        (hg : LazyTrace (configurationAfter A h) g)
        (hrequests : ∀ r ∈ g.map Prod.fst, r ∈ Set.range s) :
        matching (configurationAfter A (h++g)) s=0 := by
    …

    Mentions: OAI.KServer.Configuration, OAI.KServer.Episode.traceCost, OAI.KServer.Episode.LazyTrace, OAI.KServer.configurationAfter, OAI.KServer.matching

24. lemma OAI.KServer.Episode.lazyTrace_append line 232
25. lemma OAI.KServer.Episode.discrete_trace_cost line 240
26. def OAI.KServer.Episode.cycleTrace line 257
27. def OAI.KServer.Episode.resetTrace line 260
28. lemma OAI.KServer.Episode.cycleTrace_requests line 264
29. lemma OAI.KServer.Episode.resetTrace_requests line 270
30. lemma OAI.KServer.Episode.reset_dichotomy line 278
31. lemma OAI.KServer.Episode.matching_le_diameter line 298
32. theorem OAI.KServer.Episode.reset_mismatch line 308

    Source documentation

    Equation reset-mismatch with its actual finite-reset cost. The metric gap is used only to choose the number of cycles; no bound depends on the horizon.

    theorem reset_mismatch (s A : Configuration k X) (hs : Function.Injective s)
        (δ Δ : ℝ) (hδ : 0  ≤  δ) (hg : ∀ x y : X, x ≠ y → δ  ≤  dist x y)
        (hdiam : ∀ x y : X, dist x y  ≤  Δ)
        (ls : List (Fin k → Fin k)) (hR : (k : ℝ)*Δ  ≤  (ls.length : ℝ)*δ)
        (hl : LazyTrace A (resetTrace s ls)) :
        matching (configurationAfter A (resetTrace s ls)) s  ≤ 
          traceCost A (resetTrace s ls) := by
    …

    Mentions: OAI.KServer.Configuration, OAI.KServer.Episode.LazyTrace, OAI.KServer.Episode.resetTrace, OAI.KServer.matching, OAI.KServer.configurationAfter, OAI.KServer.Episode.traceCost

33. lemma OAI.KServer.Episode.finite_gap_diameter line 323

    Source documentation

    Source's finite-space gap and diameter, with no assumption of discreteness on the eventual arbitrary metric space. Only the local finite experiment uses these constants.

    lemma finite_gap_diameter [Fintype X] (hne : ∃ x y : X, x ≠ y) :
        ∃ δ Δ : ℝ, 0 < δ ∧ 0  ≤  Δ ∧
          (∀ x y : X, x ≠ y → δ  ≤  dist x y) ∧ (∀ x y : X, dist x y  ≤  Δ) := by
    …

34. def OAI.KServer.Episode.resetCount line 341
35. lemma OAI.KServer.Episode.resetCount_bound line 343
36. theorem OAI.KServer.Episode.exists_uniform_reset line 352

    Source documentation

    The finite reset length is chosen once for the metric and starting stock, not for the law or horizon. It applies to every strongly lazy trace of that reset word, including choices of labels occupying equal positions.

    theorem exists_uniform_reset [Fintype X] (s : Configuration k X)
        (hs : Function.Injective s) (hne : ∃ x y : X, x ≠ y) :
        ∃ R : ℕ, 0 < R ∧ ∀ A : Configuration k X,
          ∀ ls : List (Fin k → Fin k), ls.length=R →
            LazyTrace A (resetTrace s ls) →
            matching (configurationAfter A (resetTrace s ls)) s  ≤  traceCost A (resetTrace s ls) := by
    …

    Mentions: OAI.KServer.Configuration, OAI.KServer.Episode.LazyTrace, OAI.KServer.Episode.resetTrace, OAI.KServer.matching, OAI.KServer.configurationAfter, OAI.KServer.Episode.traceCost

37. def OAI.KServer.Amplification.after line 377

    Source documentation

    Exact finite-input Bellman expectation of an arbitrary terminal observable. The private action history, not only the current configuration, is retained.

    def after (A : Policy k X) (h : List (X × Fin k)) : List X →
        (List (X × Fin k) → ℝ) → ℝ
      | [],f => f h
      | r::σ,f => ∑ i, (A h r).val i * after A (h++[(r,i)]) σ f

    Mentions: OAI.KServer.Policy

38. def OAI.KServer.Amplification.cost line 382
39. lemma OAI.KServer.Amplification.cost_nil line 387
40. lemma OAI.KServer.Amplification.cost_cons line 391
41. lemma OAI.KServer.Amplification.after_const line 398
42. lemma OAI.KServer.Amplification.after_mono line 405
43. lemma OAI.KServer.Amplification.after_nonneg line 414
44. lemma OAI.KServer.Amplification.after_add line 419
45. lemma OAI.KServer.Amplification.after_mul line 427
46. lemma OAI.KServer.Amplification.after_append line 435
47. lemma OAI.KServer.Amplification.cost_append line 443
48. lemma OAI.KServer.Amplification.cost_nonneg line 453
49. lemma OAI.KServer.Amplification.after_paths line 459
50. lemma OAI.KServer.Amplification.cost_paths line 473
51. lemma OAI.KServer.Amplification.supported_trace_lazy line 479
52. lemma OAI.KServer.Amplification.trace_of_cycle_requests line 498

    Source documentation

    Extract one cycle's label list from any trace whose requests are the fixed starting tuple. This prevents an unjustified switch from label multisets to labeled equality in the reset argument.

    lemma trace_of_cycle_requests (s : Configuration k X) (h : List (X × Fin k))
        (hr : h.map Prod.fst=List.ofFn s) :
        ∃ j : Fin k → Fin k, h=Episode.cycleTrace s j := by
    …

    Mentions: OAI.KServer.Configuration, OAI.KServer.Episode.cycleTrace

53. lemma OAI.KServer.Amplification.trace_of_reset_requests line 516
54. theorem OAI.KServer.Amplification.expected_reset line 543

    Source documentation

    The reset bound for literal Bellman expectation under an actual strongly lazy policy, not an assumed distribution of reset costs.

    theorem expected_reset [Fintype X] (s : Configuration k X) (hs : Function.Injective s)
        (hne : ∃ x y : X, x ≠ y) :
        ∃ R : ℕ, 0<R ∧ ∀ A : Policy k X, StronglyLazy s A → ∀ h,
          after A h ((List.replicate R (List.ofFn s)).flatten)
            (fun g=>matching (configurationAfter s g) s)  ≤ 
          cost A s h ((List.replicate R (List.ofFn s)).flatten) := by
    …

    Mentions: OAI.KServer.Configuration, OAI.KServer.Policy, OAI.KServer.StronglyLazy, OAI.KServer.Amplification.after, OAI.KServer.matching, OAI.KServer.configurationAfter, OAI.KServer.Amplification.cost

55. lemma OAI.KServer.Amplification.law_minimum line 571

    Source documentation

    The minimum is attained in the full product of causal decision simplexes, not in a horizon-dependent surrogate space.

    lemma law_minimum (s : Configuration k X) (σ : Ω → List X) (w : Ω → ℝ) :
        ∃ P : Policy k X, ∀ A : Policy k X,
          (∑ ω, w ω*expectedCost P s (σ ω))  ≤  ∑ ω, w ω*expectedCost A s (σ ω) := by
    …

    Mentions: OAI.KServer.Configuration, OAI.KServer.Policy

56. lemma OAI.KServer.Amplification.minimum_continuation line 583

    Source documentation

    Minimum-law continuation and compactness give a causal policy without sampling fictitious prefixes.

    lemma minimum_continuation (s : Configuration k X) (σ : Ω → List X) (w : Ω → ℝ)
        (hw : ∀ ω, 0 ≤ w ω) (hsum : ∑ ω, w ω=1) (m : ℝ)
        (hmin : ∀ B : Policy k X, m  ≤  ∑ ω, w ω*expectedCost B s (σ ω))
        (A : Policy k X) (h : List (X × Fin k)) :
        m  ≤  matching (configurationAfter s h) s+∑ ω, w ω*cost A s h (σ ω) := by
    …

    Mentions: OAI.KServer.Configuration, OAI.KServer.Policy, OAI.KServer.matching, OAI.KServer.configurationAfter, OAI.KServer.Amplification.cost

57. def OAI.KServer.Amplification.lawAfter line 594
58. def OAI.KServer.Amplification.lawCost line 598
59. lemma OAI.KServer.Amplification.lawAfter_mono line 602
60. lemma OAI.KServer.Amplification.lawAfter_const line 609
61. lemma OAI.KServer.Amplification.lawAfter_add line 615
62. def OAI.KServer.Amplification.runCost line 620
63. lemma OAI.KServer.Amplification.episode_telescope line 629

    Source documentation

    Exact telescoping lower bound for repeated independent closed episodes. The second premise here is derived from expected_reset below; it is not an assumed policy-existence claim.

    lemma episode_telescope (A : Policy k X) (s : Configuration k X)
        (w : Ω → ℝ) (hw : ∀ ω, 0 ≤ w ω) (hsum : ∑ ω, w ω=1)
        (ep : Ω → List X) (m : ℝ)
        (hstep : ∀ h, m+lawAfter A w ep h (fun g=>matching (configurationAfter s g) s)  ≤ 
          matching (configurationAfter s h) s+lawCost A s w ep h) :
        ∀ (N : ℕ) h, (N : ℝ)*m  ≤  matching (configurationAfter s h) s+runCost A s w ep N h := by
    …

    Mentions: OAI.KServer.Policy, OAI.KServer.Configuration, OAI.KServer.Amplification.lawAfter, OAI.KServer.matching, OAI.KServer.configurationAfter, OAI.KServer.Amplification.lawCost, OAI.KServer.Amplification.runCost

64. lemma OAI.KServer.Amplification.episode_step line 648

    Source documentation

    The reset charge and the minimum-continuation inequality together give the one-episode drift needed for the preceding telescope.

    lemma episode_step (A : Policy k X) (s : Configuration k X)
        (w : Ω → ℝ) (hw : ∀ ω, 0 ≤ w ω) (hsum : ∑ ω, w ω=1)
        (σ ρ : Ω → List X) (z : List X) (m : ℝ)
        (hmin : ∀ B : Policy k X, m  ≤  ∑ ω, w ω*expectedCost B s (σ ω))
        (hz : ∀ h, after A h z (fun g=>matching (configurationAfter s g) s) ≤ cost A s h z) :
        ∀ h, m+lawAfter A w (fun ω=>σ ω++ρ ω++z) h
          (fun g=>matching (configurationAfter s g) s)  ≤ 
          matching (configurationAfter s h) s+lawCost A s w (fun ω=>σ ω++ρ ω++z) h := by
    …

    Mentions: OAI.KServer.Policy, OAI.KServer.Configuration, OAI.KServer.Amplification.after, OAI.KServer.matching, OAI.KServer.configurationAfter, OAI.KServer.Amplification.cost, OAI.KServer.Amplification.lawAfter, OAI.KServer.Amplification.lawCost

65. lemma OAI.KServer.Amplification.sum_strings line 678
66. def OAI.KServer.Amplification.iidWord line 683
67. def OAI.KServer.Amplification.iidWeight line 687
68. lemma OAI.KServer.Amplification.iidWeight_nonneg line 692
69. lemma OAI.KServer.Amplification.iidWeight_sum line 699
70. lemma OAI.KServer.Amplification.after_sum line 709
71. lemma OAI.KServer.Amplification.runCost_iid line 719

    Source documentation

    The Bellman recursion is exactly the expectation under the concrete finite product law on iid forward words, including the algorithm's labels.

    lemma runCost_iid (A : Policy k X) (s : Configuration k X) (w : Ω → ℝ)
        (hsum : ∑ ω, w ω=1) (ep : Ω → List X) :
        ∀ N h, runCost A s w ep N h=
          ∑ v, iidWeight w N v*cost A s h (iidWord ep N v) := by
    …

    Mentions: OAI.KServer.Policy, OAI.KServer.Configuration, OAI.KServer.Amplification.runCost, OAI.KServer.Amplification.iidWeight, OAI.KServer.Amplification.cost, OAI.KServer.Amplification.iidWord

72. lemma OAI.KServer.Amplification.iidWord_length line 743
73. lemma OAI.KServer.Amplification.stationary_trace line 751
74. lemma OAI.KServer.Amplification.stationary_reset line 764
75. lemma OAI.KServer.Amplification.reset_length line 775
76. lemma OAI.KServer.Amplification.reset_requests_eq line 785
77. lemma OAI.KServer.Amplification.closed_padded_episodes line 798

    Source documentation

    Padded closed episodes, valid even when forward lengths differ. Padding is inserted after the reverse path and before the reset, so it costs the closed offline trace zero and does not compromise the online reset-mismatch bound.

    lemma closed_padded_episodes (s : Configuration k X) (σ : Ω → List X) (R : ℕ) :
        ∃ L : ℕ, ∃ ρ : Ω → List X, ∃ t : Ω → List (X × Fin k),
          ∀ ω, (t ω).map Prod.fst=σ ω++ρ ω++(List.replicate R (List.ofFn s)).flatten ∧
            configurationAfter s (t ω)=s ∧ Episode.traceCost s (t ω)=2*optimalCost s (σ ω) ∧
            (t ω).length=L := by
    …

    Mentions: OAI.KServer.Configuration, OAI.KServer.configurationAfter, OAI.KServer.Episode.traceCost

78. def OAI.KServer.Amplification.iidTrace line 833
79. def OAI.KServer.Amplification.iidSum line 837
80. lemma OAI.KServer.Amplification.iidTrace_requests line 842
81. lemma OAI.KServer.Amplification.iidTrace_cost line 850
82. lemma OAI.KServer.Amplification.iidSum_expectation line 858
83. lemma OAI.KServer.Amplification.iid_offline line 871
84. def OAI.KServer.Amplification.pushWeights line 890
85. lemma OAI.KServer.Amplification.pushWeights_nonneg line 894
86. lemma OAI.KServer.Amplification.pushWeights_expectation line 901
87. lemma OAI.KServer.Amplification.pushWeights_sum line 911
88. lemma OAI.KServer.Amplification.fixed_law_indexed line 918

    Source documentation

    Exact transport of a horizon law to a finite indexed family; identically valued words are grouped rather than incorrectly treated as different inputs.

    lemma fixed_law_indexed [Fintype X] (s : Configuration k X) (c D : ℝ)
        (hfinite : ∀ H : ℕ, ∀ q : (Fin H → X) → ℝ,
          (∀ v,0 ≤ q v) → (∑ v,q v=1) → ∃ A : Policy k X, StronglyLazy s A ∧
            (∑ v,q v*expectedCost A s (List.ofFn v))  ≤ 
              c*(∑ v,q v*optimalCost s (List.ofFn v))+D)
        (σ : Ω → List X) (w : Ω → ℝ) (hw : ∀ ω,0 ≤ w ω) (hsum : ∑ ω,w ω=1)
        (H : ℕ) (hH : ∀ ω,(σ ω).length=H) :
        ∃ A : Policy k X, StronglyLazy s A ∧
          (∑ ω,w ω*expectedCost A s (σ ω))  ≤  c*(∑ ω,w ω*optimalCost s (σ ω))+D := by
    …

    Mentions: OAI.KServer.Configuration, OAI.KServer.Policy, OAI.KServer.StronglyLazy

89. lemma OAI.KServer.Amplification.remove_additive line 940

    Source documentation

    Removing a fixed additive term by arbitrarily many repetitions. This argument includes the zero-optimum case without assuming a positive Q.

    lemma remove_additive (m q D : ℝ) (h : ∀ N : ℕ, (N : ℝ)*m ≤ (N : ℝ)*q+D) : m ≤ q := by
    …

90. theorem OAI.KServer.Amplification.amplification_of_uniform_finite_law line 951

    Source documentation

    Episode amplification transfers the finite-law estimate to a horizon-uniform competitive bound.

    theorem amplification_of_uniform_finite_law [Fintype X]
        (s : Configuration k X) (hs : Function.Injective s) (hne : ∃ x y : X,x≠y)
        (c D : ℝ) (hc : 0 ≤ c)
        (hfinite : ∀ H : ℕ, ∀ q : (Fin H → X) → ℝ,
          (∀ v,0 ≤ q v) → (∑ v,q v=1) → ∃ A : Policy k X, StronglyLazy s A ∧
            (∑ v,q v*expectedCost A s (List.ofFn v))  ≤ 
              c*(∑ v,q v*optimalCost s (List.ofFn v))+D)
        (σ : Ω → List X) (w : Ω → ℝ) (hw : ∀ ω,0 ≤ w ω) (hsum : ∑ ω,w ω=1) :
        ∃ P : Policy k X, (∑ ω,w ω*expectedCost P s (σ ω))  ≤ 
          2*c*(∑ ω,w ω*optimalCost s (σ ω)) := by
    …

    Mentions: OAI.KServer.Configuration, OAI.KServer.Policy, OAI.KServer.StronglyLazy

91. def OAI.KServer.FiniteDistribution line 999
92. def OAI.KServer.FiniteLawStatement line 1002
93. theorem OAI.KServer.finite_law_suffices_for_main line 1014

    Source documentation

    The finite-law estimate implies the arbitrary-metric competitive bound through closed-episode amplification and product compactness.

    theorem finite_law_suffices_for_main : FiniteLawStatement.{u} → ReductionStatement.{u} := by
    …