OAI/Combinatorics/ContingencyTables/Counting/CompanionCappedReturn.lean

GitHub source file

10 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.ContingencyTables.CompanionCappedReturn.returnDefault line 23
2. lemma OAI.ContingencyTables.CompanionCappedReturn.returnDefault_value line 26
3. theorem OAI.ContingencyTables.CompanionCappedReturn.returnDefault_expectation line 36

   Source documentation

   The missing cap mass is assigned to the starting state, exactly.

   theorem returnDefault_expectation (C : FiniteChain X) (B : X → Prop)
       (Q : KilledKernel (FiniteChain.Outside B))
       (hQ : ∀ x y,Q.Q x y=C.P x.val y.val)
       (phi : FiniteChain.Inside B → ℝ) (n : ℕ) (x : FiniteChain.Inside B) :
       C.pathExpectation (n+1) x.val (fun xs => phi (returnDefault B x xs))=
         (∑ y,C.cappedTrace B Q n x y*phi y)+
           phi x*(1-∑ y,C.cappedTrace B Q n x y) := by
   …

   Mentions: OAI.ContingencyTables.CompanionCappedReturn.returnDefault

4. theorem OAI.ContingencyTables.CompanionCappedReturn.returnDefault_error line 54

   Source documentation

   Bounded observations lose at most the exact omitted return mass.

   theorem returnDefault_error (C : FiniteChain X) (B : X → Prop)
       (Q : KilledKernel (FiniteChain.Outside B))
       (hQ : ∀ x y,Q.Q x y=C.P x.val y.val)
       (phi : FiniteChain.Inside B → ℝ) (hphi : ∀ y,0≤phi y ∧ phi y≤1)
       (n : ℕ) (x : FiniteChain.Inside B) :
       |C.pathExpectation (n+1) x.val (fun xs => phi (returnDefault B x xs))-
         (∑ y,C.traceMatrix B Q x y*phi y)|≤
           1-∑ y,C.cappedTrace B Q n x y := by
   …

   Mentions: OAI.ContingencyTables.CompanionCappedReturn.returnDefault

5. theorem OAI.ContingencyTables.CompanionCappedReturn.returnDefault_event_upper line 89
6. theorem OAI.ContingencyTables.CompanionCappedReturn.warm_returnDefault_error line 103

   Source documentation

   The cap error is small on a warm input law even when a pointwise return-time bound would be too expensive.

   theorem warm_returnDefault_error (C : FiniteChain X) (B : X → Prop)
       [Nonempty (FiniteChain.Inside B)]
       (Q : KilledKernel (FiniteChain.Outside B))
       (hQ : ∀ x y,Q.Q x y=C.P x.val y.val)
       (phi : FiniteChain.Inside B → ℝ) (hphi : ∀ y,0≤phi y ∧ phi y≤1)
       (n : ℕ) (hn : 0<n) (nu : FiniteChain.Inside B → ℝ) (hnu : ∀ x,0≤nu x)
       (U : ℝ) (hwarm : ∀ x,nu x≤U*(C.traceChain B Q hQ).π x) :
       (∑ x,nu x*|C.pathExpectation (n+1) x.val (fun xs => phi (returnDefault B x xs))-
         (∑ y,C.traceMatrix B Q x y*phi y)|)≤U/C.insideMass B/(n:ℝ) := by
   …

   Mentions: OAI.ContingencyTables.CompanionCappedReturn.returnDefault

7. def OAI.ContingencyTables.CompanionCappedReturn.returnWordDefault line 125

   Source documentation

   A concrete total draw: a missing capped return keeps the input.

   def returnWordDefault (A : Instance I J) (C K j k n : ℕ)
       (hK : 1≤K) (hW : 100*A.d*K≤A.W) (xi : ℚ)
       (v : Grid (I := Fin (dimension A)) K) (w : Pair A → Pair A → ℚ)
   …

8. theorem OAI.ContingencyTables.CompanionCappedReturn.returnWordDefault_to_path line 132
9. theorem OAI.ContingencyTables.CompanionCappedReturn.target_returnDefault_bound line 149
10. theorem OAI.ContingencyTables.CompanionCappedReturn.returnWordDefault_event line 164

    Source documentation

    The implemented total return step is compared to the exact trace, with its cap loss left explicit for subsequent warm-law averaging.

    theorem returnWordDefault_event (A : Instance I J) (C : ℕ) (hC : 0<C) (K j k n : ℕ)
        (hK : 1≤K) (hW : 100*A.d*K≤A.W) (hB : (K:ℝ)=binWidth A C)
        (hj : j≤rationalHeight A C) (xi : ℚ) (hx0 : 0<xi) (hx1 : xi≤1/4)
        (hPL : PublishedInputs.FiniteBoxPrekopaLeindler (dimension A))
        (hCheeger : PublishedInputs.FiniteCheeger (Grid (I := Fin (dimension A)) K))
    …

    Mentions: OAI.ContingencyTables.PublishedInputs.FiniteBoxPrekopaLeindler, OAI.ContingencyTables.PublishedInputs.FiniteCheeger