Cocycle.lean`

GitHub source file

13 declarations, 0 contain sorry, 0 declared as axioms

def OAI.FiniteFactor.coordinateRotate line 12
Source documentation
Integer iterates of the source rotation, in [0,1) representatives.
Also declared: ComparatorChallenges/ProductBrown.lean:312 (same declaration text).
```
def coordinateRotate {ι : Type*} (θ : ι → ℝ) (k : ℤ) (x : ι → ℝ) (i : ι) : ℝ :=
…
```
theorem OAI.FiniteFactor.coordinateFloor_add line 15
theorem OAI.FiniteFactor.finiteFloorSupport_rotate line 27
def OAI.FiniteFactor.sourceLog line 39
Source documentation
The source logarithmic cocycle, using the actual weighted floor sum.
Also declared: ComparatorChallenges/ProductBrown.lean:315 (same declaration text).
```
def sourceLog {ι : Type*} (θ c : ι → ℝ) (k : ℤ) (x : ι → ℝ) : ℝ :=
…
```
def OAI.FiniteFactor.sourceCocycle line 42
Also declared: ComparatorChallenges/ProductBrown.lean:318 (same declaration text).
theorem OAI.FiniteFactor.sourceLog_summable line 45
theorem OAI.FiniteFactor.sourceLog_add line 56
theorem OAI.FiniteFactor.sourceCocycle_add line 66
Source documentation
The actual cocycle identity, proved on the conull domain supplied by Borel--Cantelli. The rotation and sums are explicit.
```
theorem sourceCocycle_add {ι : Type*} (θ c : ι → ℝ) {x : ι → ℝ}
    (hx : finiteFloorSupport θ x) (k n : ℤ) :
    sourceCocycle θ c (k+n) x = sourceCocycle θ c n (coordinateRotate θ k x) * sourceCocycle θ c k x := by
…
```
Mentions: OAI.FiniteFactor.finiteFloorSupport, OAI.FiniteFactor.sourceCocycle, OAI.FiniteFactor.coordinateRotate
theorem OAI.FiniteFactor.sourceCocycle_pos line 72
Also declared: ComparatorChallenges/ProductBrown.lean:321 (same declaration text).
theorem OAI.FiniteFactor.sourceCocycle_zero line 75
theorem OAI.FiniteFactor.sourceCocycle_measurable line 81
Also declared: ComparatorChallenges/ProductBrown.lean:324 (same declaration text).
theorem OAI.FiniteFactor.sourceWeight_le_one line 96
Source documentation
The weight f=F_1 is positive and at most one on the source coordinate cube.
Also declared: ComparatorChallenges/ProductBrown.lean:338 (same declaration text).
```
theorem sourceWeight_le_one {ι : Type*} (θ c : ι → ℝ)
    (hθ : ∀ i, 0 ≤ θ i) (hc : ∀ i, 0 ≤ c i) {x : ι → ℝ}
    (hx : ∀ i, x i ∈ Set.Ico 0 1) : sourceCocycle θ c 1 x ≤ 1 := by
…
```
Mentions: OAI.FiniteFactor.sourceCocycle
theorem OAI.FiniteFactor.sourceCocycle_ordered line 109
Source documentation
Ordered endpoints give the ratio bound for every integer, including negative integers. Both infinite sums are justified by finite support.
```
theorem sourceCocycle_ordered {ι : Type*} (θ c : ι → ℝ)
    (hc : ∀ i, 0 ≤ c i) {x y : ι → ℝ}
    (hx : finiteFloorSupport θ x) (hy : finiteFloorSupport θ y)
    (hxy : ∀ i, x i ≤ y i) (k : ℤ) : sourceCocycle θ c k y ≤ sourceCocycle θ c k x := by
…
```
Mentions: OAI.FiniteFactor.finiteFloorSupport, OAI.FiniteFactor.sourceCocycle