OAI/Analysis/FiniteFactor/CrossedProduct/Powers.lean

GitHub source file

7 declarations, 0 contain sorry, 0 declared as axioms

1. theorem OAI.FiniteFactor.coordinateRotate_add line 13

   Source documentation

   Composition of the actual representative rotations.

   theorem coordinateRotate_add {ι : Type*} (θ : ι → ℝ) (k n : ℤ) (x : ι → ℝ) :
       coordinateRotate θ n (coordinateRotate θ k x) = coordinateRotate θ (k+n) x := by
   …

   Mentions: OAI.FiniteFactor.coordinateRotate

2. def OAI.FiniteFactor.sourceShiftNIndex line 23
3. theorem OAI.FiniteFactor.sourceShiftNIndex_preserving line 26
4. theorem OAI.FiniteFactor.sourceOperator_apply_ae line 38
5. theorem OAI.FiniteFactor.sourceOperator_pow_apply_ae line 50

   Source documentation

   The actual powers of the constructed weighted shift, on the conull finite-floor-support domain. No power formula is assumed.

   theorem sourceOperator_pow_apply_ae {ι : Type*} [Countable ι] (θ c : ι → ℝ)
       (hθ : ∀ i, 0 ≤ θ i) (hc : ∀ i, 0 ≤ c i)
       (hs : Summable (fun i => |θ i|)) (n : ℕ) (f : SourceHilbert ι) :
       (sourceOperator θ c hθ hc ^ n) f =ᵐ[sourceMeasure ι] fun z =>
         (sourceCocycle θ c n (coordinateRotate θ (z.2-(n : ℤ)) z.1) : ℂ) *
           f (sourceShiftNIndex n z) := by
   …

   Mentions: OAI.FiniteFactor.SourceHilbert, OAI.FiniteFactor.sourceOperator, OAI.FiniteFactor.sourceMeasure, OAI.FiniteFactor.sourceCocycle, OAI.FiniteFactor.coordinateRotate, OAI.FiniteFactor.sourceShiftNIndex

6. theorem OAI.FiniteFactor.sourceOperator_pow_norm_prefix_bound line 96

   Source documentation

   The source's finite-prefix operator bound, now for the constructed T.

   theorem sourceOperator_pow_norm_prefix_bound {ι : Type*} [Countable ι] (θ c : ι → ℝ)
       (hθ : ∀ i, 0 ≤ θ i) (hc : ∀ i, 0 ≤ c i)
       (hs : Summable (fun i => |θ i|)) (I : Finset ι) (n : ℕ) :
       ‖sourceOperator θ c hθ hc ^ n‖ ≤
         Real.exp ((∑ i ∈ I, c i) - (n : ℝ)*(∑ i ∈ I, c i*θ i)) := by
   …

   Mentions: OAI.FiniteFactor.sourceOperator

7. theorem OAI.FiniteFactor.sourceOperator_norm_quasinilpotent line 120

   Source documentation

   Norm quasinilpotence of this concrete operator follows from divergence of its coordinate weighted-angle sums, not from any assumed operator property.

   theorem sourceOperator_norm_quasinilpotent {ι : Type*} [Countable ι] (θ c : ι → ℝ)
       (hθ : ∀ i, 0 ≤ θ i) (hc : ∀ i, 0 ≤ c i)
       (hs : Summable (fun i => |θ i|)) (I : ℕ → Finset ι)
       (hdiv : Tendsto (fun q => ∑ i ∈ I q, c i*θ i) atTop atTop) :
       Tendsto (fun n : ℕ => ‖sourceOperator θ c hθ hc ^ n‖ ^ (1/(n : ℝ))) atTop (𝓝 0) :=
   …

   Mentions: OAI.FiniteFactor.sourceOperator