SyntheticCore.lean`

12 declarations, 0 contain sorry, 0 declared as axioms

Common-core preparation in the adaptive allocation update, companion eqs. synthetic-core-input and synthetic-core-errors. All input probabilities here are the NEW posteriors, including when used with the old flags.

def OAI.UniformKServer.SyntheticCore.input line 16
def OAI.UniformKServer.SyntheticCore.changes line 18
theorem OAI.UniformKServer.SyntheticCore.input_nonneg line 20
theorem OAI.UniformKServer.SyntheticCore.changes_nonneg line 27
theorem OAI.UniformKServer.SyntheticCore.no_flags line 32
theorem OAI.UniformKServer.SyntheticCore.input_difference line 35
def OAI.UniformKServer.SyntheticCore.core line 43
def OAI.UniformKServer.SyntheticCore.Supported line 47
Source documentation
Inactivity entails an empty core, not merely a zero observed value.
```
def Supported (active : ι → Bool) (flag : ι → κ → Bool) : Prop :=
…
```
theorem OAI.UniformKServer.SyntheticCore.core_le_new line 51
theorem OAI.UniformKServer.SyntheticCore.old_core_difference line 60
theorem OAI.UniformKServer.SyntheticCore.new_core_difference line 78

theorem OAI.UniformKServer.SyntheticCore.errors line 97

Source documentation

All three source errors, on the fixed child set with zero extension.

theorem errors (old new : ι → Bool) (p : ι → κ → ℝ)
    (f g : ι → κ → Bool) (hp : ∀ i j, p i j ∈ Set.Icc (0:ℝ) 1)
    (hf : Supported old f) (hg : Supported new g) :
    (∑ i, |input (p i) (f i)-core old new p g i|) ≤ ∑ i, changes (f i) (g i) ∧
    (∑ i, |input (p i) (g i)-core old new p g i|) ≤ ∑ i, changes (f i) (g i) ∧
    0 ≤ (∑ i, input (p i) (g i))-(∑ i, core old new p g i) ∧
    (∑ i, input (p i) (g i))-(∑ i, core old new p g i) ≤ ∑ i, changes (f i) (g i) := by
…

Mentions: OAI.UniformKServer.SyntheticCore.Supported, OAI.UniformKServer.SyntheticCore.input, OAI.UniformKServer.SyntheticCore.core, OAI.UniformKServer.SyntheticCore.changes