OAI/Analysis/FiniteFactor/CompactZeroTransfer.lean

GitHub source file

2 declarations, 0 contain sorry, 0 declared as axioms

1. theorem OAI.FiniteFactor.finiteMeasure_ae_of_compact_approximation line 12

   Source documentation

   Compact subsets carrying uniformly almost all approximating mass carry all limiting mass as their uniform losses tend to zero.

   theorem finiteMeasure_ae_of_compact_approximation {X : Type*}
       [MeasurableSpace X] [TopologicalSpace X] [T2Space X]
       [OpensMeasurableSpace X] [HasOuterApproxClosed X]
       (μ : ℕ → FiniteMeasure X) (ν : FiniteMeasure X)
       (hlim : Tendsto μ atTop (𝓝 ν)) (Z : Set X) (hZ : MeasurableSet Z)
       (hcompact : ∀ ε : ℝ≥0, 0 < ε → ∃ K, IsCompact K ∧ K ⊆ Z ∧
         ∀ n, (μ n : Measure X) Kᶜ ≤ ε) :
       ∀ᵐ x ∂(ν : Measure X), x ∈ Z := by
   …

2. theorem OAI.FiniteFactor.measure_pair_compact_loss line 43

   Source documentation

   The loss outside a product compact set is bounded by its two marginal losses. The identity set itself may only be Borel.

   theorem measure_pair_compact_loss {X : Type*} [MeasurableSpace X]
       (μ : Measure (X × X)) (Q : Set X) (hQ : MeasurableSet Q)
       (Z : Set (X × X)) (hZ : ∀ᵐ z ∂μ, z ∈ Z) :
       μ ((Q ×ˢ Q) ∩ Z)ᶜ ≤ (μ.map Prod.fst) Qᶜ + (μ.map Prod.snd) Qᶜ := by
   …