OAI/Combinatorics/KServer/Potential.lean

GitHub source file

187 declarations, 0 contain sorry, 0 declared as axioms

Deterministic heavy-center schedule and its clipped distance profile. Random heavy radii do not affect this schedule.

  1. def OAI.KServer.HeavyCenters.ramp line 13

    Source documentation

    The heavy profile is zero up to radius 3 and one from radius 4.

    def ramp (u : ℝ) : ℝ := min 1 (max 0 (u-3))
  2. lemma OAI.KServer.HeavyCenters.ramp_bounds line 14
  3. lemma OAI.KServer.HeavyCenters.ramp_zero line 16
  4. lemma OAI.KServer.HeavyCenters.ramp_one line 18
  5. lemma OAI.KServer.HeavyCenters.ramp_lipschitz line 20
  6. def OAI.KServer.HeavyCenters.profile line 29

    Source documentation

    Finite minimum with a default value 1, also for the empty center set.

    def profile (r : ℝ) (C : Finset Y) (y : Y) : ℝ :=
…
  7. lemma OAI.KServer.HeavyCenters.profile_nonneg line 32
  8. lemma OAI.KServer.HeavyCenters.profile_le_one line 40
  9. lemma OAI.KServer.HeavyCenters.profile_bounds line 42
  10. lemma OAI.KServer.HeavyCenters.profile_le line 44
  11. lemma OAI.KServer.HeavyCenters.le_profile line 47
  12. lemma OAI.KServer.HeavyCenters.profile_empty line 55
  13. lemma OAI.KServer.HeavyCenters.profile_eq_one line 57
  14. lemma OAI.KServer.HeavyCenters.profile_eq_zero line 63
  15. lemma OAI.KServer.HeavyCenters.profile_gt_witness line 68
  16. lemma OAI.KServer.HeavyCenters.profile_lipschitz line 75
  17. def OAI.KServer.HeavyCenters.replace line 93

    Source documentation

    Delete centers at distance at most 100r, then insert the heavy request.

    def replace (r : ℝ) (C : Finset Y) (x : Y) : Finset Y :=
…
  18. lemma OAI.KServer.HeavyCenters.new_profile_zero line 96
  19. lemma OAI.KServer.HeavyCenters.profile_increase_support line 100
  20. lemma OAI.KServer.HeavyCenters.near_profile_edit line 122
  21. structure OAI.KServer.Pilot.Template line 147
  22. def OAI.KServer.Pilot.b line 156
  23. def OAI.KServer.Pilot.a line 157
  24. def OAI.KServer.Pilot.G line 160
  25. lemma OAI.KServer.Pilot.b_nonneg line 162
  26. lemma OAI.KServer.Pilot.b_le_one line 163
  27. lemma OAI.KServer.Pilot.b_eq_one line 165
  28. lemma OAI.KServer.Pilot.b_eq_zero line 168
  29. lemma OAI.KServer.Pilot.b_pos_iff line 171
  30. lemma OAI.KServer.Pilot.a_nonneg line 180
  31. lemma OAI.KServer.Pilot.a_le_one line 187
  32. lemma OAI.KServer.Pilot.a_eq_zero line 194
  33. lemma OAI.KServer.Pilot.G_nonneg line 202
  34. lemma OAI.KServer.Pilot.G_le_one line 203
  35. lemma OAI.KServer.Pilot.G_eq_zero line 205
  36. lemma OAI.KServer.Pilot.G_eq_one line 208
  37. def OAI.KServer.Pilot.Feasible line 214
  38. def OAI.KServer.Pilot.integrand line 219
  39. def OAI.KServer.Pilot.objective line 223
  40. lemma OAI.KServer.Pilot.feasible_zero line 226
  41. lemma OAI.KServer.Pilot.coordinate_le_one line 232
  42. lemma OAI.KServer.Pilot.feasible_closed line 240
  43. lemma OAI.KServer.Pilot.feasible_compact line 249
  44. lemma OAI.KServer.Pilot.objective_continuous line 255
  45. lemma OAI.KServer.Pilot.exists_minimizer line 260
  46. def OAI.KServer.Pilot.minimizer line 266

    Source documentation

    A canonical tie-break using choice is legitimate on the finite input tree.

    def minimizer (T : Template) (r : ℝ) (μ g : Y → ℝ) : Y → ℝ :=
