OAI/Combinatorics/UniformKServer/AdaptiveSide.lean

GitHub source file

23 declarations, 0 contain sorry, 0 declared as axioms

Actual side-domain update with the exact held height/offset parameters. The source leaves fixed absolute constants flexible; W=11, C'=28 apply in the eventual b≤4, θ≤1 parameter interval. Empty side domains are included.

  1. structure OAI.UniformKServer.AdaptiveSide.Config line 21
  2. def OAI.UniformKServer.AdaptiveSide.theta line 29
  3. def OAI.UniformKServer.AdaptiveSide.offset line 31
  4. def OAI.UniformKServer.AdaptiveSide.valid line 34
  5. def OAI.UniformKServer.AdaptiveSide.potential line 38
  6. def OAI.UniformKServer.AdaptiveSide.slope line 41
  7. theorem OAI.UniformKServer.AdaptiveSide.theta_pos line 44
  8. theorem OAI.UniformKServer.AdaptiveSide.offset_pos line 50
  9. theorem OAI.UniformKServer.AdaptiveSide.theta_le line 55
  10. theorem OAI.UniformKServer.AdaptiveSide.slope_nonneg line 60
  11. theorem OAI.UniformKServer.AdaptiveSide.coordinate_zero line 65
  12. theorem OAI.UniformKServer.AdaptiveSide.restrict_potential line 68
  13. theorem OAI.UniformKServer.AdaptiveSide.restrict_domain line 76
  14. theorem OAI.UniformKServer.AdaptiveSide.extend_domain line 82
  15. theorem OAI.UniformKServer.AdaptiveSide.update line 93
  16. theorem OAI.UniformKServer.AdaptiveSide.parameter_bounds line 127
  17. theorem OAI.UniformKServer.AdaptiveSide.coordinate_bound line 144
  18. theorem OAI.UniformKServer.AdaptiveSide.coordinate_le_sum line 160
  19. theorem OAI.UniformKServer.AdaptiveSide.input_bound line 164
  20. theorem OAI.UniformKServer.AdaptiveSide.theta_nonneg line 187
  21. theorem OAI.UniformKServer.AdaptiveSide.prepare line 192
  22. theorem OAI.UniformKServer.AdaptiveSide.triangle line 210
  23. theorem OAI.UniformKServer.AdaptiveSide.step line 219

    Source documentation

    Actual two-minimizer nonswitch operation. Parameter change is left as the exact prepared difference for the following size-charge lemma, not an assumed movement estimate. Both minimizations use the new nonnegative D.

    theorem step {p q : Config ι} (hp : valid p) (hq : valid q)
    (Bstar Bnew w₀ : ι → ℝ) (D S : ℝ) (hD : 0 ≤ D)
    (hB : ∀ i, 0 ≤ Bstar i) (hBn : ∀ i, 0 ≤ Bnew i)
    (hS : (∑ i, Bnew i) ≤ S)
    (hpB : DomainTransport.Supported p.active Bstar)
    (hqB : DomainTransport.Supported q.active Bstar)
    (hqN : DomainTransport.Supported q.active Bnew)
    (hw₀ : DomainTransport.domain p.active 11 w₀) :
    ∃ w b, DomainTransport.domain q.active 11 w ∧ DomainTransport.domain q.active 11 b ∧
      (∀ i, D*w i ≤ (q.b+theta q i)*Bnew i) ∧
      (S ≤ 2*D → ∀ i, q.b*Bnew i-theta q i*offset q i*D ≤ D*w i) ∧
      (∀ i, D*b i ≤ (p.b+theta p i)*Bstar i) ∧
…

    Mentions: OAI.UniformKServer.AdaptiveSide.Config, OAI.UniformKServer.AdaptiveSide.valid, OAI.UniformKServer.DomainTransport.Supported, OAI.UniformKServer.DomainTransport.domain, OAI.UniformKServer.AdaptiveSide.theta, OAI.UniformKServer.AdaptiveSide.offset