OAI/Combinatorics/UniformKServer/BalancedRepair.lean

GitHub source file

35 declarations, 0 contain sorry, 0 declared as axioms

  1. abbrev OAI.UniformKServer.BalancedRepair.Joint line 16
  2. def OAI.UniformKServer.BalancedRepair.admissible line 18
  3. def OAI.UniformKServer.BalancedRepair.marginal line 22
  4. def OAI.UniformKServer.BalancedRepair.discrepancy line 25
  5. def OAI.UniformKServer.BalancedRepair.hamming line 28
  6. def OAI.UniformKServer.BalancedRepair.cost line 31
  7. def OAI.UniformKServer.BalancedRepair.initial line 34
  8. def OAI.UniformKServer.BalancedRepair.objective line 37
  9. theorem OAI.UniformKServer.BalancedRepair.initial_admissible line 42
  10. theorem OAI.UniformKServer.BalancedRepair.total_mass line 60
  11. theorem OAI.UniformKServer.BalancedRepair.initial_cost line 66
  12. theorem OAI.UniformKServer.BalancedRepair.admissible_compact line 76
  13. theorem OAI.UniformKServer.BalancedRepair.objective_continuous line 102
  14. theorem OAI.UniformKServer.BalancedRepair.minimizer_exists line 108
  15. def OAI.UniformKServer.BalancedRepair.transfer line 116
  16. theorem OAI.UniformKServer.BalancedRepair.sum_transfer line 119
  17. theorem OAI.UniformKServer.BalancedRepair.transfer_admissible line 130
  18. def OAI.UniformKServer.BalancedRepair.exchange line 167
  19. theorem OAI.UniformKServer.BalancedRepair.exchange_card line 170
  20. theorem OAI.UniformKServer.BalancedRepair.exchange_indicator line 177
  21. theorem OAI.UniformKServer.BalancedRepair.exchange_hamming line 188
  22. def OAI.UniformKServer.BalancedRepair.swap line 204
  23. theorem OAI.UniformKServer.BalancedRepair.swap_admissible line 208
  24. theorem OAI.UniformKServer.BalancedRepair.swap_marginal line 215
  25. theorem OAI.UniformKServer.BalancedRepair.swap_cost line 225
  26. theorem OAI.UniformKServer.BalancedRepair.discrepancy_transfer line 233
  27. theorem OAI.UniformKServer.BalancedRepair.sum_marginal line 261
  28. theorem OAI.UniformKServer.BalancedRepair.supported_card line 282
  29. theorem OAI.UniformKServer.BalancedRepair.supported_mem line 289
  30. theorem OAI.UniformKServer.BalancedRepair.supported_notMem line 299
  31. theorem OAI.UniformKServer.BalancedRepair.four_positive line 313
  32. theorem OAI.UniformKServer.BalancedRepair.exchange_intermediate line 322
  33. theorem OAI.UniformKServer.BalancedRepair.discrepancy_pair line 339
  34. theorem OAI.UniformKServer.BalancedRepair.minimizer_exact line 352
  35. theorem OAI.UniformKServer.BalancedRepair.repair line 428

    Source documentation

    A finite kernel repairs all coordinate means while keeping each actual state's prescribed total, even when the total is correlated with the old vector.

    theorem repair (μ : Ω → ℝ) (r : Ω → ℕ) (base : Ω → Finset ι) (f : ι → ℝ)
    (hμ : ∀ ω, 0 ≤ μ ω) (hμsum : ∑ ω, μ ω = 1)
    (hbase : ∀ ω, (base ω).card = r ω)
    (s : ℕ) (hr : ∀ ω, r ω = s ∨ r ω = s+1)
    (hf : ∀ i, f i ∈ Set.Icc (0 : ℝ) 1)
    (hsum : ∑ i, f i = ∑ ω, μ ω * (r ω : ℝ)) :
    ∃ g : Joint Ω ι, admissible μ r g ∧ (∀ i, marginal g i = f i) ∧
      cost base g ≤ 10 * discrepancy f (initial μ base) := by
…

    Mentions: OAI.UniformKServer.BalancedRepair.Joint, OAI.UniformKServer.BalancedRepair.admissible, OAI.UniformKServer.BalancedRepair.marginal, OAI.UniformKServer.BalancedRepair.cost, OAI.UniformKServer.BalancedRepair.discrepancy, OAI.UniformKServer.BalancedRepair.initial