OAI/Combinatorics/UniformKServer/PilotDrift.lean

GitHub source file

1 declarations, 0 contain sorry, 0 declared as axioms

1. theorem OAI.UniformKServer.PilotCompact.pilot_drift line 16

   Source documentation

   Companion §06, Lemma pilot-drift, in increasing scale order (the finite source list is its reversal). The integer p is any fixed scale-shift with 2^p γ ≥ 100R; the source uses ceil(log₂(100R/γ)). No drift estimate is assumed.

   theorem pilot_drift (r τ σ R γ δ L : ℝ) (N p k : ℕ)
       (hr : 0 < r) (hτ : 2 ≤ τ) (hσ : 0 < σ) (hσ1 : σ ≤ 1) (hR : 256 ≤ R)
       (hL : 0 ≤ L) (hγ : 0 < γ) (hγσ : γ ≤ σ/64) (hγL : γ ≤ 1/(1+L))
       (hδ : 0 < δ) (hδbound : δ ≤ 1/4112) (hk : 2 ≤ k)
       (hp : 100*R ≤ γ*(2:ℝ)^p)
       (μ ν : X → ℝ) (g : ℕ → X → ℝ) (x : X)
       (hμ : ∀ y, 0 ≤ μ y) (hμk : ∑ y, μ y = k)
       (hν : ∀ y, 0 ≤ ν y) (hν1 : ∑ y, ν y = 1) (hνμ : ∀ y, ν y ≤ μ y)
       (hg : ∀ j y, g j y ∈ Set.Icc (0:ℝ) 1)
       (hgLip : ∀ j y z, |g j y-g j z| ≤ L*(dist y z/(r*τ^j))) :
       (∑ j ∈ Finset.range N,
         max (value (r*τ^j) σ R (fun y => μ y-ν y+if y=x then 1 else 0) (g j) -
   …

   Mentions: OAI.UniformKServer.PilotCompact.value