OAI/Combinatorics/KServer/Allocation.lean

GitHub source file

169 declarations, 0 contain sorry, 0 declared as axioms

The exact source primitives installed in the actual affine minimizer recursion. The coefficients use raw core flags; fine caps are deliberately absent. The zero-potential cases do not evaluate the marked denominator.

  1. structure OAI.KServer.SimplexFamilies.Data line 20
  2. def OAI.KServer.SimplexFamilies.K line 33
  3. def OAI.KServer.SimplexFamilies.Z line 35
  4. def OAI.KServer.SimplexFamilies.core line 37
  5. def OAI.KServer.SimplexFamilies.potential line 39
  6. def OAI.KServer.SimplexFamilies.coefficient line 42
  7. lemma OAI.KServer.SimplexFamilies.K_continuous line 47
  8. lemma OAI.KServer.SimplexFamilies.Z_continuous line 56
  9. lemma OAI.KServer.SimplexFamilies.coefficient_continuous line 64
  10. def OAI.KServer.SimplexFamilies.family line 73
  11. lemma OAI.KServer.SimplexFamilies.value_eq line 84

    Source documentation

    Algebraic equality with the literal sum of the source's improper integrals. In particular the family does not substitute another potential.

    lemma value_eq (C ell : ℝ) (d : Data J R) (p : J × R → ℝ) (a : J → ℝ)
    (ha : a ∈ ChangingDomains.simplex d.active) :
    (family C ell).value d p a=potential C ell d (core d p) a := by
…

    Mentions: OAI.KServer.SimplexFamilies.Data, OAI.KServer.ChangingDomains.simplex, OAI.KServer.SimplexFamilies.family, OAI.KServer.SimplexFamilies.potential, OAI.KServer.SimplexFamilies.core

  12. lemma OAI.KServer.SimplexFamilies.value_bound line 111

    Source documentation

    Uniform endpoint bound from the same dimension-free rank slopes; the finite number of coordinates may occur only in this additive endpoint.

    lemma value_bound (C ell : ℝ) (d : Data J R) (p : J × R → ℝ) (a : J → ℝ) {L : ℝ}
    (hc : ∀ ir, |coefficient C ell d a ir| ≤ L) (hp : ∀ ir, p ir ∈ Set.Icc 0 1) :
    |(family C ell).value d p a| ≤ L*Fintype.card (J × R) := by
…

    Mentions: OAI.KServer.SimplexFamilies.Data, OAI.KServer.SimplexFamilies.coefficient, OAI.KServer.SimplexFamilies.family

  13. def OAI.KServer.SimplexFamilies.regular line 122
  14. lemma OAI.KServer.SimplexFamilies.regular_coefficient_bound line 136
  15. def OAI.KServer.SimplexFamilies.marked line 164

    Source documentation

    The marked base point is exactly one; no value with u=0 is accepted.

    def marked (A : Finset J) (flags : J → R → Bool) (o : J) (h eta : J → ℝ)
    (u : ℝ) (hu : 0 < u) (hu1 : u ≤ 1) (hh : ∀ i ≠ o, 1 ≤ h i) : Data J R where
…

    Mentions: OAI.KServer.SimplexFamilies.Data

  16. lemma OAI.KServer.SimplexFamilies.marked_coefficient_bound line 192
  17. def OAI.KServer.SimplexFamilies.automatic line 241

    Source documentation

    The automatic empty/singleton rule is a genuine zero potential, not a singular marked potential evaluated at a zero side parameter.

    def automatic (A : Finset J) (flags : J → R → Bool) : Data J R :=
…

    Mentions: OAI.KServer.SimplexFamilies.Data

  18. lemma OAI.KServer.SimplexFamilies.automatic_value line 244
  19. def OAI.KServer.SimplexTracker.simplex line 258
  20. def OAI.KServer.SimplexTracker.potential line 260
  21. def OAI.KServer.SimplexTracker.movement line 262
  22. def OAI.KServer.SimplexTracker.objective line 264
  23. lemma OAI.KServer.SimplexTracker.max_coordinate line 267
  24. lemma OAI.KServer.SimplexTracker.weighted_deficit line 272

    Source documentation

    Quantitative deficit from replacing alpha_i by alpha_i/(1+eta_i).

    lemma weighted_deficit {a h η : ι → ℝ} {ct ell ηmax : ℝ}
    (ha : a ∈ simplex) (hh : ∀ i, 0 ≤ h i) (hc : 0 < ct) (hl : 0 < ell)
    (hη : ∀ i, η i = ct * h i / ell) (hmax : ∀ i, η i ≤ ηmax) :
    ∑ i, a i / (1 + η i) ≤
      1 - ct / (ell * (1 + ηmax)) * ∑ i, a i * h i := by
