OAI/Analysis/FiniteFactor/FiniteSingleTag.lean

GitHub source file

3 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.FiniteFactor.singleTagCylinder line 13
2. theorem OAI.FiniteFactor.singleTagCylinder_measurable line 16
3. theorem OAI.FiniteFactor.finite_single_tag_lower line 35

   Source documentation

   Independent finite coordinates with one distinguished tag. The other coordinates are explicitly nontagged, so these cylinders are disjoint.

   theorem finite_single_tag_lower (μ : ι → Measure X) [∀ q, IsProbabilityMeasure (μ q)]
       (F : Finset ι) (T A : ι → Set X)
       (hT : ∀ q ∈ F, MeasurableSet (T q)) (hA : ∀ q ∈ F, MeasurableSet (A q))
       (hdisj : ∀ q ∈ F, Disjoint (T q) (A q)) (t a : ℝ≥0∞)
       (hTm : ∀ q ∈ F, t ≤ μ q (T q)) (hAm : ∀ q ∈ F, a ≤ μ q (A q)) :
       (F.card : ℝ≥0∞)*t*a^(F.card-1) ≤
         (Measure.infinitePi μ) (⋃ i ∈ F, singleTagCylinder F T A i) := by
   …

   Mentions: OAI.FiniteFactor.singleTagCylinder