OAI/Combinatorics/ContingencyTables/Sampling/SmallProfileEncoding.lean

GitHub source file

5 declarations, 0 contain sorry, 0 declared as axioms

1. abbrev OAI.ContingencyTables.SmallGraphProfiles.VarianceEncoding line 18
2. def OAI.ContingencyTables.SmallGraphProfiles.encodeProfile line 22
3. lemma OAI.ContingencyTables.SmallGraphProfiles.encodeProfile_injective line 30
4. lemma OAI.ContingencyTables.SmallGraphProfiles.outside_encoding_weight_zero line 63

   Source documentation

   Every omitted physical profile has zero completion weight.

   lemma outside_encoding_weight_zero (small : I → J → Bool) (B : I → J → ℕ)
       (r : I → ℕ) (c : J → ℕ) (L U : ℕ)
       (hB : ∀ i j,small i j=true → B i j=U) (p : Profiles small B)
       (hp : p ∉ Set.range (encodeProfile small B r c L U hB)) :
       hardMarginal small B r c L (naturalProfile p.val)=0 := by
   …

   Mentions: OAI.ContingencyTables.SmallGraphProfiles.Profiles, OAI.ContingencyTables.SmallGraphProfiles.encodeProfile

5. theorem OAI.ContingencyTables.SmallGraphProfiles.encoding_variance_eq line 81

   Source documentation

   The completed graph variance proof concerns the literal bounded physical profiles; the auxiliary encoding drops only zero-mass defects.

   theorem encoding_variance_eq (small : I → J → Bool) (B : I → J → ℕ)
       (r : I → ℕ) (c : J → ℕ) (L U : ℕ)
       (hB : ∀ i j,small i j=true → B i j=U) (H : SmallProfile small → ℝ) :
       variance
         (Sum.elim (wordWeight small B r c L U)
           (fun z : PositiveDefects small B r c L => hardMarginal small B r c L (naturalProfile z.val)))
         (Sum.elim (wordObservable small U H) (fun z => H (naturalProfile z.val)))=
         variance (fun z : Profiles small B => hardMarginal small B r c L (naturalProfile z.val))
           (fun z => H (naturalProfile z.val)) := by
   …

   Mentions: OAI.ContingencyTables.SmallGraphProfiles.PositiveDefects, OAI.ContingencyTables.SmallGraphProfiles.Profiles