AlphaParameterChanges.lean`

11 declarations, 0 contain sorry, 0 declared as axioms

Prepared logarithmic parameter changes. All bounds concern the actual improper primitives, with constants uniform at vanishing side mass.

def OAI.UniformKServer.AlphaParameterChanges.piece line 17
theorem OAI.UniformKServer.AlphaParameterChanges.sum_piece line 21
theorem OAI.UniformKServer.AlphaParameterChanges.piece_outside line 25
theorem OAI.UniformKServer.AlphaParameterChanges.piece_inside line 29

theorem OAI.UniformKServer.AlphaParameterChanges.regular_piece line 34

Source documentation

An ordinary coordinate costs only its prepared input.

theorem regular_piece {p : Config ι} (hp : valid p) (B a : ι → ℝ)
    (hB : ∀ i, 0 ≤ B i) (hs : DomainTransport.Supported p.active B)
    (ha : ∀ i, a i ∈ Set.Icc (0:ℝ) 1)
    (hf : ∀ i, (∑ j, B j)*a i ≤ 2*B i) (i : p.active)
    (he : ProportionParameters.component p.param (fun j => B j) i (a i)=
      AlphaTracker.regularG p.param.h (fun j => B j) p.param.ell p.param.ct p.param.C i (a i))
    (hh : 1 ≤ p.param.h i) : |piece p B a i| ≤ 4*scale p*B i := by
…

Mentions: OAI.UniformKServer.DomainTransport.Supported, OAI.UniformKServer.ProportionParameters.component, OAI.UniformKServer.AlphaTracker.regularG, OAI.UniformKServer.AlphaParameterChanges.piece

theorem OAI.UniformKServer.AlphaParameterChanges.prepared_two line 57

theorem OAI.UniformKServer.AlphaParameterChanges.prepared_side line 69

Source documentation

Sum of prepared side constraints, without division by total input.

theorem prepared_side (B a : ι → ℝ) (ha : ∑ i, a i=1)
    (hf : ∀ i, (∑ j, B j)*a i ≤ 2*B i) (o : ι) :
    (∑ j, B j)*(1-a o) ≤ 2*((∑ j, B j)-B o) := by
…

theorem OAI.UniformKServer.AlphaParameterChanges.regular_jump line 80

Source documentation

A regular epoch, including additions/removals, charges only the coordinates whose parameter piece changes. The indicator is later identified with held size refreshes; no degree factor appears.

theorem regular_jump {p q : Config ι} (hp : valid p) (hq : valid q)
    (hep : p.param.kind=.regular) (heq : q.param.kind=.regular)
    (B a : ι → ℝ) (hB : ∀ i, 0 ≤ B i)
    (hsp : DomainTransport.Supported p.active B) (hsq : DomainTransport.Supported q.active B)
    (ha : ∀ i, a i ∈ Set.Icc (0:ℝ) 1)
    (hf : ∀ i, (∑ j, B j)*a i ≤ 2*B i)
    (changed : ι → Prop) [DecidablePred changed]
    (same : ∀ i, ¬changed i → piece p B a i=piece q B a i) :
    |potential q B a-potential p B a| ≤
      4*(scale p+scale q)*(∑ i, if changed i then B i else 0) := by
…

Mentions: OAI.UniformKServer.DomainTransport.Supported, OAI.UniformKServer.AlphaParameterChanges.piece

theorem OAI.UniformKServer.AlphaParameterChanges.marked_prepared line 110

Source documentation

Whole marked potential on a prepared state. In particular only side input and u times total input are charged when the distinguished parameter changes.

theorem marked_prepared {p : Config ι} (hp : valid p) (o : p.active) (u : ℝ)
    (he : p.param.kind=.marked o u) (B a : ι → ℝ)
    (hB : ∀ i, 0 ≤ B i) (hs : DomainTransport.Supported p.active B)
    (ha : ∀ i, a i ∈ Set.Icc (0:ℝ) 1) (hasum : ∑ i, a i=1)
    (hf : ∀ i, (∑ j, B j)*a i ≤ 2*B i) :
    |potential p B a| ≤ 13*scale p*((∑ i, B i)-B o)+
      3*scale p*(p.param.ct/p.param.ell)*u*(∑ i, B i) := by
…

Mentions: OAI.UniformKServer.DomainTransport.Supported

theorem OAI.UniformKServer.AlphaParameterChanges.marked_sparse_jump line 162

Source documentation

The distinguished summand does not move when its held ratio is unchanged. Only regular side summands remain in a size-refresh charge.

theorem marked_sparse_jump {p q : Config ι} (hp : valid p) (hq : valid q)
    (op : p.active) (oq : q.active) (u : ℝ)
    (hep : p.param.kind=.marked op u) (heq : q.param.kind=.marked oq u)
    (ho : op.val=oq.val) (B a : ι → ℝ) (hB : ∀ i, 0 ≤ B i)
    (hsp : DomainTransport.Supported p.active B) (hsq : DomainTransport.Supported q.active B)
    (ha : ∀ i, a i ∈ Set.Icc (0:ℝ) 1)
    (hf : ∀ i, (∑ j, B j)*a i ≤ 2*B i)
    (changed : ι → Prop) [DecidablePred changed]
    (same : ∀ i, ¬changed i → piece p B a i=piece q B a i)
    (mark : ¬changed op.val) :
    |potential q B a-potential p B a| ≤
      4*(scale p+scale q)*(∑ i, if changed i then B i else 0) := by
…

Mentions: OAI.UniformKServer.DomainTransport.Supported, OAI.UniformKServer.AlphaParameterChanges.piece

theorem OAI.UniformKServer.AlphaParameterChanges.singleton_potential line 202