…

    Mentions: OAI.KServer.Pilot.Template

  47. lemma OAI.KServer.Pilot.minimizer_spec line 268
  48. def OAI.KServer.Pilot.potential line 273
  49. lemma OAI.KServer.Pilot.potential_le line 276
  50. lemma OAI.KServer.Pilot.weighted_bump_le_capacity line 280
  51. lemma OAI.KServer.Pilot.sum_b_le_one line 291
  52. lemma OAI.KServer.Pilot.sum_a_le_one line 298
  53. lemma OAI.KServer.Pilot.integrand_bounds line 309
  54. lemma OAI.KServer.Pilot.potential_bounds line 332
  55. lemma OAI.KServer.Pilot.objective_mix line 348
  56. lemma OAI.KServer.Pilot.potential_concave line 355
  57. lemma OAI.KServer.Pilot.positive_b_support_disjoint line 365
  58. lemma OAI.KServer.Pilot.feasible_downward line 380
  59. def OAI.KServer.Pilot.coefficient line 389
  60. lemma OAI.KServer.Pilot.objective_linear line 392
  61. lemma OAI.KServer.Pilot.minimizer_zero_of_coefficient_pos line 424
  62. lemma OAI.KServer.Pilot.a_middle_lower line 452
  63. def OAI.KServer.Pilot.ball line 462

    Source documentation

    Closed metric balls.

    def ball (x : Y) (r : ℝ) : Finset Y := univ.filter fun p => dist x p ≤ r
  64. def OAI.KServer.Pilot.nearBall line 465

    Source documentation

    Only the near-site region in pilot-local(2) uses a strict inequality.

    def nearBall (x : Y) (r : ℝ) : Finset Y := univ.filter fun p => dist x p < r
  65. def OAI.KServer.Pilot.mass line 467
  66. lemma OAI.KServer.Pilot.coefficient_middle_pos line 469
  67. lemma OAI.KServer.Pilot.no_middle_site line 538
  68. def OAI.KServer.Pilot.insertUnit line 549

    Source documentation

    The clear-and-insert competitor; the clearing radius is 5D*.

    def insertUnit (T : Template) (r : ℝ) (z : Y → ℝ) (x : Y) : Y → ℝ :=
…

    Mentions: OAI.KServer.Pilot.Template

  69. lemma OAI.KServer.Pilot.insertUnit_self line 553
  70. lemma OAI.KServer.Pilot.insertUnit_le line 556
  71. lemma OAI.KServer.Pilot.G_lt_one line 561
  72. lemma OAI.KServer.Pilot.insertUnit_feasible line 566
  73. lemma OAI.KServer.Pilot.insertUnit_integrand_outside line 620

    Source documentation

    No changed bump reaches the complement of the outer ball.

    lemma insertUnit_integrand_outside {T : Template} {r : ℝ} {g z : Y → ℝ} {x p : Y}
    (hr : 0 < r) (hp : 100 * T.R * r ≤ dist x p) :
    integrand T r g (insertUnit T r z x) p = integrand T r g z p := by
…

    Mentions: OAI.KServer.Pilot.Template, OAI.KServer.Pilot.integrand, OAI.KServer.Pilot.insertUnit

  74. lemma OAI.KServer.Pilot.sum_min_ge_min_sum line 653

    Source documentation

    Dimension-free repair inequality used in relocating a pilot site.

    lemma sum_min_ge_min_sum {I : Type*} [Fintype I] {q : ℝ} {β : I → ℝ}
    (hq : 0 ≤ q) (hβ : ∀ i, 0 ≤ β i) :
    min q (∑ i, β i) ≤ ∑ i, min q (β i) := by
