OAI/Analysis/FiniteFactor/CrossedProduct/FiniteCocycleBounds.lean

GitHub source file

4 declarations, 0 contain sorry, 0 declared as axioms

1. theorem OAI.FiniteFactor.SourceAngles.le_one line 10
2. theorem OAI.FiniteFactor.sourceCoordinateFloor_abs_le line 20

   Source documentation

   Earlier coordinates contribute at most K+1 in absolute floor value.

   theorem sourceCoordinateFloor_abs_le (θ : SourceCoordinate → ℝ) (hθ : SourceAngles θ)
       (K : ℕ) (k : ℤ) (hk : |(k : ℝ)| ≤ K) (x : SourceCoordinate → ℝ)
       (hx : ∀ i, x i ∈ Set.Ico 0 1) (i : SourceCoordinate) :
       |(coordinateFloor θ k x i : ℝ)| ≤ (K : ℝ)+1 := by
   …

   Mentions: OAI.FiniteFactor.SourceCoordinate, OAI.FiniteFactor.SourceAngles, OAI.FiniteFactor.coordinateFloor

3. theorem OAI.FiniteFactor.sourcePrefix_logWeight_sum line 36
4. theorem OAI.FiniteFactor.sourceLog_finite_bound line 47

   Source documentation

   If later floors vanish, the actual full source logarithm is bounded by the recursively recorded earlier-block sum.

   theorem sourceLog_finite_bound (θ : SourceCoordinate → ℝ) (hθ : SourceAngles θ)
       (j : ℕ) (k : ℤ) (hk : |(k : ℝ)| ≤ (sourceStageState j).K)
       (x : SourceCoordinate → ℝ) (hx : ∀ i, x i ∈ Set.Ico 0 1)
       (hzero : ∀ i : SourceCoordinate, j ≤ i.1 → coordinateFloor θ k x i = 0) :
       |sourceLog θ sourceLogWeight k x| ≤ (((sourceStageState j).K : ℝ)+1)*(sourceStageState j).B := by
   …

   Mentions: OAI.FiniteFactor.SourceCoordinate, OAI.FiniteFactor.SourceAngles, OAI.FiniteFactor.sourceStageState, OAI.FiniteFactor.coordinateFloor, OAI.FiniteFactor.sourceLog, OAI.FiniteFactor.sourceLogWeight