ReferenceOrdered.lean`

GitHub source file

4 declarations, 0 contain sorry, 0 declared as axioms

theorem OAI.FiniteFactor.sourceSamplingPairHaar_coordinate_ne line 11
Source documentation
The independent Haar pair has no equality boundary at any coordinate.
```
theorem sourceSamplingPairHaar_coordinate_ne :
    ∀ᵐ z ∂sourceSamplingPairHaar, ∀ i, (z i).1 ≠ (z i).2 := by
…
```
Mentions: OAI.FiniteFactor.sourceSamplingPairHaar
theorem OAI.FiniteFactor.sourceSamplingLimit_order_event line 28
Source documentation
Strict and non-strict order coincide for the replacement coordinates.
```
theorem sourceSamplingLimit_order_event (I : Finset SourceCoordinate) :
    (sourceSamplingLimitMap I ⁻¹' sourceSamplingOrdered) =ᵐ[sourceSamplingPairHaar]
      sourceSamplingTriangleSet I := by
…
```
Mentions: OAI.FiniteFactor.SourceCoordinate, OAI.FiniteFactor.sourceSamplingLimitMap, OAI.FiniteFactor.sourceSamplingOrdered, OAI.FiniteFactor.sourceSamplingPairHaar, OAI.FiniteFactor.sourceSamplingTriangleSet
theorem OAI.FiniteFactor.sourceResampling_ordered_restriction line 43
theorem OAI.FiniteFactor.sourceFiniteReference_ordered_mixture line 52
Source documentation
Exact finite-prefix reference mixture after imposing global order.
```
theorem sourceFiniteReference_ordered_mixture (F : Finset SourceCoordinate) :
    (sourceSamplingHaar ⊗ₘ sourceFiniteReferenceKernel F).restrict sourceSamplingOrdered =
      ((2 : ℝ≥0∞)⁻¹)^F.card • ∑ I ∈ F.powerset, sourceSamplingLambda I := by
…
```
Mentions: OAI.FiniteFactor.SourceCoordinate, OAI.FiniteFactor.sourceSamplingHaar, OAI.FiniteFactor.sourceFiniteReferenceKernel, OAI.FiniteFactor.sourceSamplingOrdered, OAI.FiniteFactor.sourceSamplingLambda