DomainTransport.lean`

19 declarations, 0 contain sorry, 0 declared as axioms

Zero-extension and the exact prepared domain-change operation in companion §04. Departing coordinates are NOT erased until the minimizing feasibility inequalities have been obtained for the synthetic common-core input.

def OAI.UniformKServer.DomainTransport.Supported line 19
def OAI.UniformKServer.DomainTransport.extend line 21
def OAI.UniformKServer.DomainTransport.simplex line 23
def OAI.UniformKServer.DomainTransport.domain line 26
theorem OAI.UniformKServer.DomainTransport.sum_restrict line 29
theorem OAI.UniformKServer.DomainTransport.extend_supported line 35
theorem OAI.UniformKServer.DomainTransport.extend_apply line 40
theorem OAI.UniformKServer.DomainTransport.extend_sum line 43
theorem OAI.UniformKServer.DomainTransport.restrict_simplex line 49
theorem OAI.UniformKServer.DomainTransport.extend_simplex line 54
theorem OAI.UniformKServer.DomainTransport.exists_simplex line 65
theorem OAI.UniformKServer.DomainTransport.potential_extend line 74
theorem OAI.UniformKServer.DomainTransport.potential_restrict line 86
theorem OAI.UniformKServer.DomainTransport.movement_extend line 91

theorem OAI.UniformKServer.DomainTransport.lift_update line 106

Source documentation

Lift an actual compact minimizing update; no conclusion is assumed about the full-domain state. The premise is the already-proved subtype update.

theorem lift_update {I : Finset ι} {g : ι → ℝ → ℝ} {B h a₀ : ι → ℝ} {ell ct : ℝ}
    (hB : Supported I B) (ha₀ : simplex I a₀) (hg : ∀ i, i ∉ I → g i 0=0)
    (hu : AlphaTracker.UpdateConclusion (fun i : I => g i) (fun i : I => B i)
      (fun i : I => h i) ell ct (fun i : I => a₀ i)) :
    ∃ a, simplex I a ∧ (∀ i, (∑ j, B j)*a i ≤ (1+ct*h i/ell)*B i) ∧
      (∑ j, B j)*SimplexTracker.movement a a₀ ≤
        (∑ i, g i (a₀ i))-(∑ i, g i (a i)) := by
…

Mentions: OAI.UniformKServer.DomainTransport.Supported, OAI.UniformKServer.DomainTransport.simplex, OAI.UniformKServer.AlphaTracker.UpdateConclusion, OAI.UniformKServer.SimplexTracker.movement

theorem OAI.UniformKServer.DomainTransport.prepared_alpha line 128
Source documentation
Preparation with common-core input makes deletion and zero insertion free. At zero common input the entire alpha primitive is zero, so redistribution on the new nonempty domain does not spend weighted movement or potential.
```
theorem prepared_alpha {I J : Finset ι} {a B : ι → ℝ} {S : ℝ}
    (ha : simplex I a) (hJ : J.Nonempty) (hS : 0 ≤ S)
    (hf : ∀ i, i ∉ J → S*a i ≤ B i) (hB : Supported J B)
    (g : ι → ℝ → ℝ) (hg : S=0 → ∀ i x, g i x=0) :
    ∃ b, simplex J b ∧ S*SimplexTracker.movement b a=0 ∧
      (∑ i, g i (b i))=∑ i, g i (a i) := by
…
```
Mentions: OAI.UniformKServer.DomainTransport.simplex, OAI.UniformKServer.DomainTransport.Supported, OAI.UniformKServer.SimplexTracker.movement
def OAI.UniformKServer.DomainTransport.delete line 147
theorem OAI.UniformKServer.DomainTransport.delete_domain line 149

theorem OAI.UniformKServer.DomainTransport.prepared_side line 161

Source documentation

Exact side primitive is unchanged by prepared deletion, including D=0.

theorem prepared_side {I J : Finset ι} {w B θ z : ι → ℝ} {W D b C : ℝ}
    (hw : domain I W w) (hD : 0 ≤ D) (hB : Supported J B)
    (hf : ∀ i, i ∉ J → D*w i ≤ (b+θ i)*B i) :
    domain J W (delete J w) ∧ D*SideTracker.movement (delete J w) w=0 ∧
      SideTracker.potential b C D θ z B (delete J w)=SideTracker.potential b C D θ z B w := by
…

Mentions: OAI.UniformKServer.DomainTransport.domain, OAI.UniformKServer.DomainTransport.Supported, OAI.UniformKServer.DomainTransport.delete, OAI.UniformKServer.SideTracker.movement, OAI.UniformKServer.SideTracker.potential