OAI/Combinatorics/KServer/AllocationMovement.lean

GitHub source file

41 declarations, 0 contain sorry, 0 declared as axioms

1. lemma OAI.KServer.OutputDynamics.holesI_movement_subprob line 15
2. lemma OAI.KServer.OutputDynamics.outputI_movement_subprob line 29
3. lemma OAI.KServer.OutputDynamics.variation_divide line 39
4. lemma OAI.KServer.OutputDynamics.restricted_variation_le line 43
5. def OAI.KServer.OutputDynamics.residual line 49

   Source documentation

   The same residual formula as Rule II on a fixed star universe.

   def residual (o:J) (d:J→ℝ) (q D:ℝ) (w:J→ℝ):J→ℝ:=
   …

6. lemma OAI.KServer.OutputDynamics.residual_movement line 52
7. def OAI.KServer.OutputDynamics.residualHoles line 110
8. lemma OAI.KServer.OutputDynamics.residualHoles_nonneg line 113
9. lemma OAI.KServer.OutputDynamics.residualHoles_mass line 123
10. lemma OAI.KServer.OutputDynamics.residual_eq_sub_holes line 151
11. lemma OAI.KServer.OutputDynamics.holesI_mass_subprob line 157
12. lemma OAI.KServer.OutputDynamics.downcross_fixed line 162
13. lemma OAI.KServer.OutputDynamics.upcross_fixed line 177
14. lemma OAI.KServer.ActualOutput.alpha_subprob line 208
15. lemma OAI.KServer.ActualOutput.error_le_T line 213
16. lemma OAI.KServer.ActualOutput.actual_excess line 226
17. lemma OAI.KServer.ActualOutput.excess_ruleI line 238
18. lemma OAI.KServer.ActualOutput.excess_down line 247
19. lemma OAI.KServer.ActualOutput.outI_movement line 253
20. lemma OAI.KServer.ActualOutput.outII_movement line 264
21. lemma OAI.KServer.ActualOutput.out_downcross line 276
22. lemma OAI.KServer.ActualOutput.out_upcross line 286
23. lemma OAI.KServer.AdaptiveMinimization.actual_payment_step line 315
24. theorem OAI.KServer.AdaptiveMinimization.actual_payment line 362

    Source documentation

    The full causal minimizer telescope. The computed signed edit term must be bounded from the actual coordinate preparation/deletion and coarse schedules; there is no asserted policy or asserted coarse-budget estimate here.

    theorem actual_payment (F : Family Θ I J) (T : Transport F) {w : Ω → ℝ}
        (hw : ∀ ω, 0 ≤ w ω) (R : I → FilteredRanks w)
        (θ : ℕ → Ω → Θ) (c : ℕ → Ω → ℝ)
        (H : ℕ → Ω → ℕ) (hH : ∀ i, (R i).history=H)
        (hr : ∀ t ω z, H (t+1) ω=H (t+1) z → H t ω=H t z)
        (hθ : ∀ t ω z, H t ω=H t z → θ t ω=θ t z)
        (hc : ∀ t, Adapted (H t) (c t)) (hcn : ∀ t ω, 0 ≤ c t ω)
        {L : ℝ} (hL : ∀ t ω a, a ∈ F.domain (θ t ω) → ∀ i, |F.coefficient (θ t ω) a i| ≤ L)
        (n : ℕ) :
        (∑ t ∈ range n, avg w (fun ω => c (t+1) ω*movement
          (state F T θ (rankVector R) c (t+1) ω) (state F T θ (rankVector R) c t ω))) ≤
        avg w (fun ω => F.value (θ 0 ω) (rankVector R 0 ω) (state F T θ (rankVector R) c 0 ω))-
    …

    Mentions: OAI.KServer.AdaptiveMinimization.Family, OAI.KServer.AdaptiveMinimization.Transport, OAI.KServer.AdaptiveMinimization.movement, OAI.KServer.AdaptiveMinimization.state, OAI.KServer.AdaptiveMinimization.rankVector

25. theorem OAI.KServer.AdaptiveMinimization.actual_payment_bounded line 386

    Source documentation

    Uniform endpoint removal: a bound depending only on the fixed finite family, not on the horizon or its law, contributes at most twice that bound.

    theorem actual_payment_bounded (F : Family Θ I J) (T : Transport F) {w : Ω → ℝ}
        (hw : ∀ ω, 0 ≤ w ω) (hw1 : ∑ ω, w ω=1) (R : I → FilteredRanks w)
        (θ : ℕ → Ω → Θ) (c : ℕ → Ω → ℝ)
        (H : ℕ → Ω → ℕ) (hH : ∀ i, (R i).history=H)
        (hr : ∀ t ω z, H (t+1) ω=H (t+1) z → H t ω=H t z)
        (hθ : ∀ t ω z, H t ω=H t z → θ t ω=θ t z)
        (hc : ∀ t, Adapted (H t) (c t)) (hcn : ∀ t ω, 0 ≤ c t ω)
        {L B : ℝ} (hL : ∀ t ω a, a ∈ F.domain (θ t ω) → ∀ i, |F.coefficient (θ t ω) a i| ≤ L)
        (hB : ∀ t ω p a, a ∈ F.domain (θ t ω) → (∀ i, p i ∈ Set.Icc 0 1) → |F.value (θ t ω) p a| ≤ B)
        (n : ℕ) :
        (∑ t ∈ range n, avg w (fun ω => c (t+1) ω*movement
          (state F T θ (rankVector R) c (t+1) ω) (state F T θ (rankVector R) c t ω))) ≤
    …

    Mentions: OAI.KServer.AdaptiveMinimization.Family, OAI.KServer.AdaptiveMinimization.Transport, OAI.KServer.AdaptiveMinimization.movement, OAI.KServer.AdaptiveMinimization.state, OAI.KServer.AdaptiveMinimization.rankVector

26. lemma OAI.KServer.ScheduledSlope.coefficient_bound line 425
27. lemma OAI.KServer.ScheduledSlope.actual_bound line 452
28. lemma OAI.KServer.ScheduleEdits.ordinary_reference line 491
29. lemma OAI.KServer.ScheduleEdits.ordinary_mass line 499
30. lemma OAI.KServer.ScheduleEdits.ordinary_mark line 504
31. lemma OAI.KServer.ScheduleEdits.ordinary_weight line 510
32. lemma OAI.KServer.ScheduleEdits.count_bound line 516
33. lemma OAI.KServer.ScheduleEdits.raw_core_bound line 530
34. lemma OAI.KServer.ScheduleEdits.prepared_input_bound line 540
35. lemma OAI.KServer.ScheduleEdits.regular_charge line 554
36. lemma OAI.KServer.ScheduleEdits.side_ratio_charge line 581
37. def OAI.KServer.ActualOutput.switchCharge line 658
38. lemma OAI.KServer.ActualOutput.switchCharge_nonneg line 662
39. lemma OAI.KServer.ActualOutput.reset_iff line 666
40. lemma OAI.KServer.ActualOutput.ordinary_mark line 673
41. lemma OAI.KServer.ActualOutput.ordinary_movement line 677