OAI/Analysis/FiniteFactor/BiasedPairs/Conull.lean

GitHub source file

4 declarations, 0 contain sorry, 0 declared as axioms

1. theorem OAI.FiniteFactor.sourceBiasedEndpoint_cube line 11
2. theorem OAI.FiniteFactor.sourceBiasedLaw_ordered line 20
3. theorem OAI.FiniteFactor.sourceBiasedTorusMeasure_ordered line 35

   Source documentation

   Every mixed law, including nu_j, is carried by the actual ordered representatives.

   theorem sourceBiasedTorusMeasure_ordered (j : ℕ) (r : SourceCoordinate → Bool) :
       ∀ᵐ z ∂(sourceBiasedTorusMeasure j r : Measure SourceSamplingTorus),
         ∀ i, sourceTorusRepresentative z.1 i ≤ sourceTorusRepresentative z.2 i := by
   …

   Mentions: OAI.FiniteFactor.SourceCoordinate, OAI.FiniteFactor.sourceBiasedTorusMeasure, OAI.FiniteFactor.SourceSamplingTorus, OAI.FiniteFactor.sourceTorusRepresentative

4. theorem OAI.FiniteFactor.sourceBiasedTorusMeasure_endpoints_conull line 59

   Source documentation

   The same Borel conull set works for both endpoints of every actual biased or mixed-prefix coupling; there is no new null-set choice for each identity.

   theorem sourceBiasedTorusMeasure_endpoints_conull (j : ℕ) (r : SourceCoordinate → Bool)
       (Q : Set SourceTorus) (hQ : ∀ᵐ z ∂sourceTorusHaar, z ∈ Q) :
       ∀ᵐ z ∂(sourceBiasedTorusMeasure j r : Measure SourceSamplingTorus), z.1 ∈ Q ∧ z.2 ∈ Q :=
   …

   Mentions: OAI.FiniteFactor.SourceCoordinate, OAI.FiniteFactor.SourceTorus, OAI.FiniteFactor.sourceTorusHaar, OAI.FiniteFactor.sourceBiasedTorusMeasure, OAI.FiniteFactor.SourceSamplingTorus