SideStability.lean`

9 declarations, 0 contain sorry, 0 declared as axioms

The exact side primitives have dimension-free input slopes, uniformly in the number of sides and their sizes. Companion §04 side-potential-bounds.

def OAI.UniformKServer.SideStability.dCoefficient line 16
Source documentation
The coefficient of the parent input D, after analytic integration.
```
def dCoefficient (θ z s : ℝ) : ℝ :=
…
```
def OAI.UniformKServer.SideStability.bCoefficient line 19
Source documentation
The negative coefficient of the side input B.
```
def bCoefficient (b θ z s : ℝ) : ℝ :=
…
```
theorem OAI.UniformKServer.SideStability.coordinate_affine line 22
theorem OAI.UniformKServer.SideStability.logarithm_bounds line 27
theorem OAI.UniformKServer.SideStability.dCoefficient_bounds line 36
theorem OAI.UniformKServer.SideStability.bCoefficient_bounds line 47

theorem OAI.UniformKServer.SideStability.coordinate_bound line 59

Source documentation

A scalar slope bound; B,D may have either sign, as needed for a raw filtered-input difference.

theorem coordinate_bound {b θ z s T J Q : ℝ} (hb : 0 ≤ b) (hθ : 0 < θ)
    (hz : 0 < z) (hs : 0 ≤ s) (hT : 1/θ ≤ T)
    (hJ : Real.log (1+s/z)/θ ≤ J) (hQ : b+θ/2 ≤ Q) (C B D : ℝ) :
    |coordinate b θ z C B D s| ≤ |C| * (|D| *(T+1/2)*s+|B| *Q*J) := by
…

theorem OAI.UniformKServer.SideStability.coordinate_sub line 76

theorem OAI.UniformKServer.SideStability.input_bound line 86

Source documentation

Summing the exact coefficients costs the side-domain bound, not its cardinality. This applies even when the raw filtered inputs are infeasible.

theorem input_bound (b C D D' T J Q W : ℝ) (θ z B B' w : ι → ℝ)
    (hb : 0 ≤ b) (hθ : ∀ i, 0 < θ i) (hz : ∀ i, 0 < z i)
    (hw : domain W w) (hT : ∀ i, 1/θ i ≤ T)
    (hJ : ∀ i, Real.log (1+w i/z i)/θ i ≤ J)
    (hQ : ∀ i, b+θ i/2 ≤ Q) (hT' : 0 ≤ T+1/2) :
    |potential b C D θ z B w-potential b C D' θ z B' w| ≤
      |C| * (|D-D'| *(T+1/2)*W+Q*J*(∑ i, |B i-B' i|)) := by
…