SumObstruction.lean`

7 declarations, 0 contain sorry, 0 declared as axioms

The operator-theoretic direct-sum obstruction, constructed from stage operators without any uniform bound on their norms.

abbrev OAI.Dixmier.DirectSumObstruction.Stage line 17
abbrev OAI.Dixmier.DirectSumObstruction.Total line 18
abbrev OAI.Dixmier.DirectSumObstruction.Carrier line 19
theorem OAI.Dixmier.DirectSumObstruction.stage_unitary line 21

theorem OAI.Dixmier.DirectSumObstruction.direct_sum_obstruction line 27

Source documentation

The direct-sum obstruction with its representation and bound. The stage operators A_j and T_j need not be uniformly bounded.

theorem direct_sum_obstruction (k : ℕ → ℕ) (hk : ∀ j, 0 < k j)
    (A T : ∀ j, Stage G k j →L[ℂ] Stage G k j)
    (hA : ∀ j, A j ∈ KernelObstruction.Commutant)
    {κ : ℝ} (hκ : 0 ≤ κ)
    (hr : ∀ j, ‖KernelObstruction.row (T j) 1‖ ≤ κ)
    (hc : ∀ j, ‖KernelObstruction.col (A j-T j) 1‖ ≤ κ)
    (hb : ∀ j g, ‖coboundary KernelObstruction.translation (T j) g‖ ≤ κ)
    (he : Tendsto (fun j => KernelObstruction.energy (A j) / k j) atTop atTop) :
    ∃ π : G →* (Carrier G k →L[ℂ] Carrier G k),
      (∀ g, ‖π g‖ ≤ 1 + κ) ∧ ¬ SimilarToUnitary π := by
…

Mentions: OAI.Dixmier.DirectSumObstruction.Stage, OAI.Dixmier.KernelObstruction.Commutant, OAI.Dixmier.KernelObstruction.row, OAI.Dixmier.KernelObstruction.col, OAI.Dixmier.coboundary, OAI.Dixmier.KernelObstruction.translation, OAI.Dixmier.KernelObstruction.energy, OAI.Dixmier.DirectSumObstruction.Carrier, OAI.Dixmier.SimilarToUnitary

theorem OAI.Dixmier.DirectSumObstruction.carrier_separable line 75
Source documentation
The concrete carrier is separable when the group is countable.
```
theorem carrier_separable [Countable G] (k : ℕ → ℕ) :
    TopologicalSpace.SeparableSpace (Carrier G k) := by
…
```
Mentions: OAI.Dixmier.DirectSumObstruction.Carrier

theorem OAI.Dixmier.DirectSumObstruction.separable_direct_sum_obstruction line 83

Source documentation

The direct-sum obstruction with all Hilbert-space structure and separability explicit in the conclusion.

theorem separable_direct_sum_obstruction [Countable G] (k : ℕ → ℕ) (hk : ∀ j, 0 < k j)
    (A T : ∀ j, Stage G k j →L[ℂ] Stage G k j)
    (hA : ∀ j, A j ∈ KernelObstruction.Commutant)
    {κ : ℝ} (hκ : 0 ≤ κ)
    (hr : ∀ j, ‖KernelObstruction.row (T j) 1‖ ≤ κ)
    (hc : ∀ j, ‖KernelObstruction.col (A j-T j) 1‖ ≤ κ)
    (hb : ∀ j g, ‖coboundary KernelObstruction.translation (T j) g‖ ≤ κ)
    (he : Tendsto (fun j => KernelObstruction.energy (A j) / k j) atTop atTop) :
    TopologicalSpace.SeparableSpace (Carrier G k) ∧
    ∃ π : G →* (Carrier G k →L[ℂ] Carrier G k),
      (∀ g, ‖π g‖ ≤ 1 + κ) ∧ ¬ SimilarToUnitary π :=
…