OAI/RepresentationTheory/VertexAlgebra/CutoffPowerControl.lean

GitHub source file

22 declarations, 0 contain sorry, 0 declared as axioms

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

  1. def OAI.StronglyRationalVOA.CutoffPowerControl line 12
  2. theorem OAI.StronglyRationalVOA.cutoffPowerControl_add line 15
  3. theorem OAI.StronglyRationalVOA.cutoffPowerControl_sum line 28
  4. theorem OAI.StronglyRationalVOA.cutoffPowerControl_one line 44
  5. theorem OAI.StronglyRationalVOA.root_lift_power_bound line 50
  6. theorem OAI.StronglyRationalVOA.CFTTypeVOA.UnitaryStructure.sharpMajorant_power_contraction line 72
  7. def OAI.StronglyRationalVOA.PolynomialCutoffControl line 135
  8. theorem OAI.StronglyRationalVOA.polynomialCutoffControl_add line 138
  9. theorem OAI.StronglyRationalVOA.polynomialCutoffControl_sum line 153
  10. theorem OAI.StronglyRationalVOA.polynomialCutoffControl_one line 164
  11. theorem OAI.StronglyRationalVOA.rpow_inv_nat_le_one_add line 167
  12. theorem OAI.StronglyRationalVOA.polynomialCutoffControl_root line 176
  13. theorem OAI.StronglyRationalVOA.CFTTypeVOA.UnitaryStructure.positiveColumnNorm_sq_polynomial line 191
  14. theorem OAI.StronglyRationalVOA.CFTTypeVOA.UnitaryStructure.sharpQuantities_polynomial line 225
  15. theorem OAI.StronglyRationalVOA.CFTTypeVOA.UnitaryStructure.sharpMajorant_polynomial line 244
  16. theorem OAI.StronglyRationalVOA.multiplicative_cutoff_log_bound line 273
  17. theorem OAI.StronglyRationalVOA.polynomial_power_contraction_bounded line 323
  18. theorem OAI.StronglyRationalVOA.CFTTypeVOA.UnitaryStructure.exists_bounded_sharpGrowth line 379
  19. theorem OAI.StronglyRationalVOA.CFTTypeVOA.UnitaryStructure.optimal_quasiPrimary_cutoff line 394
  20. theorem OAI.StronglyRationalVOA.CFTTypeVOA.UnitaryStructure.physical_energyBound_of_cutoffs line 445
  21. theorem OAI.StronglyRationalVOA.CFTTypeVOA.UnitaryStructure.optimal_quasiPrimary_energyBound line 474
  22. theorem OAI.StronglyRationalVOA.CFTTypeVOA.UnitaryStructure.current_linear_energyBound line 484