PilotEdits.lean`

14 declarations, 0 contain sorry, 0 declared as axioms

structure OAI.UniformKServer.PilotEdits.Template line 16
Source documentation
A fixed admissible pilot template, independent of the input law and horizon.
```
structure Template where
…
```
def OAI.UniformKServer.PilotEdits.rate line 34
def OAI.UniformKServer.PilotEdits.average line 38
def OAI.UniformKServer.PilotEdits.potential line 40
structure OAI.UniformKServer.PilotEdits.Flow line 48
Source documentation
Finite form of the posterior identity of the source. filtered t is the new pre-move posterior at step t+1; post t is the previous post-move measure. The test-function identity is over every old measurable function, not merely on an event selected later by the edit rule.
```
structure Flow (X Ω : Type*) [Fintype X] [Fintype Ω] (k : ℕ) where
…
```
def OAI.UniformKServer.PilotEdits.moverCost line 71
lemma OAI.UniformKServer.PilotEdits.average_add line 81
lemma OAI.UniformKServer.PilotEdits.average_sub line 85
lemma OAI.UniformKServer.PilotEdits.average_smul line 89
lemma OAI.UniformKServer.PilotEdits.average_mono line 96
lemma OAI.UniformKServer.PilotEdits.potential_bounds line 100
lemma OAI.UniformKServer.PilotEdits.potential_filtering line 124
lemma OAI.UniformKServer.PilotEdits.potential_drift line 155

theorem OAI.UniformKServer.PilotEdits.pilot_edits line 195

Source documentation

The finite-family pilot edit budget, companion Corollary pilot-edits. All constants on the right are fixed before choosing the law and horizon.

theorem pilot_edits {k : ℕ} (hk : 2 ≤ k) (F : Flow X Ω k)
    (T : I → Template) (a : I → ℝ) (ha : ∀ i, 0 ≤ a i)
    (r τ : ℝ) (hr : 0 < r) (hτ : 2 ≤ τ) (N H : ℕ)
    (g : ℕ → Ω → I → ℕ → X → ℝ)
    (hg : ∀ t ω i j y, g t ω i j y ∈ Set.Icc (0:ℝ) 1)
    (hLip : ∀ t ω i j y z, |g t ω i j y-g t ω i j z| ≤
      (T i).L*(dist y z/(r*τ^j)))
    (hmeas : ∀ t i j ω ω', (F.filtration t).r ω ω' → g t ω i j = g t ω' i j)
    (charge : ℕ → Ω → ℝ) (_hc : ∀ t ω, 0 ≤ charge t ω)
    (hedit : ∀ t ω, charge t ω ≤
      potential T a r τ N (F.post (t+1) ω) (g t ω) -
        potential T a r τ N (F.post (t+1) ω) (g (t+1) ω)) :
…

Mentions: OAI.UniformKServer.PilotEdits.Flow, OAI.UniformKServer.PilotEdits.Template, OAI.UniformKServer.PilotEdits.potential