OAI/Combinatorics/UniformKServer/AlphaLinear.lean

GitHub source file

7 declarations, 0 contain sorry, 0 declared as axioms

1. theorem OAI.UniformKServer.AlphaLinear.primitive_linear line 16
2. def OAI.UniformKServer.AlphaLinear.potential line 36
3. def OAI.UniformKServer.AlphaLinear.coefficient line 40
4. theorem OAI.UniformKServer.AlphaLinear.potential_affine line 45
5. theorem OAI.UniformKServer.AlphaLinear.coefficient_of_lipschitz line 74

   Source documentation

   An affine functional's coefficients inherit its exact L1 input bound.

   theorem coefficient_of_lipschitz [DecidableEq ι] (f : (ι → ℝ) → ℝ) (c : ι → ℝ)
       (L : ℝ) (hf : ∀ B, f B=∑ i, c i*B i)
       (hLip : ∀ B B', |f B-f B'| ≤ L*(∑ i, |B i-B' i|)) (j : ι) : |c j| ≤ L := by
   …

6. theorem OAI.UniformKServer.AlphaLinear.regular_coefficient line 82

   Source documentation

   All regular old-state coefficients, independent of the active dimension.

   theorem regular_coefficient [DecidableEq ι] (h η a : ι → ℝ) (scale E : ℝ)
       (hh : ∀ i, 1 ≤ h i) (ha : ∀ i, a i ∈ Icc (0:ℝ) 1)
       (hasum : ∑ i, a i=1) (hη : ∀ i, 0 ≤ η i) (hηE : ∀ i, η i ≤ E) (j : ι) :
       |coefficient (fun i => regular (h i)) (fun _ => 0) η scale a j| ≤ |scale| *(2+E) := by
   …

   Mentions: OAI.UniformKServer.AlphaLinear.coefficient

7. theorem OAI.UniformKServer.AlphaLinear.marked_coefficient line 96

   Source documentation

   Marked coefficients are bounded before filtering or selecting a change event; no lower bound on the new or old side parameter is introduced.

   theorem marked_coefficient [DecidableEq ι] (o : ι) (u : ℝ)
       (h η a : ι → ℝ) (scale E : ℝ) (hu : 0 < u) (hu₁ : u ≤ 1)
       (hh : ∀ i, i ≠ o → 1 ≤ h i) (ha : ∀ i, a i ∈ Icc (0:ℝ) 1)
       (hasum : ∑ i, a i=1) (hη : ∀ i, 0 ≤ η i) (hηE : ∀ i, η i ≤ E) (j : ι) :
       |coefficient (fun i => if i=o then marked u else regular (h i))
         (fun i => if i=o then 1 else 0) η scale a j| ≤ |scale| * (11+4*E) := by
   …

   Mentions: OAI.UniformKServer.AlphaLinear.coefficient