OAI/Analysis/FiniteFactor/Coupling/Order.lean

GitHub source file

6 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.FiniteFactor.CouplingParameters.orderedPairs line 12
2. theorem OAI.FiniteFactor.CouplingParameters.orderedPairs_measurable line 14
3. theorem OAI.FiniteFactor.CouplingParameters.componentPair_ordered line 17
4. theorem OAI.FiniteFactor.CouplingParameters.coupling_ordered line 38
5. theorem OAI.FiniteFactor.CouplingParameters.labelledCoupling_ordered line 44
6. theorem OAI.FiniteFactor.CouplingParameters.productCoupling_ordered line 50

   Source documentation

   All infinitely many coordinates are ordered under the actual augmented law.

   theorem productCoupling_ordered (p : ℕ → CouplingParameters) :
       productCoupling p {ω | ∀ i, (ω i).2.1 ≤ (ω i).2.2} = 1 := by
   …

   Mentions: OAI.FiniteFactor.CouplingParameters, OAI.FiniteFactor.CouplingParameters.productCoupling