OAI/Combinatorics/ContingencyTables/Sampling/ExactMatrixLimits.lean

GitHub source file

2 declarations, 0 contain sorry, 0 declared as axioms

Limiting output law of the executed matrix rejection loop

  1. lemma OAI.ContingencyTables.ExactMatrixTrial.prefix_mass line 13
  2. theorem OAI.ContingencyTables.ExactMatrixTrial.prefix_limit line 26

    Source documentation

    The integer rejection loop tends to the exact weighted pushforward, including repeated matrix codes in a candidate list.

    theorem prefix_limit {K : ℕ} (candidates : Lookup) (w : Fin K → ℕ)
    (hw : 0<totalWeight w) (X : MatrixCode) :
    Filter.Tendsto (fun N =>
      ((OnlineIntegerRetry.prefixExperiment (f := trial) (candidates,List.ofFn w) N).mean
…

    Mentions: OAI.ContingencyTables.ExactMatrixTrial.Lookup, OAI.ContingencyTables.OnlineIntegerRetry.prefixExperiment, OAI.ContingencyTables.ExactMatrixTrial.trial