OAI/Combinatorics/ContingencyTables/Counting/CompanionOracleChain.lean

GitHub source file

8 declarations, 0 contain sorry, 0 declared as axioms

1. lemma OAI.ContingencyTables.CompanionOracleDensity.proposal_bounds line 20

   Source documentation

   The dyadic proposal is valid already at d = 1, including the zero-dimensional grid.

   lemma proposal_bounds (d : ℕ) (hd : 1 ≤ d) :
       0 < binProposal d ∧ 1/(16*(d:ℝ)) ≤ binProposal d ∧
         binProposal d ≤ 1/(8*(d:ℝ)) := by
   …

2. lemma OAI.ContingencyTables.CompanionOracleDensity.proposal_degree line 40
3. def OAI.ContingencyTables.CompanionOracleDensity.gridWeight line 51
4. def OAI.ContingencyTables.CompanionOracleDensity.oracleChain line 54
5. lemma OAI.ContingencyTables.CompanionOracleDensity.oracleChain_pi line 63
6. def OAI.ContingencyTables.CompanionOracleDensity.cutConstant line 68
7. lemma OAI.ContingencyTables.CompanionOracleDensity.corner_injective line 70
8. theorem OAI.ContingencyTables.CompanionOracleDensity.oracleChain_poincare line 78

   Source documentation

   All geometric cut obligations are discharged for the literal forest penalty. Only finite-box PL and finite-chain Cheeger remain conditional.

   theorem oracleChain_poincare (A : Instance I J) (C a : ℝ) (hC : 0 < C)
       (ha : 0 ≤ a) (haH : a ≤ height A C) (z : View A → ℕ)
       {K : ℕ} (hK : 1 ≤ K)
       (hPL : PublishedInputs.FiniteBoxPrekopaLeindler (dimension A))
       (hCheeger : PublishedInputs.FiniteCheeger (Grid (I := Fin (dimension A)) K)) :
   …

   Mentions: OAI.ContingencyTables.CompanionOracleDensity.height, OAI.ContingencyTables.PublishedInputs.FiniteBoxPrekopaLeindler, OAI.ContingencyTables.CompanionOracleDensity.dimension, OAI.ContingencyTables.PublishedInputs.FiniteCheeger