…
  75. lemma OAI.KServer.Pilot.capacity_repair line 665
  76. def OAI.KServer.Pilot.nearWeight line 685
  77. def OAI.KServer.Pilot.innerMoment line 688
  78. lemma OAI.KServer.Pilot.innerMoment_le line 691
  79. lemma OAI.KServer.Pilot.nearWeight_eq_b_sum line 701
  80. lemma OAI.KServer.Pilot.old_integrand_inner_lower line 734
  81. lemma OAI.KServer.Pilot.insertUnit_integrand_inner line 747
  82. lemma OAI.KServer.Pilot.nearWeight_deficit line 797
  83. lemma OAI.KServer.Pilot.nearWeight_large line 862
  84. lemma OAI.KServer.Pilot.near_sites_unique line 891
  85. lemma OAI.KServer.Pilot.near_site_of_large line 906
  86. lemma OAI.KServer.Pilot.near_site line 928

    Source documentation

    Unit-site pilot-local conclusions and the shell-ratio estimate.

    lemma near_site {T : Template} {r γ δ : ℝ} {μ g : Y → ℝ} {x : Y}
    (hr : 0 < r) (hγ0 : 0 ≤ γ) (hγ : γ ≤ T.σ / 64) (hδ : δ ≤ 1 / 4112)
    (hμ : ∀ p, 0 ≤ μ p) (hg : ∀ p, g p ∈ Set.Icc 0 1)
    (hM : 0 < mass μ (ball x (γ * r)))
    (hconc : mass μ (ball x (100 * T.R * r) \ ball x (γ * r)) ≤
      δ * mass μ (ball x (γ * r))) :
    ∃ s, dist s x < T.σ * r / 4 ∧ 3 / 4 ≤ minimizer T r μ g s ∧
      (1 - minimizer T r μ g s) * mass μ (ball x (γ * r)) ≤
        512 * γ / T.σ ^ 2 * innerMoment μ x γ r +
        514 * mass μ (ball x (100 * T.R * r) \ ball x (γ * r)) := by
…

    Mentions: OAI.KServer.Pilot.Template, OAI.KServer.Pilot.mass, OAI.KServer.Pilot.ball, OAI.KServer.Pilot.minimizer, OAI.KServer.Pilot.innerMoment

  87. lemma OAI.KServer.Pilot.clamp_abs line 966
  88. lemma OAI.KServer.Pilot.b_lipschitz line 973
  89. lemma OAI.KServer.Pilot.G_lipschitz line 979
  90. lemma OAI.KServer.Pilot.a_min_rep line 985
  91. lemma OAI.KServer.Pilot.a_lipschitz line 1020
  92. lemma OAI.KServer.Pilot.scaled_dist_lipschitz line 1057
  93. lemma OAI.KServer.Pilot.finite_sum_split line 1063
  94. lemma OAI.KServer.Pilot.clip_reduction line 1069
  95. def OAI.KServer.Pilot.relocate line 1082
  96. lemma OAI.KServer.Pilot.relocate_at line 1087
  97. lemma OAI.KServer.Pilot.relocate_le line 1091
  98. lemma OAI.KServer.Pilot.near_site_others_vanish line 1101
  99. lemma OAI.KServer.Pilot.relocate_feasible line 1117
  100. lemma OAI.KServer.Pilot.b_sum_single line 1221
  101. lemma OAI.KServer.Pilot.sum_relocate_le line 1246
  102. lemma OAI.KServer.Pilot.moved_square_gain line 1261
  103. lemma OAI.KServer.Pilot.a_eq_square line 1278
  104. lemma OAI.KServer.Pilot.relocate_inner_gain line 1285
  105. lemma OAI.KServer.Pilot.sum_unique_le line 1334
  106. lemma OAI.KServer.Pilot.relocate_decrease_le line 1350
  107. lemma OAI.KServer.Pilot.relocate_residual_loss line 1361
  108. lemma OAI.KServer.Pilot.moved_surcharge_loss line 1418
  109. lemma OAI.KServer.Pilot.relocate_shell_loss line 1444
  110. lemma OAI.KServer.Pilot.relocate_integrand_outside line 1472
  111. lemma OAI.KServer.Pilot.relocation_coefficient_bound line 1506
  112. lemma OAI.KServer.Pilot.relocate_displacement line 1526
  113. lemma OAI.KServer.Pilot.b_sum_near line 1596
  114. lemma OAI.KServer.Pilot.surcharge_diff_by_capacity line 1617
  115. lemma OAI.KServer.Pilot.near_square_loss line 1653
  116. lemma OAI.KServer.Pilot.near_integrand_slope line 1683
  117. def OAI.KServer.Pilot.localConstant line 1729

    Source documentation

    Exact constant displayed in (6.10), with no dependence on the metric size.

    def localConstant (T : Template) : ℝ :=
