OAI/RepresentationTheory/VertexAlgebra/SmoothConjugatePrimary.lean

GitHub source file

26 declarations, 0 contain sorry, 0 declared as axioms

Vertex algebra, energy bounds and closed smeared-field operators.

  1. lemma OAI.StronglyRationalVOA.CFTTypeVOA.UnitaryStructure.smoothConjugate_primary_real_graph line 37
  2. lemma OAI.StronglyRationalVOA.CFTTypeVOA.UnitaryStructure.primary_complex_graph_invariant line 67
  3. lemma OAI.StronglyRationalVOA.CFTTypeVOA.UnitaryStructure.primary_complex_entry_mem line 97
  4. lemma OAI.StronglyRationalVOA.CFTTypeVOA.smearedMap_add_state line 116
  5. lemma OAI.StronglyRationalVOA.CFTTypeVOA.smearedMap_smul_state line 124
  6. lemma OAI.StronglyRationalVOA.CFTTypeVOA.UnitaryStructure.sobolevExtension_add line 132
  7. lemma OAI.StronglyRationalVOA.CFTTypeVOA.UnitaryStructure.smoothSmear_add_state line 145
  8. lemma OAI.StronglyRationalVOA.CFTTypeVOA.UnitaryStructure.smoothSmear_smul_state line 175
  9. lemma OAI.StronglyRationalVOA.CFTTypeVOA.UnitaryStructure.smoothSmear_zero_state line 198
  10. def OAI.StronglyRationalVOA.CFTTypeVOA.UnitaryStructure.stateCommutant line 203
  11. lemma OAI.StronglyRationalVOA.CFTTypeVOA.UnitaryStructure.primary_graph_invariant_of_hermitian line 215
  12. lemma OAI.StronglyRationalVOA.CFTTypeVOA.UnitaryStructure.smoothConjugate_primary_complex_graph line 241
  13. lemma OAI.StronglyRationalVOA.CFTTypeVOA.UnitaryStructure.all_primary_graph_invariant line 269
  14. lemma OAI.StronglyRationalVOA.CFTTypeVOA.UnitaryStructure.all_primary_entry_mem line 294
  15. lemma OAI.StronglyRationalVOA.frequency_weight_shift line 312
  16. lemma OAI.StronglyRationalVOA.RapidCoefficients.shift line 320
  17. lemma OAI.StronglyRationalVOA.CFTTypeVOA.UnitaryStructure.physicalMode_bound_of_homogeneous line 337
  18. lemma OAI.StronglyRationalVOA.CFTTypeVOA.UnitaryStructure.physicalMode_positive_shift_bound line 360
  19. lemma OAI.StronglyRationalVOA.CFTTypeVOA.UnitaryStructure.physicalMode_sobolev_fixed_bound line 394
  20. lemma OAI.StronglyRationalVOA.CFTTypeVOA.UnitaryStructure.physicalMode_positive_shift_sobolev_bound line 427
  21. lemma OAI.StronglyRationalVOA.CFTTypeVOA.UnitaryStructure.weightedSmearedMap_positive_shift_bound line 444
  22. lemma OAI.StronglyRationalVOA.CFTTypeVOA.UnitaryStructure.smearedMap_positive_shift_bound line 476
  23. lemma OAI.StronglyRationalVOA.CFTTypeVOA.UnitaryStructure.smoothSmear_positive_shift_bound line 486
  24. lemma OAI.StronglyRationalVOA.CFTTypeVOA.UnitaryStructure.smoothEnergyPower_smoothSmear_eq_extension line 497
  25. lemma OAI.StronglyRationalVOA.CFTTypeVOA.UnitaryStructure.smoothSmear_positive_shift_sobolev_bound line 511
  26. lemma OAI.StronglyRationalVOA.coefficientSeminorm_shift line 533