OAI/Combinatorics/EditApproximation/Refinement/PhysicalSeedMedian.lean

GitHub source file

9 declarations, 0 contain sorry, 0 declared as axioms

The seed update uses the actual integer ceilings, upper median and clamp. Copies share an entire table within each run and are independent between runs.

  1. def OAI.EditApproximation.finiteMedianSeed line 14
  2. theorem OAI.EditApproximation.ofFn_countP_filter line 17
  3. theorem OAI.EditApproximation.finiteMedianSeed_lower line 23
  4. theorem OAI.EditApproximation.finiteMedianSeed_upper line 32
  5. theorem OAI.EditApproximation.finiteMedianSeed_failure_bound line 45
  6. theorem OAI.EditApproximation.scaledCopy_rounding line 84

    Source documentation

    The integer multiplication and ceiling used before the median preserve both the deterministic lower approximation and a successful copy's upper bound.

    theorem scaledCopy_rounding (c a : ℕ) (ha : 0 < a) (value : ℚ)
    (hlower : (c : ℚ) / a ≤ value) (hupper : value ≤ 2 * c) :
    c ≤ ⌈(a : ℚ) * value⌉₊ ∧ ⌈(a : ℚ) * value⌉₊ ≤ 2 * a * c := by
…
  7. theorem OAI.EditApproximation.finite_positive_excess_tail line 98
  8. def OAI.EditApproximation.physicalScaledCopy line 117
  9. theorem OAI.EditApproximation.physicalScaledCopy_lower line 124