SecondLevels.lean`

4 declarations, 0 contain sorry, 0 declared as axioms

def OAI.FiniteFactor.samplingSecondLevelLeft line 12
Source documentation
The two closed intervals representing a positive superlevel of the second-oriented tested reciprocal. Endpoint changes are dealt with separately.
```
def samplingSecondLevelLeft (h α a c s r : ℝ) : Set ℝ :=
…
```
def OAI.FiniteFactor.samplingSecondLevelRight line 16

theorem OAI.FiniteFactor.sampling_reciprocal_level line 21

Source documentation

A reciprocal superlevel is the union of two endpoint intervals.

theorem sampling_reciprocal_level (h r z : ℝ) (hh : 0 < h) (hr : 0 < r)
    (hz : 0 < z) (hz1 : z < 1) :
    r ≤ 1/(h*samplingDistance z) ↔
      (z ≤ 1/2 ∧ z ≤ 1/(h*r)) ∨ (1/2 ≤ z ∧ 1-z ≤ 1/(h*r)) := by
…

Mentions: OAI.FiniteFactor.samplingDistance

theorem OAI.FiniteFactor.samplingTestedSecond_level_intervals line 52

Source documentation

Away from three possible jumps, the exact level indicator is the sum of two closed-interval indicators. No variation theorem is assumed.

theorem samplingTestedSecond_level_intervals (h α : ℝ) (G : Set ℝ) (a c s r t : ℝ)
    (hh : 0 < h) (hh1 : h < 1) (hα : 0 < α)
    (hs : s ∈ Set.Ico (0 : ℝ) 1) (ht : t ∈ Set.Ico (0 : ℝ) 1)
    (hr : 0 < r) (hsG : s ∈ G)
    (ht0 : t ≠ 0) (htL : t ≠ samplingSecondLength h s) (htmid : t ≠ s-1/2) :
    (if r ≤ samplingTestedSecondWeight h α (Set.Icc a c) G s t then (1 : ℝ) else 0) =
      (samplingSecondLevelLeft h α a c s r).indicator (fun _ => (1 : ℝ)) t +
      (samplingSecondLevelRight h α a c s r).indicator (fun _ => (1 : ℝ)) t := by
…

Mentions: OAI.FiniteFactor.samplingSecondLength, OAI.FiniteFactor.samplingTestedSecondWeight, OAI.FiniteFactor.samplingSecondLevelLeft, OAI.FiniteFactor.samplingSecondLevelRight