…

    Mentions: OAI.KServer.Pilot.Template

  118. lemma OAI.KServer.Pilot.localConstant_nonneg line 1732
  119. lemma OAI.KServer.Pilot.near_slope_mass line 1737
  120. theorem OAI.KServer.Pilot.local_structure line 1780

    Source documentation

    The full local-optimality theorem, derived from the actual compact minimizer, deletion, insertion and relocation competitors.

    theorem local_structure {T : Template} {r γ δ : ℝ} {μ g z : Y → ℝ} {x : Y}
    (hr : 0 < r) (hγ0 : 0 ≤ γ) (hγ : γ ≤ T.σ/64) (hγL : T.L*γ ≤ 1)
    (hδ : δ ≤ 1/4112) (hμ : ∀ p, 0 ≤ μ p) (hg : ∀ p, g p ∈ Set.Icc 0 1)
    (hglip : ∀ i j, |g i-g j| ≤ T.L*(dist i j/r))
    (hz : Feasible T r z) (hmin : IsMinOn (objective T r μ g) {w | Feasible T r w} z)
    (hM : 0 < mass μ (ball x (γ*r)))
    (hconc : mass μ (ball x (100*T.R*r) \ ball x (γ*r)) ≤ δ*mass μ (ball x (γ*r))) :
    (∀ i, T.σ*r/4 ≤ dist i x → dist i x ≤ T.R*r/2 → z i=0) ∧
    ∃ s, dist s x < T.σ*r/4 ∧ 3/4 ≤ z s ∧
      (∀ i, dist i x < T.σ*r/4 → 0 < z i → i=s) ∧
      (1-z s)*mass μ (ball x (γ*r)) ≤ 512*γ/T.σ^2*innerMoment μ x γ r +
        514*mass μ (ball x (100*T.R*r) \ ball x (γ*r)) ∧
…

    Mentions: OAI.KServer.Pilot.Template, OAI.KServer.Pilot.Feasible, OAI.KServer.Pilot.objective, OAI.KServer.Pilot.mass, OAI.KServer.Pilot.ball, OAI.KServer.Pilot.innerMoment

  121. lemma OAI.KServer.Pilot.surcharge_global_by_capacity line 1828
  122. lemma OAI.KServer.Pilot.b_global_by_capacity line 1862
  123. def OAI.KServer.Pilot.globalConstant line 1888
  124. lemma OAI.KServer.Pilot.globalConstant_ge line 1890
  125. lemma OAI.KServer.Pilot.integrand_diff_le line 1895
  126. theorem OAI.KServer.Pilot.integrand_lipschitz line 1939
  127. lemma OAI.KServer.ScaleMass.capped_log line 1960
  128. lemma OAI.KServer.ScaleMass.shifted_sum_le line 1977

    Source documentation

    A p-step telescoping sum has only p boundary differences. The function is allowed to be extended by the upper endpoint.

    lemma shifted_sum_le (f : ℕ → ℝ) (a b : ℝ) (hf : ∀ i, f i ∈ Set.Icc a b)
    (n p : ℕ) : ∑ i ∈ range n, (f (i+p)-f i) ≤ p*(b-a) := by
