OAI/Analysis/Unitarizability/MaskAlgebra.lean

GitHub source file

12 declarations, 0 contain sorry, 0 declared as axioms

Sparse masks yield operator conjugation identities, and the constant mask has a rank-one collision kernel.

  1. theorem OAI.Dixmier.Masked.masked_bound_of_frame line 19

    Source documentation

    The masked operator bound in finite-cardinality form.

    theorem masked_bound_of_frame (v : I → Fibre K) (s : I → G) (c : G → I → ℂ)
    (hc : ∀ x i, ‖c x i‖ ≤ 1) {p : ℕ} {b : ℝ} (hb : 0 ≤ b)
    (hv : FiniteSynthesis.FrameBound v p b)
    (hr : ∀ x, (rowSet c x).card ≤ p) (hcol : ∀ y, (columnSet s c y).card ≤ p) :
    ‖operator v s c hc‖ ≤ b^2 :=
…

    Mentions: OAI.Dixmier.Masked.Fibre, OAI.Dixmier.FiniteSynthesis.FrameBound, OAI.Dixmier.Masked.rowSet, OAI.Dixmier.Masked.columnSet, OAI.Dixmier.Masked.operator

  2. theorem OAI.Dixmier.Masked.operator_sub line 26
  3. theorem OAI.Dixmier.Masked.conjugate_operator line 37
  4. def OAI.Dixmier.Masked.constant line 49
  5. theorem OAI.Dixmier.Masked.constant_commutant line 52
  6. theorem OAI.Dixmier.Masked.basis_inner_right line 59
  7. theorem OAI.Dixmier.Masked.constant_kernel line 63
  8. theorem OAI.Dixmier.Masked.constant_energy_ge_card line 80
  9. theorem OAI.Dixmier.Masked.bool_mask_norm line 87
  10. def OAI.Dixmier.Masked.oriented line 90
  11. theorem OAI.Dixmier.Masked.difference_operator line 93
  12. theorem OAI.Dixmier.Masked.difference_norm_le line 100