DiagonalLimit.lean`

5 declarations, 0 contain sorry, 0 declared as axioms

theorem OAI.FiniteFactor.sourceSamplingWidth_tendsto line 11
theorem OAI.FiniteFactor.sourceSamplingCutoff_tendsto line 19
theorem OAI.FiniteFactor.sampling_interval_small_displacement line 24

theorem OAI.FiniteFactor.samplingTestedFirstDensity_diagonal_exact line 45

Source documentation

Away from the interval endpoints, a sufficiently short retained diagonal step has exactly the same interval test as its starting coordinate.

theorem samplingTestedFirstDensity_diagonal_exact (h α s a c : ℝ) (E : Set ℝ)
    (hh : 0 < h) (hh1 : h < 1) (hα : 0 < α)
    (hs : s ∈ Set.Ico (0 : ℝ) 1) (hcut : α ≤ samplingDistance s)
    (ha : s ≠ a) (hc : s ≠ c) (hha : h < |s-a|) (hhc : h < |s-c|) :
    samplingTestedFirstDensity false h α E (Set.Icc a c) s =
      if s ∈ E ∧ s ∈ Set.Icc a c then 1 else 0 := by
…

Mentions: OAI.FiniteFactor.samplingDistance, OAI.FiniteFactor.samplingTestedFirstDensity

theorem OAI.FiniteFactor.sourceSampling_diagonal_eventually line 77
Source documentation
At each interior starting point away from the two tested endpoints, the actual diagonal density eventually equals the uniform diagonal test.
```
theorem sourceSampling_diagonal_eventually (s a c : ℝ) (E : Set ℝ)
    (hs : s ∈ Set.Ioo (0 : ℝ) 1) (ha : s ≠ a) (hc : s ≠ c) :
    ∀ᶠ stage in atTop,
      samplingTestedFirstDensity false (sourceSamplingWidth stage) (sourceSamplingCutoff stage)
        E (Set.Icc a c) s = if s ∈ E ∧ s ∈ Set.Icc a c then 1 else 0 := by
…
```
Mentions: OAI.FiniteFactor.samplingTestedFirstDensity, OAI.FiniteFactor.sourceSamplingWidth, OAI.FiniteFactor.sourceSamplingCutoff