…
  129. lemma OAI.KServer.ScaleMass.shell_log_sum line 1993
  130. lemma OAI.KServer.ScaleMass.relative_increment_le_log line 2019

    Source documentation

    Relative new mass is controlled by the logarithmic increase.

    lemma relative_increment_le_log {a b : ℝ} (ha : 0 < a) (hab : a ≤ b) :
    (b-a)/b ≤ Real.log b-Real.log a := by
…
  131. lemma OAI.KServer.ScaleMass.relative_increment_sum line 2027
  132. lemma OAI.KServer.ScaleMass.geometric_sum_le_two line 2038
  133. lemma OAI.KServer.ScaleMass.geometric_weighted_sum line 2046

    Source documentation

    Geometric radius sums, including every initial atom and any finite cutoff.

    lemma geometric_weighted_sum {n : ℕ} {r : ℕ → ℝ} (hr : ∀ i < n, 0 ≤ r i)
    (hstep : ∀ i, i+1 < n → 2*r i ≤ r (i+1)) :
    ∑ i ∈ range n, r i ≤ if n=0 then 0 else 2*r (n-1) := by
…
  134. def OAI.KServer.ScaleMass.convolution line 2063
  135. lemma OAI.KServer.ScaleMass.convolution_nonneg line 2066
  136. lemma OAI.KServer.ScaleMass.convolution_succ line 2070
  137. lemma OAI.KServer.ScaleMass.convolution_sum_aux line 2081
  138. lemma OAI.KServer.ScaleMass.convolution_sum_le line 2093
  139. def OAI.KServer.ScaleMass.increment line 2101

    Source documentation

    The first relative increment includes the entire first ball.

    def increment (m : ℕ → ℝ) (i : ℕ) : ℝ := if i=0 then m 0 else m i-m (i-1)
  140. lemma OAI.KServer.ScaleMass.increment_nonneg line 2103
  141. lemma OAI.KServer.ScaleMass.increment_sum_le line 2109
  142. lemma OAI.KServer.ScaleMass.moment_sum_le line 2121

    Source documentation

    Exact Fubini/geometric moment estimate, encoded as a finite convolution. The hypotheses here are the ball-layer pointwise estimate and monotone masses; no estimate to be proved is hidden among them.

    lemma moment_sum_le {m t : ℕ → ℝ} {q γ k : ℝ} {n : ℕ}
    (hq0 : 0 ≤ q) (hq : q ≤ 1/2) (hγ : 0 ≤ γ) (hk : 1/2 ≤ k)
    (hm0 : 1/2 ≤ m 0) (hm : Monotone m) (hmk : ∀ i < n, m i ≤ k)
    (ht : ∀ j < n, t j ≤ γ*∑ i ∈ range (j+1), q^(j-i)*increment m i/m j) :
    ∑ j ∈ range n, t j ≤ 2*γ*(1+Real.log (2*k)) := by
