OAI/Combinatorics/UniformKServer/PilotFiltering.lean

GitHub source file

4 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.UniformKServer.PilotCompact.minimizer line 12
2. theorem OAI.UniformKServer.PilotCompact.minimizer_feasible line 15
3. theorem OAI.UniformKServer.PilotCompact.minimizer_value line 19
4. theorem OAI.UniformKServer.PilotCompact.filtering line 25

   Source documentation

   The old template is measurable before the edit decision. In particular, this theorem is never conditional on the event that an edit is selected.

   theorem filtering (r σ R : ℝ) (w : Ω → ℝ) (F : Setoid Ω)
       (μold μminus g : Ω → X → ℝ)
       (hw : ∀ ω, 0 ≤ w ω)
       (hμ : ∀ ω ω', F.r ω ω' → μold ω = μold ω')
       (hg : ∀ ω ω', F.r ω ω' → g ω = g ω')
       (hfilter : ∀ (a : Ω → ℝ), (∀ ω ω', F.r ω ω' → a ω = a ω') →
         ∀ y, (∑ ω, w ω * a ω * (μminus ω y - μold ω y)) = 0) :
       (∑ ω, w ω * value r σ R (μminus ω) (g ω)) ≤
         ∑ ω, w ω * value r σ R (μold ω) (g ω) := by
   …

   Mentions: OAI.UniformKServer.PilotCompact.value