OAI/Combinatorics/ContingencyTables/Counting/CompanionWarmReturn.lean

GitHub source file

10 declarations, 0 contain sorry, 0 declared as axioms

The implemented capped return on a warm input law

The output kernel comes from the actual bounded Boolean word. Its error against the literal trace is bounded using the cap loss and the proved joint-path approximation, averaged under the incoming warm law.

  1. lemma OAI.ContingencyTables.CompanionWarmReturn.weighted_error line 24
  2. lemma OAI.ContingencyTables.CompanionWarmReturn.push_observation line 35
  3. theorem OAI.ContingencyTables.CompanionWarmReturn.distance_of_events line 41
  4. def OAI.ContingencyTables.CompanionWarmReturn.returnLaw line 65
  5. def OAI.ContingencyTables.CompanionWarmReturn.returnKernel line 72
  6. lemma OAI.ContingencyTables.CompanionWarmReturn.return_observation line 78
  7. theorem OAI.ContingencyTables.CompanionWarmReturn.warm_cap_loss line 88
  8. lemma OAI.ContingencyTables.CompanionWarmReturn.returnKernel_stochastic line 118
  9. theorem OAI.ContingencyTables.CompanionWarmReturn.weighted_return_event line 126
  10. theorem OAI.ContingencyTables.CompanionWarmReturn.warm_return_distance line 165

    Source documentation

    This is the law of the implemented Boolean return, compared to the literal trace on the same incoming warm distribution.

    theorem warm_return_distance (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