OAI/Analysis/FiniteFactor/CrossedProduct/Operator.lean

GitHub source file

18 declarations, 0 contain sorry, 0 declared as axioms

1. abbrev OAI.FiniteFactor.sourceMeasure line 14

   Source documentation

   The regular representation written as L2(X × Z), canonically equivalent to the source's L2(X; l2(Z)).

   Also declared: ComparatorChallenges/ProductBrown.lean:359 (same declaration text).

   abbrev sourceMeasure (ι : Type*) : Measure ((ι → ℝ) × ℤ) :=
   …

2. abbrev OAI.FiniteFactor.SourceHilbert line 17

   Also declared: ComparatorChallenges/ProductBrown.lean:362 (same declaration text).

3. def OAI.FiniteFactor.sourceDiagonal line 20

   Source documentation

   The actual diagonal entry f(sigma^k x) of pi(f).

   Also declared: ComparatorChallenges/ProductBrown.lean:364 (same declaration text).

   def sourceDiagonal {ι : Type*} (θ c : ι → ℝ) (z : (ι → ℝ) × ℤ) : ℂ :=
   …

4. theorem OAI.FiniteFactor.sourceDiagonal_measurable line 23

   Also declared: ComparatorChallenges/ProductBrown.lean:367 (same declaration text).

5. theorem OAI.FiniteFactor.sourceDiagonal_norm_le line 32

   Also declared: ComparatorChallenges/ProductBrown.lean:376 (same declaration text).

6. theorem OAI.FiniteFactor.sourceDiagonal_ne_zero line 40
7. theorem OAI.FiniteFactor.sourceDiagonal_memLp line 45

   Also declared: ComparatorChallenges/ProductBrown.lean:384 (same declaration text).

8. def OAI.FiniteFactor.sourceMultiplication line 52

   Source documentation

   A bounded multiplication operator from the actual source formula.

   Also declared: ComparatorChallenges/ProductBrown.lean:390 (same declaration text).

   def sourceMultiplication {ι : Type*} [Countable ι] (θ c : ι → ℝ)
       (hθ : ∀ i, 0 ≤ θ i) (hc : ∀ i, 0 ≤ c i) : SourceHilbert ι →L[ℂ] SourceHilbert ι :=
   …

   Mentions: OAI.FiniteFactor.SourceHilbert

9. theorem OAI.FiniteFactor.sourceMultiplication_apply_ae line 57
10. theorem OAI.FiniteFactor.sourceMultiplication_injective line 65
11. def OAI.FiniteFactor.sourceShiftIndex line 76

    Source documentation

    The shift S e_k=e_(k+1), so its action on coordinate functions uses k-1.

    Also declared: ComparatorChallenges/ProductBrown.lean:395 (same declaration text).

    def sourceShiftIndex {ι : Type*} (z : (ι → ℝ) × ℤ) : (ι → ℝ) × ℤ := (z.1, z.2-1)

12. theorem OAI.FiniteFactor.sourceShiftIndex_preserving line 78

    Also declared: ComparatorChallenges/ProductBrown.lean:397 (same declaration text).

13. def OAI.FiniteFactor.sourceShift line 90

    Also declared: ComparatorChallenges/ProductBrown.lean:409 (same declaration text).

14. def OAI.FiniteFactor.sourceOperator line 95

    Source documentation

    T=U pi(f), constructed as a bounded operator, with no assumed factor or invariant-subspace properties.

    Also declared: ComparatorChallenges/ProductBrown.lean:412 (same declaration text).

    def sourceOperator {ι : Type*} [Countable ι] (θ c : ι → ℝ)
        (hθ : ∀ i, 0 ≤ θ i) (hc : ∀ i, 0 ≤ c i) : SourceHilbert ι →L[ℂ] SourceHilbert ι :=
    …

    Mentions: OAI.FiniteFactor.SourceHilbert

15. theorem OAI.FiniteFactor.sourceOperator_injective line 99
16. theorem OAI.FiniteFactor.sourceMultiplication_norm_le line 107
17. theorem OAI.FiniteFactor.sourceOperator_norm_le_one line 115
18. theorem OAI.FiniteFactor.sourceOperator_ne_zero line 125

    Source documentation

    This constructs a nonzero bounded T, independently of any candidate projection.

    theorem sourceOperator_ne_zero {ι : Type*} [Countable ι] (θ c : ι → ℝ)
        (hθ : ∀ i, 0 ≤ θ i) (hc : ∀ i, 0 ≤ c i) : sourceOperator θ c hθ hc ≠ 0 := by
    …

    Mentions: OAI.FiniteFactor.sourceOperator