Attenuation.lean`

3 declarations, 0 contain sorry, 0 declared as axioms

theorem OAI.FiniteFactor.floor_crossing_gap line 12
Source documentation
Crossing 1-fract(a) raises the integer floor by exactly one, for either sign of a. The half-open endpoints match the source's representatives.
```
theorem floor_crossing_gap {x y a : ℝ} (hx : x ∈ Set.Ico 0 1) (hy : y ∈ Set.Ico 0 1)
    (hcross : x < 1-Int.fract a ∧ 1-Int.fract a ≤ y) :
    Int.floor (y+a) = Int.floor (x+a)+1 := by
…
```

theorem OAI.FiniteFactor.sourceCocycle_crossing_attenuation line 30

Source documentation

Every actual threshold crossing supplies the factor exp(-c_i) in the source cocycle ratio. No attenuation property of an operator is assumed.

theorem sourceCocycle_crossing_attenuation {ι : Type*} (θ c : ι → ℝ)
    (hc : ∀ i, 0 ≤ c i) {x y : ι → ℝ}
    (hx : finiteFloorSupport θ x) (hy : finiteFloorSupport θ y)
    (hxy : ∀ i, x i ≤ y i) (k : ℤ) (i : ι)
    (hxi : x i ∈ Set.Ico 0 1) (hyi : y i ∈ Set.Ico 0 1)
    (hcross : x i < 1-Int.fract ((k : ℝ)*θ i) ∧ 1-Int.fract ((k : ℝ)*θ i) ≤ y i) :
    sourceCocycle θ c k y / sourceCocycle θ c k x ≤ Real.exp (-c i) := by
…

Mentions: OAI.FiniteFactor.finiteFloorSupport, OAI.FiniteFactor.sourceCocycle

theorem OAI.FiniteFactor.sourceCocycle_prefix_bound line 58

Source documentation

The genuine finite-prefix bound for the source cocycle F_n. This is the pointwise estimate needed before lifting the bound to powers of T.

theorem sourceCocycle_prefix_bound {ι : Type*} (θ c : ι → ℝ)
    (hθ : ∀ i, 0 ≤ θ i) (hc : ∀ i, 0 ≤ c i) {x : ι → ℝ}
    (hx : finiteFloorSupport θ x) (hx0 : ∀ i, 0 ≤ x i) (I : Finset ι) (n : ℕ) :
    sourceCocycle θ c n x ≤ Real.exp ((∑ i ∈ I, c i) - (n : ℝ)*(∑ i ∈ I, c i*θ i)) := by
…

Mentions: OAI.FiniteFactor.finiteFloorSupport, OAI.FiniteFactor.sourceCocycle