…

    Mentions: OAI.KServer.ScaleMass.increment

  143. def OAI.KServer.Pilot.radius line 2169

    Source documentation

    The coarse consecutive range, written in increasing order for moment summation.

    def radius (r₀ τ : ℝ) (j : ℕ) : ℝ := r₀*τ^j
  144. lemma OAI.KServer.Pilot.radius_pos line 2171
  145. lemma OAI.KServer.Pilot.radius_succ line 2174
  146. lemma OAI.KServer.Pilot.radius_add line 2177
  147. lemma OAI.KServer.Pilot.radius_mono line 2180
  148. lemma OAI.KServer.Pilot.ball_mono line 2187
  149. lemma OAI.KServer.Pilot.mass_mono line 2192
  150. lemma OAI.KServer.Pilot.mass_nonneg line 2196
  151. def OAI.KServer.Pilot.innerMass line 2199
  152. lemma OAI.KServer.Pilot.innerMass_mono line 2202
  153. lemma OAI.KServer.Pilot.innerMoment_step line 2208
  154. lemma OAI.KServer.Pilot.innerMoment_convolution line 2247
  155. theorem OAI.KServer.Pilot.innerMoment_scale_sum line 2267

    Source documentation

    The moment sum for actual closed metric balls, not an interface assuming the ball-layer estimate. It includes atoms in the first ball.

    theorem innerMoment_scale_sum {μ : Y → ℝ} {x : Y} {γ r₀ τ k : ℝ} (n : ℕ)
    (hμ : ∀ y, 0 ≤ μ y) (hγ : 0 ≤ γ) (hr : 0 < r₀) (hτ : 2 ≤ τ)
    (hm0 : 1/2 ≤ innerMass μ x γ r₀ τ 0) (hk : ∑ y, μ y = k) :
    ∑ j ∈ range n, innerMoment μ x γ (radius r₀ τ j)/innerMass μ x γ r₀ τ j ≤
      2*γ*(1+Real.log (2*k)) := by
…

    Mentions: OAI.KServer.Pilot.innerMass, OAI.KServer.Pilot.innerMoment, OAI.KServer.Pilot.radius

  156. theorem OAI.KServer.Pilot.shell_scale_sum line 2291

    Source documentation

    Shell summation for the exact closed balls. Missing coarser masses are assigned total mass k in the telescope.

    theorem shell_scale_sum {μ : Y → ℝ} {x : Y} {γ D r₀ τ k : ℝ} (n p : ℕ)
    (hμ : ∀ y, 0 ≤ μ y) (hγ : 0 ≤ γ) (hr : 0 < r₀) (hτ : 2 ≤ τ)
    (hD : γ ≤ D) (hp : D ≤ γ*τ^p)
    (hm0 : 1/2 ≤ innerMass μ x γ r₀ τ 0) (hk : ∑ y, μ y = k) :
    ∑ j ∈ range n, min 1 (mass μ (ball x (D*radius r₀ τ j)\
      ball x (γ*radius r₀ τ j))/innerMass μ x γ r₀ τ j) ≤
      (p:ℝ)/Real.log 2*Real.log (2*k) := by
…

    Mentions: OAI.KServer.Pilot.innerMass, OAI.KServer.Pilot.mass, OAI.KServer.Pilot.ball, OAI.KServer.Pilot.radius

  157. lemma OAI.KServer.Pilot.radius_geometric line 2337
  158. lemma OAI.KServer.Pilot.radius_truncated_sum line 2344

    Source documentation

    Every truncated initial segment of a geometric radius sequence costs at most twice the cutoff; there is no number-of-scales factor.

    lemma radius_truncated_sum {r₀ τ R : ℝ} (hr : 0 ≤ r₀) (hτ : 2 ≤ τ) (hR : 0 ≤ R) (n : ℕ) :
    ∑ j ∈ range n, (if radius r₀ τ j ≤ R then radius r₀ τ j else 0) ≤ 2*R := by
