OAI/Combinatorics/EditApproximation/Probability/RejectionRuntimeLaw.lean

GitHub source file

11 declarations, 0 contain sorry, 0 declared as axioms

A probability law for terminating fair-word rejection executions. It records the failed trial count and accepted integer, identifies their joint masses with literal finite fair-word traces, and charges all trials.

  1. theorem OAI.EditApproximation.rejectionSuccessParameter_ne_zero line 18
  2. theorem OAI.EditApproximation.rejectionSuccessParameter_complement line 27
  3. def OAI.EditApproximation.rejectionExecutionLaw line 34
  4. instance OAI.EditApproximation.rejectionExecutionLaw_probability line 39
  5. theorem OAI.EditApproximation.rejectionExecutionLaw_output line 47

    Source documentation

    The accepted value has exactly the uniform law, independently of the number of failed trials.

    theorem rejectionExecutionLaw_output (N R : ℕ) [NeZero N]
    (hN : 0 < N) (hNR : N ≤ R) :
    (rejectionExecutionLaw N R hN hNR).map Prod.snd =
      (PMF.uniformOfFintype (Fin N)).toMeasure := by
…

    Mentions: OAI.EditApproximation.rejectionExecutionLaw

  6. theorem OAI.EditApproximation.rejectionExecutionLaw_atom line 55

    Source documentation

    Each execution atom has the probability of the corresponding literal finite first-success trace event.

    theorem rejectionExecutionLaw_atom (N R : ℕ) [NeZero N]
    (hN : 0 < N) (hNR : N ≤ R) (failures : ℕ) (accepted : Fin N) :
    (rejectionExecutionLaw N R hN hNR).real {(failures, accepted)} =
      ((R - N : ℕ) : ℝ) ^ failures / ((R : ℝ) ^ failures * R) := by
…

    Mentions: OAI.EditApproximation.rejectionExecutionLaw

  7. theorem OAI.EditApproximation.rejectionExecutionLaw_literal_trace line 70
  8. theorem OAI.EditApproximation.rejection_trial_moment line 80
  9. theorem OAI.EditApproximation.rejection_trials_integrable line 95
  10. theorem OAI.EditApproximation.rejection_fair_word_trial_moment line 110

    Source documentation

    All failed trials are included in this strict factor-two bound.

    theorem rejection_fair_word_trial_moment (N : ℕ) (hN : 0 < N) :
    (∫ failures : ℕ, ((failures : ℝ) + 1)
      ∂geometricMeasure (rejectionSuccessParameter N (2 ^ rejectionBitCount N)
        hN (rejectionWord_range N hN).1)) < 2 := by
…

    Mentions: OAI.EditApproximation.rejectionSuccessParameter, OAI.EditApproximation.rejectionBitCount, OAI.EditApproximation.rejectionWord_range

  11. theorem OAI.EditApproximation.rejection_consumed_bits_moment line 119

    Source documentation

    Exact expected number of consumed fair bits, including failed words.

    theorem rejection_consumed_bits_moment (N : ℕ) (hN : 0 < N) :
    (∫ failures : ℕ, (((failures : ℝ) + 1) * rejectionBitCount N)
      ∂geometricMeasure (rejectionSuccessParameter N (2 ^ rejectionBitCount N)
        hN (rejectionWord_range N hN).1)) ≤ 2 * rejectionBitCount N := by
…

    Mentions: OAI.EditApproximation.rejectionBitCount, OAI.EditApproximation.rejectionSuccessParameter, OAI.EditApproximation.rejectionWord_range