OAI/Analysis/Unitarizability/KernelObstruction.lean

GitHub source file

54 declarations, 0 contain sorry, 0 declared as axioms

Coordinate maps and the invariant-kernel obstruction. The Hilbert space is the lp space with finite Euclidean fibres.

  1. abbrev OAI.Dixmier.KernelObstruction.Fibre line 20
  2. abbrev OAI.Dixmier.KernelObstruction.Space line 21
  3. abbrev OAI.Dixmier.KernelObstruction.Op line 22
  4. def OAI.Dixmier.KernelObstruction.inclusion line 24
  5. def OAI.Dixmier.KernelObstruction.evaluation line 27
  6. theorem OAI.Dixmier.KernelObstruction.inclusion_apply line 30
  7. theorem OAI.Dixmier.KernelObstruction.evaluation_apply line 32
  8. theorem OAI.Dixmier.KernelObstruction.inclusion_norm line 35
  9. theorem OAI.Dixmier.KernelObstruction.inclusion_opNorm_le line 38
  10. theorem OAI.Dixmier.KernelObstruction.evaluation_opNorm_le line 43
  11. theorem OAI.Dixmier.KernelObstruction.inclusion_adjoint line 48
  12. theorem OAI.Dixmier.KernelObstruction.evaluation_inclusion line 58
  13. def OAI.Dixmier.KernelObstruction.block line 63
  14. def OAI.Dixmier.KernelObstruction.row line 66
  15. def OAI.Dixmier.KernelObstruction.col line 69
  16. def OAI.Dixmier.KernelObstruction.coefficients line 72
  17. theorem OAI.Dixmier.KernelObstruction.coefficients_apply line 75
  18. theorem OAI.Dixmier.KernelObstruction.coefficients_norm_sq line 78
  19. theorem OAI.Dixmier.KernelObstruction.space_norm_sq line 83
  20. theorem OAI.Dixmier.KernelObstruction.space_summable line 86
  21. theorem OAI.Dixmier.KernelObstruction.column_summable line 89
  22. theorem OAI.Dixmier.KernelObstruction.column_energy line 94
  23. theorem OAI.Dixmier.KernelObstruction.column_energy_le line 105
  24. theorem OAI.Dixmier.KernelObstruction.coefficients_adjoint_apply line 119
  25. theorem OAI.Dixmier.KernelObstruction.coefficients_adjoint_norm line 125
  26. theorem OAI.Dixmier.KernelObstruction.row_block_norm line 133
  27. theorem OAI.Dixmier.KernelObstruction.row_summable line 139
  28. theorem OAI.Dixmier.KernelObstruction.row_energy_le line 144
  29. def OAI.Dixmier.KernelObstruction.reindex line 152
  30. theorem OAI.Dixmier.KernelObstruction.reindex_norm line 156
  31. def OAI.Dixmier.KernelObstruction.reindexIsometry line 162
  32. def OAI.Dixmier.KernelObstruction.translation line 169

    Source documentation

    The fibre-valued left regular representation.

    def translation : G →* Op G K where
…

    Mentions: OAI.Dixmier.KernelObstruction.Op

  33. theorem OAI.Dixmier.KernelObstruction.translation_apply line 174
  34. theorem OAI.Dixmier.KernelObstruction.translation_inclusion line 177
  35. def OAI.Dixmier.KernelObstruction.Commutant line 187
  36. theorem OAI.Dixmier.KernelObstruction.block_invariant line 189
  37. theorem OAI.Dixmier.KernelObstruction.block_kernel line 197
  38. theorem OAI.Dixmier.KernelObstruction.block_sub line 204
  39. theorem OAI.Dixmier.KernelObstruction.coefficients_sub line 209
  40. theorem OAI.Dixmier.KernelObstruction.commutant_sub line 212
  41. def OAI.Dixmier.KernelObstruction.energy line 218
  42. theorem OAI.Dixmier.KernelObstruction.energy_summable line 220
  43. theorem OAI.Dixmier.KernelObstruction.energy_nonneg line 224
  44. theorem OAI.Dixmier.KernelObstruction.energy_le_row line 226
  45. theorem OAI.Dixmier.KernelObstruction.energy_eq_column line 230
  46. theorem OAI.Dixmier.KernelObstruction.energy_le_column line 236
  47. theorem OAI.Dixmier.KernelObstruction.row_norm_le line 242
  48. theorem OAI.Dixmier.KernelObstruction.col_norm_le line 247
  49. theorem OAI.Dixmier.KernelObstruction.row_difference_bound line 252
  50. theorem OAI.Dixmier.KernelObstruction.col_difference_bound line 259
  51. theorem OAI.Dixmier.KernelObstruction.energy_split_le line 267
  52. theorem OAI.Dixmier.KernelObstruction.kernel_obstruction line 286

    Source documentation

    The kernel-energy obstruction, proved from coordinate estimates and commutation.

    theorem kernel_obstruction {A T : Op G K} (hA : A ∈ Commutant)
    {κ : ℝ} (_hκ : 0 ≤ κ) (hr : ‖row T 1‖ ≤ κ) (hc : ‖col (A-T) 1‖ ≤ κ)
    {C : Op G K} (hC : C ∈ Commutant) :
    energy A ≤ 4 * (Fintype.card K : ℝ) * (κ + ‖T-C‖)^2 := by
…

    Mentions: OAI.Dixmier.KernelObstruction.Op, OAI.Dixmier.KernelObstruction.Commutant, OAI.Dixmier.KernelObstruction.row, OAI.Dixmier.KernelObstruction.col, OAI.Dixmier.KernelObstruction.energy

  53. theorem OAI.Dixmier.KernelObstruction.kernel_distance_pointwise line 301

    Source documentation

    Pointwise distance inequality for positive fibre dimension.

    theorem kernel_distance_pointwise [Nonempty K] {A T : Op G K} (hA : A ∈ Commutant)
    {κ : ℝ} (hκ : 0 ≤ κ) (hr : ‖row T 1‖ ≤ κ) (hc : ‖col (A-T) 1‖ ≤ κ)
    {C : Op G K} (hC : C ∈ Commutant) :
    (1/2 : ℝ) * Real.sqrt (energy A / Fintype.card K) - κ ≤ ‖T-C‖ := by
…

    Mentions: OAI.Dixmier.KernelObstruction.Op, OAI.Dixmier.KernelObstruction.Commutant, OAI.Dixmier.KernelObstruction.row, OAI.Dixmier.KernelObstruction.col, OAI.Dixmier.KernelObstruction.energy

  54. theorem OAI.Dixmier.KernelObstruction.kernel_distance line 318

    Source documentation

    The distance obstruction for the metric distance to all bounded translation-commuting operators.

    theorem kernel_distance [Nonempty K] {A T : Op G K} (hA : A ∈ Commutant)
    {κ : ℝ} (hκ : 0 ≤ κ) (hr : ‖row T 1‖ ≤ κ) (hc : ‖col (A-T) 1‖ ≤ κ) :
    (1/2 : ℝ) * Real.sqrt (energy A / Fintype.card K) - κ ≤ Metric.infDist T Commutant := by
…

    Mentions: OAI.Dixmier.KernelObstruction.Op, OAI.Dixmier.KernelObstruction.Commutant, OAI.Dixmier.KernelObstruction.row, OAI.Dixmier.KernelObstruction.col, OAI.Dixmier.KernelObstruction.energy