OAI/Combinatorics/UniformKServer/ProportionParameters.lean

GitHub source file

17 declarations, 0 contain sorry, 0 declared as axioms

Exact compact alpha update uniformly across unmarked, marked, and automatic singleton stars. The fixed numerical envelopes are justified by the actual held epoch geometry in EpochParameters; they are not competitive assumptions.

  1. inductive OAI.UniformKServer.ProportionParameters.Kind line 20
  2. structure OAI.UniformKServer.ProportionParameters.Parameters line 25
  3. def OAI.UniformKServer.ProportionParameters.eta line 32
  4. def OAI.UniformKServer.ProportionParameters.valid line 34
  5. def OAI.UniformKServer.ProportionParameters.component line 44
  6. def OAI.UniformKServer.ProportionParameters.potential line 50
  7. theorem OAI.UniformKServer.ProportionParameters.C_pos line 52
  8. theorem OAI.UniformKServer.ProportionParameters.h_nonneg line 55
  9. theorem OAI.UniformKServer.ProportionParameters.eta_nonneg line 66
  10. theorem OAI.UniformKServer.ProportionParameters.singleton_sum line 69
  11. theorem OAI.UniformKServer.ProportionParameters.update line 76
  12. theorem OAI.UniformKServer.ProportionParameters.primitive_zero line 105
  13. theorem OAI.UniformKServer.ProportionParameters.component_zero line 109
  14. theorem OAI.UniformKServer.ProportionParameters.potential_zero line 114
  15. theorem OAI.UniformKServer.ProportionParameters.component_mixed line 117
  16. theorem OAI.UniformKServer.ProportionParameters.input_bound line 128

    Source documentation

    The same bound works on the entire old compact simplex, even when the filtered core input violates current coordinate feasibility.

    theorem input_bound {p : Parameters ι} (hp : valid p) (B B' a : ι → ℝ)
    (ha : simplex a) :
    |potential p B a-potential p B' a| ≤
      15*(p.C*p.ell)*(∑ i, |B i-B' i|) := by
…

    Mentions: OAI.UniformKServer.ProportionParameters.Parameters, OAI.UniformKServer.ProportionParameters.valid, OAI.UniformKServer.ProportionParameters.potential

  17. theorem OAI.UniformKServer.ProportionParameters.potential_bound line 164