ContextWeightedEnumeration.lean`

1 declarations, 0 contain sorry, 0 declared as axioms

Physical observables in the literal conditional enumeration

theorem OAI.ContingencyTables.SmallContextEnumeration.eliminate_context_eq_weighted_sum line 22

Source documentation

Arbitrary physical observables keep exactly the same completion multiplicity in recursive elimination and in the literal child fibre.

theorem eliminate_context_eq_weighted_sum (small : I → J → Bool) (B : I → J → ℕ)
    (s : I×J) (hs : small s.1 s.2=true) (σ : I×J → ℕ) (U : ℕ)
    (hB : ∀ i j,small i j=true → B i j=U)
    (hσ : ∀ a : Earlier small s,σ a.val.val ≤ U) (k : Fin (U+1))
    {n : ℕ} (e : Fin n ≃ Later small s) (F : SmallProfile small → ℝ) :
    eliminate (widths (fun _ : Fin n => U))
      (fun p => F (assemble small s hs σ U e p)) (childProfile U k.val)=
      ∑ z : BalancedProfiles small B s σ k.val,F (naturalProfile z.val) := by
…