…

    Mentions: OAI.KServer.Pilot.radius

  159. def OAI.KServer.Pilot.moveMeasure line 2360
  160. def OAI.KServer.Pilot.moveCost line 2362
  161. lemma OAI.KServer.Pilot.moveMeasure_nonneg line 2365
  162. lemma OAI.KServer.Pilot.moveCost_nonneg line 2370
  163. lemma OAI.KServer.Pilot.moveMeasure_integral line 2374
  164. lemma OAI.KServer.Pilot.candidate_drift line 2384
  165. lemma OAI.KServer.Pilot.positive_drift_candidate line 2398
  166. lemma OAI.KServer.Pilot.positive_integrand_global line 2413
  167. lemma OAI.KServer.Pilot.positive_integrand_bounded line 2424
  168. lemma OAI.KServer.Pilot.positive_integrand_local line 2431
  169. lemma OAI.KServer.Pilot.mover_innerMass_half line 2455
  170. def OAI.KServer.Pilot.shellRatio line 2477
  171. def OAI.KServer.Pilot.momentRatio line 2480
  172. lemma OAI.KServer.Pilot.shellRatio_nonneg line 2483
  173. lemma OAI.KServer.Pilot.momentRatio_nonneg line 2486
  174. def OAI.KServer.Pilot.slopeBudget line 2490
  175. lemma OAI.KServer.Pilot.slopeBudget_nonneg line 2493
  176. lemma OAI.KServer.Pilot.positive_integrand_coarse line 2502

    Source documentation

    A single estimate covers good and bad coarse radii. The exceptional far point term is geometric and will be summed before integration.

    lemma positive_integrand_coarse {T : Template} {r γ δ : ℝ} {μ g z : Y → ℝ} {x y : Y}
    (hr : 0 < r) (hγ0 : 0 ≤ γ) (hγ : γ ≤ T.σ/64) (hγL : T.L*γ ≤ 1)
    (hδ0 : 0 < δ) (hδ : δ ≤ 1/4112) (hμ : ∀ p, 0 ≤ μ p) (hg : ∀ p, g p ∈ Set.Icc 0 1)
    (hglip : ∀ i j, |g i-g j| ≤ T.L*(dist i j/r))
    (hz : Feasible T r z) (hmin : IsMinOn (objective T r μ g) {w | Feasible T r w} z)
    (hM : 0 < mass μ (ball x (γ*r))) :
    r*max (integrand T r g z x-integrand T r g z y) 0 ≤
      slopeBudget T δ (shellRatio μ x γ (100*T.R) r) (momentRatio μ x γ r)*dist x y +
        (if r ≤ 8*dist x y/T.σ then 514*r else 0) := by
…

    Mentions: OAI.KServer.Pilot.Template, OAI.KServer.Pilot.Feasible, OAI.KServer.Pilot.objective, OAI.KServer.Pilot.mass, OAI.KServer.Pilot.ball, OAI.KServer.Pilot.integrand, OAI.KServer.Pilot.slopeBudget, OAI.KServer.Pilot.shellRatio, OAI.KServer.Pilot.momentRatio

  177. def OAI.KServer.Pilot.coarseBudget line 2551
  178. lemma OAI.KServer.Pilot.coarse_drift_sum line 2555
  179. lemma OAI.KServer.Pilot.radius_shift line 2616
  180. lemma OAI.KServer.Pilot.positive_drift_bounded line 2619
  181. theorem OAI.KServer.Pilot.drift_sum line 2631

    Source documentation

    Full positive drift sum, with the actual minimizer at each scale. The ascending order is just a reversal of the finite geometric scale list.

    theorem drift_sum {T : Template} {γ δ r₀ τ k : ℝ} {μ ν : Y → ℝ} {x : Y}
    (g : ℕ → Y → ℝ) (n p : ℕ)
    (hr : 0 < r₀) (hτ : 2 ≤ τ) (hγ0 : 0 < γ) (hγ : γ ≤ T.σ/64)
    (hγL : T.L*γ ≤ 1) (hδ0 : 0 < δ) (hδ : δ ≤ 1/4112)
    (hpow : 100*T.R ≤ γ*τ^p)
    (hμ : ∀ y, 0 ≤ μ y) (hν : ∀ y, 0 ≤ ν y) (hνμ : ∀ y, ν y ≤ μ y)
    (hν1 : ∑ y, ν y=1) (hk : ∑ y, μ y=k)
    (hg : ∀ j<n, ∀ y, g j y ∈ Set.Icc 0 1)
    (hgLip : ∀ j<n, ∀ y z, |g j y-g j z| ≤ T.L*(dist y z/radius r₀ τ j)) :
    ∑ j ∈ range n, max (potential T (radius r₀ τ j) (moveMeasure μ ν x) (g j)-
      potential T (radius r₀ τ j) μ (g j)) 0 ≤
        (2056/γ+coarseBudget T γ δ k p)*moveCost ν x := by
