FirstInterval.lean`

6 declarations, 0 contain sorry, 0 declared as axioms

def OAI.FiniteFactor.samplingFirstLength line 10
def OAI.FiniteFactor.samplingFirstHeight line 13
theorem OAI.FiniteFactor.samplingWeight_first_interval line 17
Source documentation
The first-oriented weight is exactly a constant times one open interval.
```
theorem samplingWeight_first_interval (b : Bool) (h α s t : ℝ) :
    samplingWeight b h α s t =
      (Set.Ioo 0 (samplingFirstLength b h s)).indicator
        (fun _ => samplingFirstHeight b h α s) t := by
…
```
Mentions: OAI.FiniteFactor.samplingWeight, OAI.FiniteFactor.samplingFirstLength, OAI.FiniteFactor.samplingFirstHeight

theorem OAI.FiniteFactor.samplingTestedFirstWeight_interval line 27

Source documentation

Rational rectangle tests retain a single interval in the first orientation; no bounded-variation theorem or independent pair density is assumed.

theorem samplingTestedFirstWeight_interval (b : Bool) (h α : ℝ) (E : Set ℝ) (a c s t : ℝ)
    (hh : 0 < h) (hh1 : h < 1) (hα : 0 < α) (hs : s ∈ Set.Ico (0 : ℝ) 1) :
    samplingTestedFirstWeight b h α E (Set.Icc a c) s t =
      (Set.Ioo 0 (samplingFirstLength b h s) ∩ Set.Icc (a-s) (c-s)).indicator
        (fun _ => if s ∈ E then samplingFirstHeight b h α s else 0) t := by
…

Mentions: OAI.FiniteFactor.samplingTestedFirstWeight, OAI.FiniteFactor.samplingFirstLength, OAI.FiniteFactor.samplingFirstHeight

theorem OAI.FiniteFactor.samplingTestedFirstWeight_closed_interval line 51

Source documentation

Closing the two support endpoints changes only those two points, even when the tested interval is empty or degenerates to a singleton.

theorem samplingTestedFirstWeight_closed_interval (b : Bool) (h α : ℝ) (E : Set ℝ) (a c s t : ℝ)
    (hh : 0 < h) (hh1 : h < 1) (hα : 0 < α) (hs : s ∈ Set.Ico (0 : ℝ) 1)
    (ht0 : t ≠ 0) (htL : t ≠ samplingFirstLength b h s) :
    samplingTestedFirstWeight b h α E (Set.Icc a c) s t =
      (Set.Icc (max 0 (a-s)) (min (samplingFirstLength b h s) (c-s))).indicator
        (fun _ => if s ∈ E then samplingFirstHeight b h α s else 0) t := by
…

Mentions: OAI.FiniteFactor.samplingFirstLength, OAI.FiniteFactor.samplingTestedFirstWeight, OAI.FiniteFactor.samplingFirstHeight

theorem OAI.FiniteFactor.samplingTestedFirstWeight_closed_interval_ae line 69

Source documentation

The exact interval representation under any atomless law, including Haar.

theorem samplingTestedFirstWeight_closed_interval_ae (μ : Measure ℝ) [NullSingletonClass μ]
    (b : Bool) (h α : ℝ) (E : Set ℝ) (a c s : ℝ)
    (hh : 0 < h) (hh1 : h < 1) (hα : 0 < α) (hs : s ∈ Set.Ico (0 : ℝ) 1) :
    samplingTestedFirstWeight b h α E (Set.Icc a c) s =ᵐ[μ]
      (Set.Icc (max 0 (a-s)) (min (samplingFirstLength b h s) (c-s))).indicator
        (fun _ => if s ∈ E then samplingFirstHeight b h α s else 0) := by
…

Mentions: OAI.FiniteFactor.samplingTestedFirstWeight, OAI.FiniteFactor.samplingFirstLength, OAI.FiniteFactor.samplingFirstHeight