Weights.lean`

8 declarations, 0 contain sorry, 0 declared as axioms

def OAI.FiniteFactor.samplingDistance line 10
Source documentation
Distance of a representative to the two ends of the unit interval.
```
def samplingDistance (s : ℝ) : ℝ := min s (1-s)
```
def OAI.FiniteFactor.samplingWeight line 12
theorem OAI.FiniteFactor.samplingWeight_measurable line 20
theorem OAI.FiniteFactor.samplingWeight_bounds line 30
theorem OAI.FiniteFactor.samplingWeight_support line 45

theorem OAI.FiniteFactor.samplingWeight_orders line 62

Source documentation

The positive weight already orders each prefix coordinate strictly, with no wrap of the orbit endpoint.

theorem samplingWeight_orders (triangular : Bool) (h α s t : ℝ)
    (hh : 0 < h) (hh1 : h < 1) (hα : 0 < α)
    (hs : s ∈ Set.Ico (0 : ℝ) 1) (hw : samplingWeight triangular h α s t ≠ 0) :
    Int.fract (s+t) = s+t ∧ s < Int.fract (s+t) := by
…

Mentions: OAI.FiniteFactor.samplingWeight

theorem OAI.FiniteFactor.samplingWeight_second_no_wrap line 72

Source documentation

In the second diagonal orientation the nonzero weight has no wrap and the original coordinate is exactly s-t, as in the source calculation.

theorem samplingWeight_second_no_wrap (h α s t : ℝ) (hh : 0 < h) (hh1 : h < 1)
    (hα : 0 < α) (hs : s ∈ Set.Ico (0 : ℝ) 1) (ht : t ∈ Set.Ico (0 : ℝ) 1)
    (hw : samplingWeight false h α (Int.fract (s-t)) t ≠ 0) :
    t < s ∧ Int.fract (s-t) = s-t := by
…

Mentions: OAI.FiniteFactor.samplingWeight

theorem OAI.FiniteFactor.samplingWeight_first_integral line 100

Source documentation

Exact first marginal of either untested one-coordinate weight.

theorem samplingWeight_first_integral (triangular : Bool) (h α s : ℝ)
    (hh : 0 < h) (hh1 : h < 1) (hα : 0 < α) (hs : s ∈ Set.Ico (0 : ℝ) 1) :
    (∫ t, samplingWeight triangular h α s t ∂unitIntervalMeasure) =
      if triangular then 1-s else if α ≤ samplingDistance s then 1 else 0 := by
…

Mentions: OAI.FiniteFactor.samplingWeight, OAI.FiniteFactor.unitIntervalMeasure, OAI.FiniteFactor.samplingDistance