OAI/Analysis/Unitarizability/Masked.lean

GitHub source file

17 declarations, 0 contain sorry, 0 declared as axioms

1. abbrev OAI.Dixmier.Masked.Space line 17
2. abbrev OAI.Dixmier.Masked.Fibre line 18
3. def OAI.Dixmier.Masked.shift line 20
4. theorem OAI.Dixmier.Masked.shift_apply line 23
5. def OAI.Dixmier.Masked.term line 25
6. def OAI.Dixmier.Masked.operator line 33
7. theorem OAI.Dixmier.Masked.term_apply line 37
8. theorem OAI.Dixmier.Masked.operator_apply line 43
9. def OAI.Dixmier.Masked.rowSet line 48
10. def OAI.Dixmier.Masked.columnSet line 49
11. def OAI.Dixmier.Masked.edgeEnergy line 52
12. theorem OAI.Dixmier.Masked.edge_summable line 56
13. theorem OAI.Dixmier.Masked.edgeEnergy_summable line 72
14. theorem OAI.Dixmier.Masked.sum_subfamily line 75
15. theorem OAI.Dixmier.Masked.row_estimate line 79
16. theorem OAI.Dixmier.Masked.edgeEnergy_reindex line 110
17. theorem OAI.Dixmier.Masked.masked_bound line 135

    Source documentation

    Row and column synthesis bounds imply the masked operator bound, without assuming that the product labels s_i are distinct.

    theorem masked_bound (v : I → Fibre K) (s : I → G) (c : G → I → ℂ)
        (hc : ∀ x i, ‖c x i‖ ≤ 1) {b : ℝ} (hb : 0 ≤ b)
        (hrow : ∀ x, ‖FiniteSynthesis.synthesis v (rowSet c x)‖ ≤ b)
        (hcol : ∀ y, ‖FiniteSynthesis.synthesis v (columnSet s c y)‖ ≤ b) :
        ‖operator v s c hc‖ ≤ b^2 := by
    …

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