FloorSupport.lean`

4 declarations, 0 contain sorry, 0 declared as axioms

theorem OAI.FiniteFactor.unitInterval_floor_exception line 15
Source documentation
A uniform coordinate crosses the cut under translation by a with probability at most |a|, valid for either sign and any size of translation.
```
theorem unitInterval_floor_exception (a : ℝ) :
    unitIntervalMeasure {t : ℝ | Int.floor (t+a) ≠ 0} ≤ ENNReal.ofReal |a| := by
…
```
Mentions: OAI.FiniteFactor.unitIntervalMeasure
def OAI.FiniteFactor.coordinateFloor line 41
Source documentation
Source coordinate floors. Integer times include both directions.
Also declared: ComparatorChallenges/ProductBrown.lean:299 (same declaration text).
```
def coordinateFloor {ι : Type*} (θ : ι → ℝ) (k : ℤ) (x : ι → ℝ) (i : ι) : ℤ :=
…
```
def OAI.FiniteFactor.finiteFloorSupport line 44
theorem OAI.FiniteFactor.ae_finiteFloorSupport line 49
Source documentation
Borel--Cantelli proves that every integer-time floor sum has only finitely many nonzero terms, simultaneously. This is the source's conull domain for F_k.
```
theorem ae_finiteFloorSupport {ι : Type*} [Countable ι]
    (θ : ι → ℝ) (hθ : Summable (fun i => |θ i|)) :
    ∀ᵐ x ∂Measure.infinitePi (fun _ : ι => unitIntervalMeasure), finiteFloorSupport θ x := by
…
```
Mentions: OAI.FiniteFactor.unitIntervalMeasure, OAI.FiniteFactor.finiteFloorSupport