…

    Mentions: OAI.KServer.SimplexTracker.simplex

  25. lemma OAI.KServer.SimplexTracker.exists_negative_derivative line 302

    Source documentation

    The derivative contradiction in eq:alpha-derivative-contradiction, with coefficients general enough to include the marked denominator.

    lemma exists_negative_derivative {a h η F B γ : ι → ℝ}
    {ct ell ηmax Cα CF S : ℝ}
    (ha : a ∈ simplex) (hh : ∀ i, 0 ≤ h i) (hc : 0 < ct) (hl : 0 < ell)
    (hη : ∀ i, η i = ct * h i / ell) (hmax : ∀ i, η i ≤ ηmax)
    (hCa : 0 < Cα) (_hCF : 0 ≤ CF) (hS : 0 < S)
    (hB : ∑ i, B i = S) (hF : ∀ i, 0 ≤ F i)
    (hT : 0 < ∑ i, a i * h i)
    (hden : ∑ i, a i * F i ≤ CF * ∑ i, a i * h i)
    (hgap : 2 * CF * (1 + ηmax) < Cα * ct)
    (hidentity : ∀ i, a i * F i / (1 + η i) * γ i =
      Cα * ell * (S * (a i / (1 + η i)) - B i)) :
    ∃ i, γ i < -2 * S := by
…

    Mentions: OAI.KServer.SimplexTracker.simplex

  26. lemma OAI.KServer.SimplexTracker.simplex_isCompact line 358
  27. lemma OAI.KServer.SimplexTracker.objective_continuousOn line 369
  28. lemma OAI.KServer.SimplexTracker.exists_minimizer line 381
  29. lemma OAI.KServer.SimplexTracker.minimizer_payment line 386
  30. lemma OAI.KServer.SimplexTracker.sum_replace line 395
  31. def OAI.KServer.SimplexTracker.transfer line 409

    Source documentation

    Transfer epsilon from donor i to receiver j, exactly as in §04.

    def transfer [DecidableEq ι] (a : ι → ℝ) (i j : ι) (ε : ℝ) : ι → ℝ :=
…
  32. lemma OAI.KServer.SimplexTracker.sum_transfer line 412
  33. lemma OAI.KServer.SimplexTracker.transfer_mem_simplex line 418
  34. lemma OAI.KServer.SimplexTracker.transfer_min_comparison line 430
  35. lemma OAI.KServer.SimplexTracker.minimizer_derivative_gap line 449
  36. lemma OAI.KServer.SimplexTracker.minimizer_not_inward_atBot line 475

    Source documentation

    A singular inward slope cannot occur at a constrained global minimum: there is always a positive donor in the unit simplex.

    lemma minimizer_not_inward_atBot [DecidableEq ι] {f : ι → ℝ → ℝ} {S : ℝ} {a₀ a : ι → ℝ}
    (hS : 0 ≤ S) (ha : a ∈ simplex) (hm : IsMinOn (objective f S a₀) simplex a)
    (hderiv : ∀ i, 0 < a i → DifferentiableAt ℝ (f i) (a i))
    {j : ι} (hj : a j = 0) :
    ¬ Tendsto (fun ε : ℝ => (f j ε - f j 0) / ε) (𝓝[>] 0) atBot := by
