AdaptiveAlpha.lean`

15 declarations, 0 contain sorry, 0 declared as axioms

The two compact minimizations and intermediate common-core transport of companion §04, on a fixed child set. All movement estimates use the actual weighted L1 distance, including changing active domains and singleton states.

structure OAI.UniformKServer.AdaptiveAlpha.Config line 20
def OAI.UniformKServer.AdaptiveAlpha.valid line 24
def OAI.UniformKServer.AdaptiveAlpha.potential line 26
def OAI.UniformKServer.AdaptiveAlpha.eta line 29
def OAI.UniformKServer.AdaptiveAlpha.scale line 32
theorem OAI.UniformKServer.AdaptiveAlpha.scale_nonneg line 35
theorem OAI.UniformKServer.AdaptiveAlpha.potential_zero line 39
theorem OAI.UniformKServer.AdaptiveAlpha.update line 42
theorem OAI.UniformKServer.AdaptiveAlpha.input_bound line 64
theorem OAI.UniformKServer.AdaptiveAlpha.diameter line 73
theorem OAI.UniformKServer.AdaptiveAlpha.triangle line 81
theorem OAI.UniformKServer.AdaptiveAlpha.movement_nonneg line 87

theorem OAI.UniformKServer.AdaptiveAlpha.weight_comparison line 93

Source documentation

A slightly sharper (two rather than four) weight-change error is available by applying the diameter bound after transport. In particular it proves the source's four-delta inequality, with no positive-weight division.

theorem weight_comparison {I J K : Finset ι} {old prep moved new : ι → ℝ}
    {S T : ℝ} (hS : 0 ≤ S) (hST : S ≤ T)
    (hold : DomainTransport.simplex I old) (hmoved : DomainTransport.simplex J moved)
    (hnew : DomainTransport.simplex K new)
    (hfree : S*SimplexTracker.movement moved prep=0) :
    T*SimplexTracker.movement new old ≤
      S*SimplexTracker.movement prep old+T*SimplexTracker.movement new moved+4*(T-S) := by
…

Mentions: OAI.UniformKServer.DomainTransport.simplex, OAI.UniformKServer.SimplexTracker.movement

theorem OAI.UniformKServer.AdaptiveAlpha.prepare line 110

Source documentation

The first minimizer and genuine (possibly zero-weight) domain transport. Feasibility is proved before changing domains, not imposed on the old state.

theorem prepare {p q : Config ι} (hp : valid p) (hq : valid q)
    (B a₀ : ι → ℝ) (hB : ∀ i, 0 ≤ B i)
    (hpB : DomainTransport.Supported p.active B) (hqB : DomainTransport.Supported q.active B)
    (ha₀ : DomainTransport.simplex p.active a₀) :
    ∃ a b, DomainTransport.simplex p.active a ∧ DomainTransport.simplex q.active b ∧
      (∀ i, (∑ j, B j)*a i ≤ (1+eta p i)*B i) ∧
      (∑ j, B j)*SimplexTracker.movement a a₀ ≤ potential p B a₀-potential p B a ∧
      (∑ j, B j)*SimplexTracker.movement b a=0 ∧
      potential p B b=potential p B a ∧
      (∀ i, (∑ j, B j)*b i ≤ (1+eta p i)*B i) := by
…

Mentions: OAI.UniformKServer.AdaptiveAlpha.Config, OAI.UniformKServer.AdaptiveAlpha.valid, OAI.UniformKServer.DomainTransport.Supported, OAI.UniformKServer.DomainTransport.simplex, OAI.UniformKServer.AdaptiveAlpha.eta, OAI.UniformKServer.SimplexTracker.movement, OAI.UniformKServer.AdaptiveAlpha.potential

theorem OAI.UniformKServer.AdaptiveAlpha.step line 143

Source documentation

Complete deterministic minimizing part of one nonswitch step. jump is not a hypothesis: it is the actual prepared parameter-potential difference, available next for componentwise size-charge estimates.

theorem step {p q : Config ι} (hp : valid p) (hq : valid q)
    (Bstar Bnew a₀ : ι → ℝ) (hB : ∀ i, 0 ≤ Bstar i) (hBn : ∀ i, 0 ≤ Bnew i)
    (hST : (∑ i, Bstar i) ≤ ∑ i, Bnew i)
    (hpB : DomainTransport.Supported p.active Bstar)
    (hqB : DomainTransport.Supported q.active Bstar)
    (hqN : DomainTransport.Supported q.active Bnew)
    (ha₀ : DomainTransport.simplex p.active a₀) :
    ∃ a b, DomainTransport.simplex q.active a ∧ DomainTransport.simplex q.active b ∧
      (∀ i, (∑ j, Bnew j)*a i ≤ (1+eta q i)*Bnew i) ∧
      (∀ i, (∑ j, Bstar j)*b i ≤ (1+eta p i)*Bstar i) ∧
      (∑ j, Bnew j)*SimplexTracker.movement a a₀ ≤
        potential p Bstar a₀-potential q Bnew a+
…