OAI/Analysis/CharacterCriterion/CubeField.lean

GitHub source file

40 declarations, 0 contain sorry, 0 declared as axioms

  1. lemma OAI.KirchbergRordam.GenericRW.CubeField.norm_matrix_unit line 30
  2. def OAI.KirchbergRordam.GenericRW.CubeField.dampedFun line 37
  3. lemma OAI.KirchbergRordam.GenericRW.CubeField.damped_zero line 39
  4. lemma OAI.KirchbergRordam.GenericRW.CubeField.damped_norm line 40
  5. lemma OAI.KirchbergRordam.GenericRW.CubeField.damped_continuous line 46
  6. def OAI.KirchbergRordam.GenericRW.CubeField.damped line 64
  7. def OAI.KirchbergRordam.GenericRW.CubeField.scalarH line 67
  8. def OAI.KirchbergRordam.GenericRW.CubeField.scalarSqrt line 68
  9. def OAI.KirchbergRordam.GenericRW.CubeField.x line 69
  10. def OAI.KirchbergRordam.GenericRW.CubeField.v line 70
  11. def OAI.KirchbergRordam.GenericRW.CubeField.h line 72
  12. lemma OAI.KirchbergRordam.GenericRW.CubeField.x_apply line 73
  13. lemma OAI.KirchbergRordam.GenericRW.CubeField.x_zero line 75
  14. lemma OAI.KirchbergRordam.GenericRW.CubeField.v_apply line 76
  15. lemma OAI.KirchbergRordam.GenericRW.CubeField.v_zero line 78
  16. lemma OAI.KirchbergRordam.GenericRW.CubeField.x_star line 80
  17. lemma OAI.KirchbergRordam.GenericRW.CubeField.x_mul line 86
  18. lemma OAI.KirchbergRordam.GenericRW.CubeField.x_diagonal line 98
  19. lemma OAI.KirchbergRordam.GenericRW.CubeField.v_star_mul line 106
  20. lemma OAI.KirchbergRordam.GenericRW.CubeField.v_mul_star line 113
  21. lemma OAI.KirchbergRordam.GenericRW.CubeField.x_support line 121
  22. lemma OAI.KirchbergRordam.GenericRW.CubeField.x_localized line 128
  23. lemma OAI.KirchbergRordam.GenericRW.CubeField.h_nonneg line 139
  24. lemma OAI.KirchbergRordam.GenericRW.CubeField.h_norm line 143
  25. def OAI.KirchbergRordam.GenericRW.CubeField.weighted line 151
  26. lemma OAI.KirchbergRordam.GenericRW.CubeField.first_nonneg line 160
  27. lemma OAI.KirchbergRordam.GenericRW.CubeField.second_nonneg line 164
  28. lemma OAI.KirchbergRordam.GenericRW.CubeField.pair_orthogonal line 169
  29. lemma OAI.KirchbergRordam.GenericRW.CubeField.entry_norm line 178
  30. def OAI.KirchbergRordam.GenericRW.ConeCube.family line 193
  31. lemma OAI.KirchbergRordam.GenericRW.ConeCube.x_face_commute line 195
  32. lemma OAI.KirchbergRordam.GenericRW.ConeCube.x_liftable line 209
  33. def OAI.KirchbergRordam.GenericRW.ConeCube.x line 217
  34. lemma OAI.KirchbergRordam.GenericRW.ConeCube.repr_x line 218
  35. def OAI.KirchbergRordam.GenericRW.ConeCube.hScalar line 221
  36. def OAI.KirchbergRordam.GenericRW.ConeCube.h line 223
  37. lemma OAI.KirchbergRordam.GenericRW.ConeCube.repr_h line 224
  38. lemma OAI.KirchbergRordam.GenericRW.ConeCube.h_nonneg line 231
  39. lemma OAI.KirchbergRordam.GenericRW.ConeCube.h_norm line 235
  40. def OAI.KirchbergRordam.GenericRW.ConeCube.weighted line 242