…

    Mentions: OAI.KServer.SimplexTracker.simplex, OAI.KServer.SimplexTracker.objective

  37. lemma OAI.KServer.SimplexTracker.minimizer_feasible line 516

    Source documentation

    Complete minimizer feasibility reduction, using the genuine derivative and singular endpoint properties of the source primitives.

    lemma minimizer_feasible [DecidableEq ι]
    {f : ι → ℝ → ℝ} {a₀ a h η F B : ι → ℝ} {ct ell ηmax Cα CF S : ℝ}
    (ha : a ∈ simplex) (hm : IsMinOn (objective f S a₀) simplex a)
    (hh : ∀ i, 0 ≤ h i) (hc : 0 < ct) (hl : 0 < ell)
    (hη : ∀ i, η i = ct * h i / ell) (hmax : ∀ i, η i ≤ ηmax)
    (hCa : 0 < Cα) (hCF : 0 ≤ CF) (hS : 0 < S)
    (hB0 : ∀ i, 0 ≤ B i) (hB : ∑ i, B i = S)
    (hF : ∀ i, 0 ≤ F i) (hFp : ∀ i, 0 < a i → 0 < F i)
    (hT : 0 < ∑ i, a i * h i)
    (hden : ∑ i, a i * F i ≤ CF * ∑ i, a i * h i)
    (hgap : 2 * CF * (1 + ηmax) < Cα * ct)
    (hderiv : ∀ i, 0 < a i → HasDerivAt (f i)
…

    Mentions: OAI.KServer.SimplexTracker.simplex, OAI.KServer.SimplexTracker.objective

  38. lemma OAI.KServer.Allocation.simplex_weight_pos line 584
  39. lemma OAI.KServer.Allocation.log_inverse_nonneg_closed line 595
  40. lemma OAI.KServer.Allocation.exists_simplex_update line 603

    Source documentation

    The exact integral update, including compact existence, singular endpoint exclusion, feasibility and payment. Its analytic premises are proved above for both displayed denominator types; no convexity is presumed.

    lemma exists_simplex_update [DecidableEq ι]
    {F : ι → ℝ → ℝ} {a₀ h c B base : ι → ℝ} {ct ell ηmax Cα CF : ℝ}
    (ha₀ : a₀ ∈ simplex) (hh : ∀ i, 0 < h i) (hc : 0 < ct) (hl : 0 < ell)
    (hmax : ∀ i, ct * h i / ell ≤ ηmax)
    (hCa : 0 < Cα) (hCF : 0 ≤ CF)
    (hB0 : ∀ i, 0 ≤ B i) (hb : ∀ i, base i ∈ Set.Icc 0 1)
    (hFc : ∀ i, Continuous (F i)) (hci : ∀ i, 0 < c i)
    (hF : ∀ i y, 0 ≤ y → c i * (1 + y)^2 ≤ F i y)
    (hdecay : ∀ i, Tendsto (fun s : ℝ => s * F i (Real.log (1 / s))) (𝓝[>] 0) (𝓝 0))
    (hden : ∀ a ∈ simplex, ∑ i, a i * F i (Real.log (1 / a i)) ≤ CF * ∑ i, a i * h i)
    (hgap : 2 * CF * (1 + ηmax) < Cα * ct) :
    let S := ∑ i, B i
…
  41. lemma OAI.KServer.Allocation.regular_simplex_update line 652

    Source documentation

    Instantiation on a domain without a dominant child, with the manuscript's regular denominators and base point zero, at all simplex points including zero.

    lemma regular_simplex_update [DecidableEq ι]
    {a₀ h B : ι → ℝ} {ct ell ηmax Cα Cexp : ℝ}
    (ha₀ : a₀ ∈ simplex) (hh : ∀ i, 1 ≤ h i) (hc : 0 < ct) (hl : 0 < ell)
    (hmax : ∀ i, ct * h i / ell ≤ ηmax) (hCa : 0 < Cα)
    (hB0 : ∀ i, 0 ≤ B i) (hCexp : 0 ≤ Cexp)
    (htail : ∑ i, Real.exp (-h i) ≤ Cexp)
    (hgap : 2 * (25 + 32 * Cexp) * (1 + ηmax) < Cα * ct) :
    let S := ∑ i, B i
…
  42. lemma OAI.KServer.Allocation.marked_simplex_update line 677

    Source documentation

    Marked-domain instantiation; the base point is one exactly on the marked coordinate, preserving the source's cancellation under parameter changes.

    lemma marked_simplex_update [DecidableEq ι]
    {a₀ h B : ι → ℝ} {ct ell ηmax Cα Cexp c u H : ℝ} (o : ι)
    (ha₀ : a₀ ∈ simplex) (hu : 0 < u) (hu1 : u ≤ 1)
    (hH : H = 1 + Real.log (1 / u)) (ho : h o = u)
    (hh : ∀ i ≠ o, 1 ≤ h i) (hc : 0 < ct) (hl : 0 < ell)
    (hmax : ∀ i, ct * h i / ell ≤ ηmax) (hCa : 0 < Cα)
    (hB0 : ∀ i, 0 ≤ B i) (hCexp : 0 ≤ Cexp)
    (hsideC : 0 < c) (hsideC1 : c ≤ 1) (hside : ∀ i ≠ o, c * H ≤ h i)
    (htail : ∑ i ∈ Finset.univ.erase o, Real.exp (-h i) ≤ Cexp * u)
    (hgap : 2 * ((25 * c + 2 + 32 * Cexp) / c) * (1 + ηmax) < Cα * ct) :
    let S := ∑ i, B i
…
  43. def OAI.KServer.SupportedAllocation.restrict line 748
  44. def OAI.KServer.SupportedAllocation.extend line 750
  45. lemma OAI.KServer.SupportedAllocation.extend_apply_mem line 753
  46. lemma OAI.KServer.SupportedAllocation.extend_apply_not_mem line 757
  47. lemma OAI.KServer.SupportedAllocation.restrict_extend line 761
  48. lemma OAI.KServer.SupportedAllocation.extend_restrict line 765
  49. lemma OAI.KServer.SupportedAllocation.sum_restrict line 773
  50. lemma OAI.KServer.SupportedAllocation.sum_extend line 778
  51. lemma OAI.KServer.SupportedAllocation.restrict_simplex line 783
  52. lemma OAI.KServer.SupportedAllocation.extend_simplex line 789
  53. lemma OAI.KServer.SupportedAllocation.movement_restrict line 800
  54. lemma OAI.KServer.SupportedAllocation.movement_extend line 806
  55. lemma OAI.KServer.SupportedAllocation.potential_restrict line 813
  56. lemma OAI.KServer.SupportedAllocation.restrict_isMin line 821

    Source documentation

    Restriction is exact, including both the movement penalty and the literal source potentials. No dummy inactive coordinate enters the denominator bound.

    lemma restrict_isMin {A : Finset J} (hA : A.Nonempty) {f : J → ℝ → ℝ}
    {S : ℝ} {a a₀ : J → ℝ} (ha : a ∈ ChangingDomains.simplex A)
    (ha₀ : a₀ ∈ ChangingDomains.simplex A) (hf : ∀ i∉A, f i 0=0)
    (hm : IsMinOn (fun b => (∑ i, f i (b i))+S*ChangingDomains.variation b a₀)
      (ChangingDomains.simplex A) a) :
    IsMinOn (SimplexTracker.objective (fun i : A => f i) S (restrict A a₀))
      SimplexTracker.simplex (restrict A a) := by
…

    Mentions: OAI.KServer.ChangingDomains.simplex, OAI.KServer.ChangingDomains.variation, OAI.KServer.SimplexTracker.objective, OAI.KServer.SupportedAllocation.restrict, OAI.KServer.SimplexTracker.simplex

  57. lemma OAI.KServer.Allocation.every_simplex_minimizer_feasible line 851

    Source documentation

    The feasibility argument holds for every attained minimizer, in particular for the fixed noncomputable choice in the causal recurrence.

    lemma every_simplex_minimizer_feasible
    {F : ι → ℝ → ℝ} {a₀ a h c B base : ι → ℝ} {ct ell ηmax Cα CF : ℝ}
    (ha : a ∈ simplex) (hh : ∀ i, 0 < h i) (hc : 0 < ct) (hl : 0 < ell)
    (hmax : ∀ i, ct*h i/ell ≤ ηmax) (hCa : 0 < Cα) (hCF : 0 ≤ CF)
    (hB0 : ∀ i, 0 ≤ B i) (hb : ∀ i, base i ∈ Set.Icc 0 1)
    (hFc : ∀ i, Continuous (F i)) (hci : ∀ i, 0 < c i)
    (hF : ∀ i y, 0 ≤ y → c i*(1+y)^2 ≤ F i y)
    (hdecay : ∀ i, Tendsto (fun s : ℝ => s*F i (Real.log (1/s))) (𝓝[>] 0) (𝓝 0))
    (hden : ∀ b ∈ simplex, ∑ i, b i*F i (Real.log (1/b i)) ≤ CF*∑ i, b i*h i)
    (hgap : 2*CF*(1+ηmax) < Cα*ct)
    (hm : IsMinOn (objective (fun i => primitive (F i) Cα ell (ct*h i/ell)
      (∑ j, B j) (B i) (base i)) (∑ i, B i) a₀) simplex a) :
…
  58. lemma OAI.KServer.Allocation.every_regular_minimizer_feasible line 897
  59. lemma OAI.KServer.SupportedAllocation.regular_supported_minimizer_feasible line 926

    Source documentation

    Uniform feasibility on the changing active domain. Its exp-tail hypothesis is a sum over active children only, exactly as in the source.

    lemma regular_supported_minimizer_feasible {A : Finset J} (hA : A.Nonempty)
    {a₀ a h B : J → ℝ} {ct ell ηmax Cα Cexp : ℝ}
    (ha : a ∈ ChangingDomains.simplex A) (ha₀ : a₀ ∈ ChangingDomains.simplex A)
    (hh : ∀ i∈A, 1≤h i) (hc : 0<ct) (hl : 0<ell)
    (hmax : ∀ i∈A, ct*h i/ell≤ηmax) (hCa : 0<Cα) (hB0 : ∀ i, 0≤B i)
    (hBout : ∀ i∉A, B i=0) (hCexp : 0≤Cexp) (htail : ∑ i∈A, Real.exp (-h i)≤Cexp)
    (hgap : 2*(25+32*Cexp)*(1+ηmax)<Cα*ct)
    (hm : IsMinOn (fun b => (∑ i, primitive (regularF (h i)) Cα ell (ct*h i/ell)
      (∑ j, B j) (B i) 0 (b i))+(∑ i, B i)*ChangingDomains.variation b a₀)
       (ChangingDomains.simplex A) a) :
    ∀ i, (∑ j, B j)*a i≤(1+ct*h i/ell)*B i := by
…

    Mentions: OAI.KServer.ChangingDomains.simplex, OAI.KServer.ChangingDomains.variation

  60. lemma OAI.KServer.Allocation.every_marked_minimizer_feasible line 964
  61. lemma OAI.KServer.SupportedAllocation.marked_supported_minimizer_feasible line 1038

    Source documentation

    Feasibility for the actual changing marked domain; inactive coordinates are zero instead of being assigned a spurious positive denominator weight.

    lemma marked_supported_minimizer_feasible {A : Finset J} {o : J} (hoA : o ∈ A)
    {a₀ a h B : J → ℝ} {ct ell ηmax Cα Cexp c u H : ℝ}
    (ha : a ∈ ChangingDomains.simplex A) (ha₀ : a₀ ∈ ChangingDomains.simplex A)
    (hu : 0 < u) (hu1 : u ≤ 1) (hH : H = 1 + Real.log (1 / u)) (ho : h o = u)
    (hh : ∀ i∈A, i ≠ o → 1 ≤ h i) (hc : 0<ct) (hl : 0<ell)
    (hmax : ∀ i∈A, ct*h i/ell ≤ ηmax) (hCa : 0<Cα)
    (hB0 : ∀ i, 0≤B i) (hBout : ∀ i∉A, B i=0) (hCexp : 0≤Cexp)
    (hsideC : 0<c) (hsideC1 : c≤1) (hside : ∀ i∈A, i≠o → c*H≤h i)
    (htail : ∑ i∈A.erase o, Real.exp (-h i) ≤ Cexp*u)
    (hgap : 2*((25*c+2+32*Cexp)/c)*(1+ηmax)<Cα*ct)
    (hm : IsMinOn (fun b => (∑ i, primitive (if i=o then markedF u H else regularF (h i))
      Cα ell (ct*h i/ell) (∑ j, B j) (B i) (if i=o then 1 else 0) (b i))+
…

    Mentions: OAI.KServer.ChangingDomains.simplex

  62. lemma OAI.KServer.AdaptiveAllocation.update_isMin line 1098
  63. lemma OAI.KServer.AdaptiveAllocation.regular_update_feasible line 1110
  64. lemma OAI.KServer.AdaptiveAllocation.core_eq line 1135
  65. def OAI.KServer.AdaptiveAllocation.preparedFlags line 1141

    Source documentation

    The prepared input is concrete and uses only new flags on the common old/new active domain, as in §04 (not intersection of old and new flags).

    def preparedFlags (A B : Finset J) (g : J → R → Bool) : J → R → Bool :=
…
  66. def OAI.KServer.AdaptiveAllocation.preparedInput line 1144
  67. lemma OAI.KServer.AdaptiveAllocation.prepared_flags_outside line 1148
  68. lemma OAI.KServer.AdaptiveAllocation.prepared_input_outside line 1154
  69. lemma OAI.KServer.AdaptiveAllocation.regular_potential_zero line 1160
  70. lemma OAI.KServer.AdaptiveAllocation.nonneg_total_zero line 1166
  71. lemma OAI.KServer.AdaptiveAllocation.regular_transpose_value line 1172
  72. lemma OAI.KServer.AdaptiveAllocation.regular_input_bound line 1189
  73. lemma OAI.KServer.AdaptiveAllocation.regular_parameter_jump line 1200
  74. lemma OAI.KServer.AdaptiveAllocation.total_variation_bound line 1237
  75. lemma OAI.KServer.AdaptiveAllocation.transpose_cap line 1243
  76. def OAI.KServer.AdaptiveAllocation.regularPrepare line 1255

    Source documentation

    This is the prepared minimizer from the manuscript; no drift inequality is an input to its definition.

    def regularPrepare (C ell ct : ℝ) (A B : Finset J) (g : J → R → Bool)
    (h : J → ℝ) (hh : ∀ i, 1≤h i) (p : J × R → ℝ) (a : J → ℝ) : J → ℝ :=
…
  77. def OAI.KServer.AdaptiveAllocation.regularTransport line 1262

    Source documentation

    Delete and insert zero coordinates following the prepared minimizing update, with a canonical simplex state only when its weight is exactly zero.

    def regularTransport (C ell ct : ℝ) (A B : Finset J) (g : J → R → Bool)
    (h : J → ℝ) (hh : ∀ i, 1≤h i) (p : J × R → ℝ) (a : J → ℝ) : J → ℝ :=
…
  78. lemma OAI.KServer.AdaptiveAllocation.regular_transport_mem line 1267
  79. lemma OAI.KServer.AdaptiveAllocation.literal_update_payment line 1290
  80. def OAI.KServer.AdaptiveAllocation.regularStep line 1303

    Source documentation

    The final update after genuine preparation and transport.

    def regularStep (C ell ct : ℝ) (A B : Finset J) (g : J → R → Bool)
    (h h' : J → ℝ) (hh : ∀ i, 1≤h i) (hh' : ∀ i, 1≤h' i)
    (p : J × R → ℝ) (a : J → ℝ) : J → ℝ :=
…
  81. lemma OAI.KServer.AdaptiveAllocation.regular_step_payment line 1310
  82. lemma OAI.KServer.AdaptiveAllocation.marked_update_feasible line 1390
  83. lemma OAI.KServer.AdaptiveAllocation.marked_input_bound line 1416
  84. lemma OAI.KServer.AdaptiveAllocation.marked_potential_zero line 1429
  85. lemma OAI.KServer.AdaptiveAllocation.marked_transpose_value line 1436
  86. lemma OAI.KServer.AdaptiveAllocation.simplex_side_weight line 1447
  87. lemma OAI.KServer.AdaptiveAllocation.marked_parameter_jump line 1463

    Source documentation

    Marked parameter edits charge the dominant component only when u changes, and charge it to the side total, not the dominant mass.

    lemma marked_parameter_jump (A A' : Finset J) (hA' : A'.Nonempty)
    (f g : J → R → Bool) (o : J) (h h' eta eta' : J → ℝ)
    {u u' : ℝ} (hu : 0<u) (hu1 : u≤1) (hu' : 0<u') (hu1' : u'≤1)
    (hh : ∀ i≠o, 1≤h i) (hh' : ∀ i≠o, 1≤h' i)
    (he : ∀ i, eta i∈Set.Icc 0 1) (he' : ∀ i, eta' i∈Set.Icc 0 1)
    (heq : ∀ i, h i=h' i → eta i=eta' i)
    (heqo : u=u' → eta o=eta' o) (heo : eta o≤u) (heo' : eta' o≤u')
    {C ell : ℝ} (hC : 0≤C) (hl : 0≤ell) {B a : J → ℝ}
    (hB : ∀ i, 0≤B i) (ha : a∈ChangingDomains.simplex A')
    (hcap : ∀ i, (∑ j, B j)*a i≤(1+eta i)*B i) :
    |potential C ell (marked A' g o h' eta' u' hu' hu1' hh') B a-
      potential C ell (marked A f o h eta u hu hu1 hh) B a| ≤
…

    Mentions: OAI.KServer.ChangingDomains.simplex

  88. def OAI.KServer.AdaptiveAllocation.markedPrepare line 1545
  89. def OAI.KServer.AdaptiveAllocation.markedTransport line 1552
  90. lemma OAI.KServer.AdaptiveAllocation.marked_transport_mem line 1558
  91. def OAI.KServer.AdaptiveAllocation.markedStep line 1579
  92. lemma OAI.KServer.AdaptiveAllocation.marked_step_payment line 1587
  93. def OAI.KServer.SideTracker.primitive line 1680

    Source documentation

    The explicit integral in eq:side-primitive-explicit.

    def primitive (c b θ z B D w : ℝ) : ℝ :=
…
  94. lemma OAI.KServer.SideTracker.primitive_derivative line 1685
  95. lemma OAI.KServer.SideTracker.derivative_le_of_left_comparison line 1710

    Source documentation

    One-sided necessary optimality, allowing a nondifferentiable movement cost.

    lemma derivative_le_of_left_comparison {f : ℝ → ℝ} {f' D x : ℝ}
    (hx : 0 < x) (hd : HasDerivAt f f' x)
    (hc : ∀ y ∈ Set.Icc 0 x, f x ≤ f y + D * (x - y)) : f' ≤ D := by
…
  96. lemma OAI.KServer.SideTracker.neg_derivative_le_of_right_comparison line 1727
  97. def OAI.KServer.SideTracker.domain line 1747
  98. def OAI.KServer.SideTracker.potential line 1749
  99. def OAI.KServer.SideTracker.movement line 1752
  100. def OAI.KServer.SideTracker.objective line 1754
  101. lemma OAI.KServer.SideTracker.movement_self line 1757
  102. lemma OAI.KServer.SideTracker.domain_isCompact line 1759
  103. lemma OAI.KServer.SideTracker.primitive_continuousOn line 1770
  104. lemma OAI.KServer.SideTracker.objective_continuousOn line 1775
  105. lemma OAI.KServer.SideTracker.exists_minimizer line 1788
  106. lemma OAI.KServer.SideTracker.minimizer_payment line 1794
  107. lemma OAI.KServer.SideTracker.sum_replace line 1804
  108. lemma OAI.KServer.SideTracker.replace_mem_domain line 1817
  109. lemma OAI.KServer.SideTracker.coordinate_min_comparison line 1828
  110. lemma OAI.KServer.SideTracker.derivative_upper_violation line 1844
  111. lemma OAI.KServer.SideTracker.derivative_lower_violation line 1869
  112. lemma OAI.KServer.SideTracker.minimizer_upper line 1897

    Source documentation

    Every minimizing update has the source's upper side feasibility.

    lemma minimizer_upper {M b D Cw : ℝ} {θ z B w₀ w : ι → ℝ}
    (hb : 1 ≤ b) (hθ : ∀ i, 0 < θ i) (hz : ∀ i, 0 < z i)
    (hB : ∀ i, 0 ≤ B i) (hD : 0 ≤ D) (hM : ∀ i, b + θ i ≤ M)
    (hw : w ∈ domain Cw)
    (hm : IsMinOn (objective (8 * M) b θ z B D w₀) (domain Cw) w) :
    ∀ i, D * w i ≤ (b + θ i) * B i := by
…

    Mentions: OAI.KServer.SideTracker.domain, OAI.KServer.SideTracker.objective

  113. lemma OAI.KServer.SideTracker.minimizer_lower line 1930

    Source documentation

    The lower bound uses the slack proved from the upper bound, not a new assumption that the simplex constraint is inactive.

    lemma minimizer_lower {M b D Cw : ℝ} {θ z B w₀ w : ι → ℝ}
    (hb : 1 ≤ b) (hθ : ∀ i, 0 < θ i) (hz : ∀ i, 0 < z i)
    (hB : ∀ i, 0 ≤ B i) (hD : 0 ≤ D) (hM : ∀ i, b + θ i ≤ M)
    (hCw : 2 * M < Cw) (hS : ∑ i, B i ≤ 2 * D)
    (hw : w ∈ domain Cw)
    (hm : IsMinOn (objective (8 * M) b θ z B D w₀) (domain Cw) w) :
    ∀ i, b * B i - θ i * z i * D ≤ D * w i := by
…

    Mentions: OAI.KServer.SideTracker.domain, OAI.KServer.SideTracker.objective

  114. theorem OAI.KServer.SideTracker.side_update line 1973

    Source documentation

    Section 04, Lemma side-tracker, with the explicit sufficient multiplier C'_w = 8M. No rank assumption or positivity assumption on D is added.

    theorem side_update {M b D Cw : ℝ} {θ z B w₀ : ι → ℝ}
    (hb : 1 ≤ b) (hθ : ∀ i, 0 < θ i) (hz : ∀ i, 0 < z i)
    (hB : ∀ i, 0 ≤ B i) (hD : 0 ≤ D) (hM : ∀ i, b + θ i ≤ M)
    (hCw : 2 * M < Cw) (hw₀ : w₀ ∈ domain Cw) :
    ∃ w ∈ domain Cw,
      IsMinOn (objective (8 * M) b θ z B D w₀) (domain Cw) w ∧
      (∀ i, D * w i ≤ (b + θ i) * B i) ∧
      ((∑ i, B i) ≤ 2 * D → ∀ i, b * B i - θ i * z i * D ≤ D * w i) ∧
      D * movement w w₀ ≤ potential (8 * M) b θ z B D w₀ -
        potential (8 * M) b θ z B D w := by
…

    Mentions: OAI.KServer.SideTracker.domain, OAI.KServer.SideTracker.objective, OAI.KServer.SideTracker.movement, OAI.KServer.SideTracker.potential

  115. lemma OAI.KServer.SideTracker.primitive_eq_integral line 1990

    Source documentation

    The logarithmic formula is exactly the source's interval integral.

    lemma primitive_eq_integral {c b θ z B D w : ℝ} (hθ : 0 < θ) (hz : 0 < z)
    (hw : 0 ≤ w) :
    primitive c b θ z B D w =
      c * ∫ s in (0 : ℝ)..w,
        (D * s - (b + θ / 2) * B + D * θ * z / 2) / (θ * (s + z)) := by
…

    Mentions: OAI.KServer.SideTracker.primitive

  116. lemma OAI.KServer.SideTracker.primitive_affine_inputs line 2017

    Source documentation

    Affinity in (B,D), used before every update decision in the all-step filtering telescope. In particular the held-D part is constant.

    lemma primitive_affine_inputs (c b θ z B₁ B₂ D₁ D₂ t w : ℝ) :
    primitive c b θ z ((1 - t) * B₁ + t * B₂) ((1 - t) * D₁ + t * D₂) w =
      (1 - t) * primitive c b θ z B₁ D₁ w + t * primitive c b θ z B₂ D₂ w := by
…

    Mentions: OAI.KServer.SideTracker.primitive

  117. lemma OAI.KServer.SideTracker.log_factors line 2028
  118. lemma OAI.KServer.SideTracker.side_log_bound line 2040
  119. def OAI.KServer.SideTracker.Dcoef line 2074

    Source documentation

    Coefficients of the actual primitive; all are nonnegative on the side domain. Their estimates use size-derived logarithmic cancellation.

    def Dcoef (c θ z w : ℝ) : ℝ :=
…
  120. def OAI.KServer.SideTracker.Bcoef line 2076
  121. lemma OAI.KServer.SideTracker.primitive_coefficients line 2079
  122. lemma OAI.KServer.SideTracker.coefficients_nonneg line 2084
  123. lemma OAI.KServer.SideTracker.Dcoef_bound line 2093
  124. lemma OAI.KServer.SideTracker.Bcoef_bound line 2119
  125. lemma OAI.KServer.SideTracker.primitive_component_bound line 2134
  126. lemma OAI.KServer.SideTracker.side_z_identity line 2155
  127. lemma OAI.KServer.SideTracker.potential_input_bound line 2162
  128. def OAI.KServer.SideSupported.restrict line 2217
  129. def OAI.KServer.SideSupported.extend line 2219
  130. lemma OAI.KServer.SideSupported.extend_apply_mem line 2222
  131. lemma OAI.KServer.SideSupported.extend_apply_not_mem line 2226
  132. lemma OAI.KServer.SideSupported.restrict_extend line 2230
  133. lemma OAI.KServer.SideSupported.extend_restrict line 2234
  134. lemma OAI.KServer.SideSupported.sum_restrict line 2242
  135. lemma OAI.KServer.SideSupported.sum_extend line 2247
  136. lemma OAI.KServer.SideSupported.restrict_mem line 2259
  137. lemma OAI.KServer.SideSupported.extend_mem line 2264
  138. lemma OAI.KServer.SideSupported.sideDomain_compact line 2276
  139. lemma OAI.KServer.SideSupported.movement_restrict line 2289
  140. lemma OAI.KServer.SideSupported.potential_restrict line 2295
  141. lemma OAI.KServer.SideSupported.restrict_isMin line 2303
  142. lemma OAI.KServer.SideSupported.supported_feasible line 2323
  143. structure OAI.KServer.SideFamilies.Data line 2356
  144. def OAI.KServer.SideFamilies.core line 2368
  145. def OAI.KServer.SideFamilies.coefficient line 2371
  146. def OAI.KServer.SideFamilies.offset line 2374
  147. lemma OAI.KServer.SideFamilies.Dcoef_continuousOn line 2377
  148. lemma OAI.KServer.SideFamilies.Bcoef_continuousOn line 2386
  149. lemma OAI.KServer.SideFamilies.coefficient_continuous line 2396
  150. lemma OAI.KServer.SideFamilies.offset_continuous line 2405
  151. def OAI.KServer.SideFamilies.family line 2413
  152. lemma OAI.KServer.SideFamilies.value_eq line 2425
  153. lemma OAI.KServer.SideFamilies.update_feasible line 2437
  154. lemma OAI.KServer.SideFamilies.update_payment line 2467
  155. lemma OAI.KServer.SideFamilies.domain_coordinate line 2483
  156. def OAI.KServer.SideFamilies.fromLog line 2489

    Source documentation

    The exact side regularizers obtained from the stored log size.

    def fromLog (A : Finset J) (f : J → R → Bool) (W b D cw ell : ℝ)
    (h : J → ℝ) (hW : 0≤W) (hcw : 0<cw) (hell : 0<ell) (hh : ∀ i, 1≤h i) : Data J R where
…

    Mentions: OAI.KServer.SideFamilies.Data

  157. lemma OAI.KServer.SideFamilies.fromLog_input_bound line 2503
  158. lemma OAI.KServer.SideFamilies.parameter_jump line 2525
  159. def OAI.KServer.SideFamilies.prepareData line 2567

    Source documentation

    Synthetic ranks use the new flags on the intersection of active sets.

    def prepareData (old new : Data J R) : Data J R :=
…

    Mentions: OAI.KServer.SideFamilies.Data

  160. def OAI.KServer.SideFamilies.prepare line 2570
  161. def OAI.KServer.SideFamilies.transport line 2573
  162. def OAI.KServer.SideFamilies.step line 2576
  163. lemma OAI.KServer.SideFamilies.prepare_mem line 2579
  164. lemma OAI.KServer.SideFamilies.transport_mem line 2583
  165. lemma OAI.KServer.SideFamilies.step_mem line 2589
  166. lemma OAI.KServer.SideFamilies.prepared_core_zero line 2594
  167. lemma OAI.KServer.SideFamilies.transport_payment line 2598
  168. lemma OAI.KServer.SideFamilies.transport_value line 2612
  169. lemma OAI.KServer.SideFamilies.step_payment line 2643

    Source documentation

    Local side edit payment for the actual two minimizers and deletion. The potential discrepancy terms will be bounded with the literal log parameters.

    lemma step_payment (old new : Data J R) {M : ℝ}
    (hb : 1≤old.b) (hD : 0≤new.D)
    (hM : ∀ i∈old.active, old.b+old.θ i≤M) (hW : 2*M<old.W)
    (p : J × R → ℝ) (hp : ∀ ir, 0≤p ir)
    (a : J → ℝ) (ha : a∈ChangingDomains.sideDomain old.active old.W)
    (hWW : old.W=new.W) :
    new.D*ChangingDomains.variation (step (8*M) old new p a) a ≤
      (family (8*M)).value old p a-(family (8*M)).value new p (step (8*M) old new p a)+
      |(family (8*M)).value (prepareData old new) p a-(family (8*M)).value old p a|+
      |(family (8*M)).value new p (transport (8*M) old new p a)-
        (family (8*M)).value (prepareData old new) p (transport (8*M) old new p a)| := by
…

    Mentions: OAI.KServer.SideFamilies.Data, OAI.KServer.ChangingDomains.sideDomain, OAI.KServer.ChangingDomains.variation, OAI.KServer.SideFamilies.step, OAI.KServer.SideFamilies.family, OAI.KServer.SideFamilies.prepareData, OAI.KServer.SideFamilies.transport