PrefixLimit.lean`

GitHub source file

4 declarations, 0 contain sorry, 0 declared as axioms

def OAI.FiniteFactor.sourceBiasedPrefixMask line 13
Source documentation
At prefix n, use y in the first n source blocks and x in the tail.
```
def sourceBiasedPrefixMask (n : ℕ) (i : SourceCoordinate) : Bool := decide (i.1 < n)
```
Mentions: OAI.FiniteFactor.SourceCoordinate
theorem OAI.FiniteFactor.sourceBiasedPrefixPair_tendsto line 15
theorem OAI.FiniteFactor.sourceBiasedPrefix_weak line 27
Source documentation
The actual beta_n converge weakly to the actual full biased law nu_j.
```
theorem sourceBiasedPrefix_weak (j : ℕ) :
    Tendsto (fun n => sourceBiasedTorusMeasure j (sourceBiasedPrefixMask n)) atTop
      (𝓝 (sourceBiasedTorusMeasure j (fun _ => true))) := by
…
```
Mentions: OAI.FiniteFactor.sourceBiasedTorusMeasure, OAI.FiniteFactor.sourceBiasedPrefixMask
theorem OAI.FiniteFactor.sourceBiasedPrefix_uniformAC line 53
Source documentation
Uniform absolute continuity covers every prefix and both endpoint choices.
```
theorem sourceBiasedPrefix_uniformAC (j : ℕ) (b : Bool) (ε : ℝ≥0) (hε : 0 < ε) :
    ∃ δ : ℝ≥0∞, 0 < δ ∧ ∀ A, MeasurableSet A → sourceTorusHaar A < δ → ∀ n,
      ((sourceBiasedTorusMeasure j (sourceBiasedPrefixMask n) : Measure SourceSamplingTorus).map
        (sourceTorusEndpoint b)) A ≤ ε := by
…
```
Mentions: OAI.FiniteFactor.sourceTorusHaar, OAI.FiniteFactor.sourceBiasedTorusMeasure, OAI.FiniteFactor.sourceBiasedPrefixMask, OAI.FiniteFactor.SourceSamplingTorus, OAI.FiniteFactor.sourceTorusEndpoint