Minimization.lean`

58 declarations, 0 contain sorry, 0 declared as axioms

Actual zero-extension and synthetic-input operations in §04. In particular zero weight and singleton transitions are included, not divided away.

lemma OAI.KServer.AdaptiveMinimization.avg_sum_any line 13
structure OAI.KServer.AdaptiveMinimization.Family line 19
Source documentation
The source primitives are affine in the rank inputs when the held parameters and the state are fixed. Both simplex and side domains are compact.
```
structure Family (Θ : Type*) (I J : Type*) [Fintype I] [Fintype J] where
…
```
def OAI.KServer.AdaptiveMinimization.Family.value line 28
def OAI.KServer.AdaptiveMinimization.movement line 31
lemma OAI.KServer.AdaptiveMinimization.movement_nonneg line 33
lemma OAI.KServer.AdaptiveMinimization.movement_self line 36
lemma OAI.KServer.AdaptiveMinimization.movement_triangle line 38
lemma OAI.KServer.AdaptiveMinimization.Family.value_continuous line 43
lemma OAI.KServer.AdaptiveMinimization.movement_continuous line 48
lemma OAI.KServer.AdaptiveMinimization.Family.exists_update line 51
def OAI.KServer.AdaptiveMinimization.Family.update line 58
Source documentation
A fixed noncomputable selection, only from the currently supplied data.
```
def Family.update (F : Family Θ I J) (θ : Θ) (p : I → ℝ) (c : ℝ) (a : J → ℝ) : J → ℝ :=
…
```
Mentions: OAI.KServer.AdaptiveMinimization.Family
lemma OAI.KServer.AdaptiveMinimization.Family.update_mem line 61
lemma OAI.KServer.AdaptiveMinimization.Family.update_payment line 64
lemma OAI.KServer.AdaptiveMinimization.Family.input_difference line 73
lemma OAI.KServer.AdaptiveMinimization.Family.input_lipschitz line 78
structure OAI.KServer.AdaptiveMinimization.Transport line 90
Source documentation
Domain transport is computed from old/new held parameters and new rank inputs. For the manuscript it is the prepared update followed by deletion and zero insertion. It is not permitted to depend on the unrealized future.
```
structure Transport (F : Family Θ I J) where
…
```
Mentions: OAI.KServer.AdaptiveMinimization.Family
def OAI.KServer.AdaptiveMinimization.state line 94
lemma OAI.KServer.AdaptiveMinimization.state_mem line 101

lemma OAI.KServer.AdaptiveMinimization.state_adapted line 111

Source documentation

Causality is proved from the recursion (not a fictitious prefix interface).

lemma state_adapted (F : Family Θ I J) (T : Transport F) (θ : ℕ → Ω → Θ)
    (p : ℕ → Ω → I → ℝ) (c : ℕ → Ω → ℝ) (H : ℕ → Ω → ℕ)
    (hr : ∀ t ω z, H (t+1) ω=H (t+1) z → H t ω=H t z)
    (hθ : ∀ t ω z, H t ω=H t z → θ t ω=θ t z)
    (hp : ∀ t ω z, H t ω=H t z → p t ω=p t z)
    (hc : ∀ t, Adapted (H t) (c t)) :
    ∀ t ω z, H t ω=H t z → state F T θ p c t ω=state F T θ p c t z := by
…

Mentions: OAI.KServer.AdaptiveMinimization.Family, OAI.KServer.AdaptiveMinimization.Transport, OAI.KServer.AdaptiveMinimization.state

def OAI.KServer.AdaptiveMinimization.edit line 131
Source documentation
The signed editing charge, evaluated after filtering and drift but before the final minimizing update. Preparation payments are allowed to lower it.
```
def edit (F : Family Θ I J) (T : Transport F) (θ : ℕ → Ω → Θ)
    (p : ℕ → Ω → I → ℝ) (c : ℕ → Ω → ℝ) (t : ℕ) (ω : Ω) : ℝ :=
