OAI/Combinatorics/ContingencyTables/Sampling/ExactIntegerOnline.lean

GitHub source file

14 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.ContingencyTables.ExactIntegerOnline.trialBits line 16
2. def OAI.ContingencyTables.ExactIntegerOnline.trialBitsRealizer line 18
3. lemma OAI.ContingencyTables.ExactIntegerOnline.polynomial_trialBits line 21
4. def OAI.ContingencyTables.ExactIntegerOnline.trial line 24
5. def OAI.ContingencyTables.ExactIntegerOnline.trialRealizer line 27
6. lemma OAI.ContingencyTables.ExactIntegerOnline.trialBits_le_weight line 30
7. theorem OAI.ContingencyTables.ExactIntegerOnline.polynomial_trial line 34
8. lemma OAI.ContingencyTables.ExactIntegerOnline.map_expectation line 44
9. lemma OAI.ContingencyTables.ExactIntegerOnline.average_expectation line 53
10. theorem OAI.ContingencyTables.ExactIntegerOnline.trial_mean line 63

    Source documentation

    The compiled variable-length trial has precisely the integer-grid probabilities, with the unused suffix of the binary range returning none.

    theorem trial_mean {r : ℕ} (w : Fin r → ℕ) (h : 0<totalWeight w) (g : Option ℕ → ℚ) :
        (trial (List.ofFn w)).mean g=
          ∑ y : Option (Fin r),
            (trialLaw w h (Nat.le_pow_clog (by decide : 1<2) (totalWeight w))).mass y*
              g (y.map Fin.val) := by
    …

    Mentions: OAI.ContingencyTables.ExactIntegerOnline.trial

11. lemma OAI.ContingencyTables.ExactIntegerOnline.retry_mass_succ line 86
12. lemma OAI.ContingencyTables.ExactIntegerOnline.prefix_mean line 96

    Source documentation

    Mean preservation for every finite prefix allows the online loop to reuse the already proved exact rational retry law.

    lemma prefix_mean {A B C : Type} [Fintype B] [DecidableEq B]
        (f : A → Experiment (Option C)) (a : A) (p : RationalLaw (Option B)) (e : B → C)
        (hf : ∀ g : Option C → ℚ,(f a).mean g=∑ y,p.mass y*g (y.map e))
        (N : ℕ) (g : Option C → ℚ) :
        (OnlineIntegerRetry.prefixExperiment (f := f) a N).mean g=
    …

    Mentions: OAI.ContingencyTables.OnlineIntegerRetry.prefixExperiment

13. theorem OAI.ContingencyTables.ExactIntegerOnline.integer_prefix_mean line 114
14. theorem OAI.ContingencyTables.ExactIntegerOnline.integer_prefix_failure line 121