FineCaps.lean`

6 declarations, 0 contain sorry, 0 declared as axioms

Companion §03, fine cap algebra. The tolerance hypotheses below are the actual absolute choices in Lemma caps; there is no assumed cap feasibility.

theorem OAI.UniformKServer.FineCaps.interpolate line 15

Source documentation

Convex interpolation preserves the same multiplicative endpoint error.

theorem interpolate {a b A B c ξ : ℝ} (hc : c ∈ Set.Icc (0:ℝ) 1)
    (ha : (1+ξ)⁻¹*a ≤ A ∧ A ≤ (1+ξ)*a)
    (hb : (1+ξ)⁻¹*b ≤ B ∧ B ≤ (1+ξ)*b) :
    (1+ξ)⁻¹*((1-c)*a+c*b) ≤ (1-c)*A+c*B ∧
      (1-c)*A+c*B ≤ (1+ξ)*((1-c)*a+c*b) := by
…

theorem OAI.UniformKServer.FineCaps.regular_factor line 27
theorem OAI.UniformKServer.FineCaps.dominant_factor line 32

theorem OAI.UniformKServer.FineCaps.caps line 39

Source documentation

Both explicit factors at once, including zero true flexible mass.

theorem caps {ell lam e T F γ ε f : ℝ} (hell : 1 ≤ ell)
    (hlam : 0 ≤ lam) (hlam' : lam ≤ 1/4) (he : 0 ≤ e) (he' : e ≤ lam/4)
    (hγ : 4*lam ≤ γ) (hε : 4*lam ≤ ε) (hT : 0 ≤ T)
    (hF : |F-T| ≤ (e/ell)*T) (hf : f ≤ (1-γ/ell)*T) :
    (f ≤ (1-lam/ell)*F ∧ (1-lam/ell)*F ≤ T) ∧
      (T ≤ (1+lam/ell)*F ∧ (1+lam/ell)*F ≤ (1+ε/ell)*T) := by
…

theorem OAI.UniformKServer.FineCaps.interpolation_variation line 79
Source documentation
A held convex interpolation costs no more variation than the two persistent endpoint trackers.
```
theorem interpolation_variation {a b A B c : ℝ} (hc : c ∈ Set.Icc (0:ℝ) 1) :
    |((1-c)*A+c*B)-((1-c)*a+c*b)| ≤ |A-a|+|B-b| := by
…
```

theorem OAI.UniformKServer.FineCaps.selected_variation line 92

Source documentation

Changing membership in the noncore set costs one bounded endpoint value; no fresh tracker is initialized.

theorem selected_variation (a b : Bool) {x y M : ℝ} (hx : |x| ≤ M)
    (hy : |y| ≤ M) :
    |(if b then y else 0)-(if a then x else 0)| ≤
      |y-x|+(if a=b then 0 else M) := by
…