OAI/Combinatorics/ContingencyTables/Counting/CompanionObservationQueriesLaw.lean

GitHub source file

9 declarations, 0 contain sorry, 0 declared as axioms

1. lemma OAI.ContingencyTables.CompanionObservationQueriesProgram.queryPair_ofFn line 17
2. lemma OAI.ContingencyTables.CompanionObservationQueriesProgram.output_ofFn line 28
3. def OAI.ContingencyTables.CompanionObservationQueriesProgram.values line 44
4. theorem OAI.ContingencyTables.CompanionObservationQueriesProgram.sameLaw line 48

   Source documentation

   Each trajectory position gets its own independent current and next query.

   theorem sameLaw {N : ℕ} {U V : Type*} [Fintype U] [Fintype V]
       (cs : Config×Config) (codes : Fin N→List ℕ) (f : Fin N→U→ℚ) (g : Fin N→V→ℚ)
       (hf : ∀ i,SameLaw (fun bits : Fin (queryWidth cs.1)→Bool =>
         TreeFraction.val (RootedLabelWeightProgram.output (cs.1,(codes i,List.ofFn bits)))) (f i))
       (hg : ∀ i,SameLaw (fun bits : Fin (queryWidth cs.2)→Bool =>
         TreeFraction.val (RootedLabelWeightProgram.output (cs.2,(codes i,List.ofFn bits)))) (g i)) :
       SameLaw (fun bits : Fin (N*blockWidth cs)→Bool =>
         values (output (cs,(List.ofFn codes,List.ofFn bits))))
         (fun bits : Fin N→U×V => List.ofFn (fun i => (f i (bits i).1,g i (bits i).2))) := by
   …

   Mentions: OAI.ContingencyTables.CompanionObservationQueriesProgram.Config, OAI.ContingencyTables.CompanionObservationQueriesProgram.queryWidth, OAI.ContingencyTables.RootedLabelWeightProgram.output, OAI.ContingencyTables.CompanionObservationQueriesProgram.blockWidth, OAI.ContingencyTables.CompanionObservationQueriesProgram.values, OAI.ContingencyTables.CompanionObservationQueriesProgram.output

5. lemma OAI.ContingencyTables.CompanionObservationQueriesProgram.queryWidth_config line 78
6. lemma OAI.ContingencyTables.CompanionObservationQueriesProgram.sameLaw_query line 86
7. def OAI.ContingencyTables.CompanionObservationQueriesProgram.phaseConfigs line 110

   Source documentation

   The two physical configurations used for observing one phase.

   def phaseConfigs (A : Instance (Fin m) (Fin n)) (C K j : ℕ) (xi : ℚ)
       (z : View A→ℕ) (v : Grid (I := Fin (RootedCatalogGrid.freeCount A)) K)
   …

   Mentions: OAI.ContingencyTables.RootedCatalogGrid.freeCount

8. lemma OAI.ContingencyTables.CompanionObservationQueriesProgram.blockWidth_phaseConfigs line 116
9. theorem OAI.ContingencyTables.CompanionObservationQueriesProgram.sameLaw_phase line 125

   Source documentation

   All state observations use the exact selected-root oracle law, independently.

   theorem sameLaw_phase (A : Instance (Fin m) (Fin n)) (C K j N : ℕ)
       (hC : 0 < C) (hj : j+1 ≤ rationalHeight A C) (hK : 1 ≤ K)
       (hW : 100*A.d*K ≤ A.W) (hB : (K:ℝ)=binWidth A C)
       (xi : ℚ) (hxi : 0 < xi) (z : View A→ℕ)
       (v : Grid (I := Fin (RootedCatalogGrid.freeCount A)) K)
   …

   Mentions: OAI.ContingencyTables.RootedCatalogGrid.freeCount