…

    Mentions: OAI.KServer.Pilot.Template, OAI.KServer.Pilot.radius, OAI.KServer.Pilot.potential, OAI.KServer.Pilot.moveMeasure, OAI.KServer.Pilot.coarseBudget, OAI.KServer.Pilot.moveCost

  182. def OAI.KServer.Pilot.driftConstant line 2696
  183. lemma OAI.KServer.Pilot.driftConstant_nonneg line 2700
  184. lemma OAI.KServer.Pilot.log_k_bound line 2709
  185. lemma OAI.KServer.Pilot.driftBudget_le line 2718
  186. theorem OAI.KServer.Pilot.pilot_drift line 2745

    Source documentation

    Section06's drift inequality with the stated dimension-free constant. The sole scale parameter p only needs the displayed fixed geometric offset.

    theorem pilot_drift {T : Template} {γ δ r₀ τ k : ℝ} {μ ν : Y → ℝ} {x : Y}
    (g : ℕ → Y → ℝ) (n p : ℕ)
    (hr : 0 < r₀) (hτ : 2 ≤ τ) (hγ0 : 0 < γ)
    (hγ : γ ≤ min (T.σ/64) (1/(1+T.L))) (hδ0 : 0 < δ) (hδ : δ ≤ 1/4112)
    (hpow : 100*T.R ≤ γ*(2:ℝ)^p)
    (hμ : ∀ y, 0 ≤ μ y) (hν : ∀ y, 0 ≤ ν y) (hνμ : ∀ y, ν y ≤ μ y)
    (hν1 : ∑ y, ν y=1) (hk : ∑ y, μ y=k)
    (hg : ∀ j<n, ∀ y, g j y ∈ Set.Icc 0 1)
    (hgLip : ∀ j<n, ∀ y z, |g j y-g j z| ≤ T.L*(dist y z/radius r₀ τ j)) :
    ∑ j ∈ range n, max (potential T (radius r₀ τ j) (moveMeasure μ ν x) (g j)-
      potential T (radius r₀ τ j) μ (g j)) 0 ≤
        driftConstant T γ δ p*(1+Real.log (k+1))*moveCost ν x := by
…

    Mentions: OAI.KServer.Pilot.Template, OAI.KServer.Pilot.radius, OAI.KServer.Pilot.potential, OAI.KServer.Pilot.moveMeasure, OAI.KServer.Pilot.driftConstant, OAI.KServer.Pilot.moveCost

  187. lemma OAI.KServer.Pilot.potential_average line 2772

    Source documentation

    A finite weighted average obeys the filtering inequality directly by comparing all posterior minima to the single old minimizer. This is the exact concavity argument, without an assumed filtering/policy interface.

    lemma potential_average {Ω : Type*} [Fintype Ω] (w : Ω → ℝ) (hw : ∀ ω, 0 ≤ w ω)
    (_ : ∑ ω, w ω=1) (T : Template) (r : ℝ) (g : Y → ℝ) (μ : Ω → Y → ℝ) :
    ∑ ω, w ω*potential T r (μ ω) g ≤
      potential T r (fun y => ∑ ω, w ω*μ ω y) g := by
…

    Mentions: OAI.KServer.Pilot.Template, OAI.KServer.Pilot.potential