…
```
Mentions: OAI.KServer.AdaptiveMinimization.Family, OAI.KServer.AdaptiveMinimization.Transport
lemma OAI.KServer.AdaptiveMinimization.state_payment line 139
def OAI.KServer.AdaptiveMinimization.rankVector line 163
Source documentation
All ranks are taken under the same true observed history.
```
def rankVector {w : Ω → ℝ} (R : I → FilteredRanks w) (t : ℕ) (ω : Ω) : I → ℝ :=
…
```
def OAI.KServer.AdaptiveMinimization.beforeVector line 166
lemma OAI.KServer.AdaptiveMinimization.rankVector_adapted line 170

lemma OAI.KServer.AdaptiveMinimization.filtering_zero line 179

Source documentation

Filtering is used on every step with the old held coefficients, before selecting any ordinary/wholesale event measurable at the new history.

lemma filtering_zero (F : Family Θ I J) (T : Transport F) {w : Ω → ℝ}
    (R : I → FilteredRanks w) (θ : ℕ → Ω → Θ) (c : ℕ → Ω → ℝ)
    (H : ℕ → Ω → ℕ) (hH : ∀ i, (R i).history=H)
    (hr : ∀ t ω z, H (t+1) ω=H (t+1) z → H t ω=H t z)
    (hθ : ∀ t ω z, H t ω=H t z → θ t ω=θ t z)
    (hc : ∀ t, Adapted (H t) (c t)) (t : ℕ) :
    avg w (fun ω =>
      F.value (θ t ω) (beforeVector R (t+1) ω) (state F T θ (rankVector R) c t ω)-
      F.value (θ t ω) (rankVector R t ω) (state F T θ (rankVector R) c t ω))=0 := by
…

Mentions: OAI.KServer.AdaptiveMinimization.Family, OAI.KServer.AdaptiveMinimization.Transport, OAI.KServer.AdaptiveMinimization.beforeVector, OAI.KServer.AdaptiveMinimization.state, OAI.KServer.AdaptiveMinimization.rankVector

lemma OAI.KServer.AdaptiveMinimization.expected_payment_step line 200

theorem OAI.KServer.AdaptiveMinimization.expected_payment line 247

Source documentation

The full causal minimizer telescope. The computed signed edit term must be bounded from the actual coordinate preparation/deletion and coarse schedules; there is no asserted policy or asserted coarse-budget estimate here.

theorem expected_payment (F : Family Θ I J) (T : Transport F) {w : Ω → ℝ}
    (hw : ∀ ω, 0 ≤ w ω) (R : I → FilteredRanks w)
    (θ : ℕ → Ω → Θ) (c : ℕ → Ω → ℝ)
    (H : ℕ → Ω → ℕ) (hH : ∀ i, (R i).history=H)
    (hr : ∀ t ω z, H (t+1) ω=H (t+1) z → H t ω=H t z)
    (hθ : ∀ t ω z, H t ω=H t z → θ t ω=θ t z)
    (hc : ∀ t, Adapted (H t) (c t)) (hcn : ∀ t ω, 0 ≤ c t ω)
    {L : ℝ} (hL : ∀ θ a, a ∈ F.domain θ → ∀ i, |F.coefficient θ a i| ≤ L)
    (n : ℕ) :
    (∑ t ∈ range n, avg w (fun ω => c (t+1) ω*movement
      (state F T θ (rankVector R) c (t+1) ω) (state F T θ (rankVector R) c t ω))) ≤
    avg w (fun ω => F.value (θ 0 ω) (rankVector R 0 ω) (state F T θ (rankVector R) c 0 ω))-
…

Mentions: OAI.KServer.AdaptiveMinimization.Family, OAI.KServer.AdaptiveMinimization.Transport, OAI.KServer.AdaptiveMinimization.movement, OAI.KServer.AdaptiveMinimization.state, OAI.KServer.AdaptiveMinimization.rankVector

theorem OAI.KServer.AdaptiveMinimization.expected_payment_bounded line 271

Source documentation

Uniform endpoint removal: a bound depending only on the fixed finite family, not on the horizon or its law, contributes at most twice that bound.

theorem expected_payment_bounded (F : Family Θ I J) (T : Transport F) {w : Ω → ℝ}
    (hw : ∀ ω, 0 ≤ w ω) (hw1 : ∑ ω, w ω=1) (R : I → FilteredRanks w)
    (θ : ℕ → Ω → Θ) (c : ℕ → Ω → ℝ)
    (H : ℕ → Ω → ℕ) (hH : ∀ i, (R i).history=H)
    (hr : ∀ t ω z, H (t+1) ω=H (t+1) z → H t ω=H t z)
    (hθ : ∀ t ω z, H t ω=H t z → θ t ω=θ t z)
    (hc : ∀ t, Adapted (H t) (c t)) (hcn : ∀ t ω, 0 ≤ c t ω)
    {L B : ℝ} (hL : ∀ θ a, a ∈ F.domain θ → ∀ i, |F.coefficient θ a i| ≤ L)
    (hB : ∀ θ p a, a ∈ F.domain θ → (∀ i, p i ∈ Set.Icc 0 1) → |F.value θ p a| ≤ B)
    (n : ℕ) :
    (∑ t ∈ range n, avg w (fun ω => c (t+1) ω*movement
      (state F T θ (rankVector R) c (t+1) ω) (state F T θ (rankVector R) c t ω))) ≤
…

def OAI.KServer.AdaptiveMinimization.countRanks line 296

Source documentation

The rank inputs of the recursion can be instantiated directly from the actual finite hidden counts, not from a postulated martingale interface.

def countRanks {w : Ω → ℝ} (hw : ∀ ω, 0 ≤ w ω) (H : ℕ → Ω → ℕ)
    (hr : ∀ t ω z, H (t+1) ω=H (t+1) z → H t ω=H t z)
    {k : ℕ} (N : ℕ → Ω → J → ℕ) : J × Fin k → FilteredRanks w :=
…

lemma OAI.KServer.AdaptiveMinimization.countRanks_history line 302
lemma OAI.KServer.AdaptiveMinimization.countRanks_drift line 307

theorem OAI.KServer.AdaptiveMinimization.hidden_count_payment line 320

Source documentation

Hidden-count variation is controlled by the explicit edit expression.

theorem hidden_count_payment {k : ℕ} (F : Family Θ (J × Fin k) J) (T : Transport F)
    {w : Ω → ℝ} (hw : ∀ ω, 0 ≤ w ω) (hw1 : ∑ ω, w ω=1)
    (H : ℕ → Ω → ℕ) (hr : ∀ t ω z, H (t+1) ω=H (t+1) z → H t ω=H t z)
    (N : ℕ → Ω → J → ℕ) (hN : ∀ t ω j, N t ω j ≤ k)
    (θ : ℕ → Ω → Θ) (c : ℕ → Ω → ℝ)
    (hθ : ∀ t ω z, H t ω=H t z → θ t ω=θ t z)
    (hc : ∀ t, Adapted (H t) (c t)) (hcn : ∀ t ω, 0 ≤ c t ω)
    {L B : ℝ} (hLn : 0 ≤ L)
    (hL : ∀ θ a, a ∈ F.domain θ → ∀ i, |F.coefficient θ a i| ≤ L)
    (hB : ∀ θ p a, a ∈ F.domain θ → (∀ i, p i ∈ Set.Icc 0 1) → |F.value θ p a| ≤ B)
    (n : ℕ) :
    let R := countRanks hw H hr N
…

Mentions: OAI.KServer.AdaptiveMinimization.Family, OAI.KServer.AdaptiveMinimization.Transport, OAI.KServer.AdaptiveMinimization.countRanks

def OAI.KServer.ChangingDomains.variation line 354
lemma OAI.KServer.ChangingDomains.variation_self line 357
lemma OAI.KServer.ChangingDomains.variation_nonneg line 359
lemma OAI.KServer.ChangingDomains.variation_triangle line 362
def OAI.KServer.ChangingDomains.simplex line 366
def OAI.KServer.ChangingDomains.canonical line 369
lemma OAI.KServer.ChangingDomains.canonical_mem line 372
lemma OAI.KServer.ChangingDomains.simplex_coordinate line 385
lemma OAI.KServer.ChangingDomains.simplex_compact line 393
lemma OAI.KServer.ChangingDomains.simplex_variation line 410
def OAI.KServer.ChangingDomains.transposeSimplex line 421
Source documentation
Deletion plus zero insertion. At zero synthetic total choose a fresh canonical vector; this has exactly zero synthetic weighted movement.
```
def transposeSimplex (A : Finset J) (S : ℝ) (a : J → ℝ) : J → ℝ :=
…
```
lemma OAI.KServer.ChangingDomains.transposeSimplex_mem line 424
lemma OAI.KServer.ChangingDomains.transposeSimplex_payment line 439

lemma OAI.KServer.ChangingDomains.prepared_weight_comparison line 447

Source documentation

Literal §04 weight comparison for the prepared and final minimizers.

lemma prepared_weight_comparison {A₀ A₁ A₂ : Finset J} {a₀ a₁ a₂ a₃ : J → ℝ}
    (ha₀ : a₀ ∈ simplex A₀) (ha₁ : a₁ ∈ simplex A₁)
    (ha₂ : a₂ ∈ simplex A₂)
    {S T : ℝ} (hS : 0 ≤ S) (hST : S ≤ T)
    (hzero : S*variation a₂ a₁=0) :
    T*variation a₃ a₀ ≤ S*variation a₁ a₀+T*variation a₃ a₂+4*(T-S) := by
…

Mentions: OAI.KServer.ChangingDomains.simplex, OAI.KServer.ChangingDomains.variation

def OAI.KServer.ChangingDomains.sideDomain line 465
def OAI.KServer.ChangingDomains.transposeSide line 468
lemma OAI.KServer.ChangingDomains.transposeSide_mem line 470
lemma OAI.KServer.ChangingDomains.transposeSide_payment line 482
def OAI.KServer.ChangingDomains.core line 499
def OAI.KServer.ChangingDomains.syntheticFlags line 502
def OAI.KServer.ChangingDomains.changedFlags line 505
lemma OAI.KServer.ChangingDomains.core_nonneg line 509
lemma OAI.KServer.ChangingDomains.synthetic_zero line 518
lemma OAI.KServer.ChangingDomains.synthetic_error_terms line 523
theorem OAI.KServer.ChangingDomains.synthetic_errors line 548
Source documentation
Both synthetic-core discrepancies are paid by the actual number of flags that changed, even when the observed rank probabilities changed drastically.
```
theorem synthetic_errors {A B : Finset J} {f g : J → R → Bool}
    {p : J → R → ℝ} (hp : ∀ i a, p i a ∈ Set.Icc 0 1)
    (hf : ∀ i ∉ A, ∀ a, f i a=false) (hg : ∀ i ∉ B, ∀ a, g i a=false) :
    variation (core f p) (core (syntheticFlags A B g) p) ≤ changedFlags f g ∧
    variation (core g p) (core (syntheticFlags A B g) p) ≤ changedFlags f g := by
…
```
Mentions: OAI.KServer.ChangingDomains.variation, OAI.KServer.ChangingDomains.core, OAI.KServer.ChangingDomains.syntheticFlags, OAI.KServer.ChangingDomains.changedFlags
lemma OAI.KServer.ChangingDomains.synthetic_total line 565