OAI/Analysis/FiniteFactor/CrossedProduct/ConvolutionCocycle.lean

GitHub source file

2 declarations, 0 contain sorry, 0 declared as axioms

1. theorem OAI.FiniteFactor.sourceCocycle_antitone line 11

   Source documentation

   The actual cocycle is antitone in every integer index, including negative indices.

   theorem sourceCocycle_antitone {ι : Type*} (θ c : ι → ℝ)
       (hθ : ∀ i, 0 ≤ θ i) (hc : ∀ i, 0 ≤ c i)
       {x : ι → ℝ} (hx : finiteFloorSupport θ x) :
       Antitone (fun k : ℤ => sourceCocycle θ c k x) := by
   …

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

2. theorem OAI.FiniteFactor.sourceCocycle_power_weight line 28

   Source documentation

   Exact positive-power weight in terms of the two integer cocycle values.

   theorem sourceCocycle_power_weight {ι : Type*} (θ c : ι → ℝ)
       {x : ι → ℝ} (hx : finiteFloorSupport θ x) (n : ℕ) (k : ℤ) :
       sourceCocycle θ c n (coordinateRotate θ k x) =
         sourceCocycle θ c ((n : ℤ)+k) x / sourceCocycle θ c k x := by
   …

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