AlphaStability.lean`

11 declarations, 0 contain sorry, 0 declared as axioms

Companion §04: exact primitive input slopes on the entire simplex. The constants do not depend on the number of children. These estimates apply to the old flags after filtering, without requiring feasibility of that input.

theorem OAI.UniformKServer.AlphaStability.primitive_sub line 19

Source documentation

Linearity in the two raw inputs, with the improper endpoint justified by the same integrable density as the original primitive.

theorem primitive_sub {D : ℝ → ℝ} {base a scale S Q S' Q' : ℝ}
    (hb : base ∈ Icc (0:ℝ) 1) (ha : a ∈ Icc (0:ℝ) 1)
    (hI : IntervalIntegrable (fun x => (S-Q/x)/D x) volume 0 1)
    (hI' : IntervalIntegrable (fun x => (S'-Q'/x)/D x) volume 0 1) :
    primitive D base scale S Q a-primitive D base scale S' Q' a =
      primitive D base scale (S-S') (Q-Q') a := by
…

theorem OAI.UniformKServer.AlphaStability.regular_integrable line 33
theorem OAI.UniformKServer.AlphaStability.marked_integrable line 38
theorem OAI.UniformKServer.AlphaStability.regular_difference line 43
theorem OAI.UniformKServer.AlphaStability.marked_difference line 50
theorem OAI.UniformKServer.AlphaStability.sum_difference line 59

theorem OAI.UniformKServer.AlphaStability.regular_input line 64

Source documentation

Dimension-free whole-simplex input Lipschitz bound in an unmarked epoch.

theorem regular_input (h η a B B' : ι → ℝ) (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) :
    |(∑ i, primitive (regular (h i)) 0 scale (∑ r, B r) ((1+η i)*B i) (a i))-
      (∑ i, primitive (regular (h i)) 0 scale (∑ r, B' r) ((1+η i)*B' i) (a i))| ≤
      |scale| *(2+E)*(∑ i, |B i-B' i|) := by
…

def OAI.UniformKServer.AlphaStability.mixedPrimitive line 89

theorem OAI.UniformKServer.AlphaStability.marked_input line 96

Source documentation

The marked primitive retains a dimension-free input bound as u tends to zero. The estimate does not require input feasibility at the old state.

theorem marked_input [DecidableEq ι] (o : ι) (h η a B B' : ι → ℝ) (scale E u : ℝ)
    (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) :
    |(∑ i, mixedPrimitive o u h η B scale a i)-
      (∑ i, mixedPrimitive o u h η B' scale a i)| ≤
      |scale| * (11+4*E)*(∑ i, |B i-B' i|) := by
…

Mentions: OAI.UniformKServer.AlphaStability.mixedPrimitive

theorem OAI.UniformKServer.AlphaStability.regular_parameter line 151

Source documentation

Refreshing a regular size costs its prepared input, not the parent's total size. There is no summation over unchanged coordinates.

theorem regular_parameter {h h' a S B η η' E : ℝ} (hh : 1 ≤ h) (hh' : 1 ≤ h')
    (ha : a ∈ Icc (0:ℝ) 1) (hS : 0 ≤ S) (hB : 0 ≤ B)
    (hη : 0 ≤ η) (hη' : 0 ≤ η') (hE : η ≤ E) (hE' : η' ≤ E)
    (hprep : S*a ≤ (1+E)*B) (scale : ℝ) :
    |primitive (regular h) 0 scale S ((1+η)*B) a-
      primitive (regular h') 0 scale S ((1+η')*B) a| ≤
      4*|scale| * (1+E)*B := by
…

theorem OAI.UniformKServer.AlphaStability.marked_prepared_component line 173

Source documentation

Cancellation at the marked base point 1 converts a parameter refresh into a side-size charge. This bound stays uniform as u tends to zero.

theorem marked_prepared_component {u a S B η κ E : ℝ} (hu : 0 < u) (hu₁ : u ≤ 1)
    (ha : a ∈ Icc (0:ℝ) 1) (hS : 0 ≤ S) (hB : 0 ≤ B) (hBS : B ≤ S)
    (hη : 0 ≤ η) (hκ : η ≤ κ*u) (hprep : S*(1-a) ≤ (1+E)*(S-B)) (scale : ℝ) :
    |primitive (marked u) 1 scale S ((1+η)*B) a| ≤
      3*|scale| * ((2+E)*(S-B)+κ*u*S) := by
…