OAI/RepresentationTheory/VertexAlgebra/ApproximatingFlowDerivative.lean

GitHub source file

25 declarations, 0 contain sorry, 0 declared as axioms

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

  1. lemma OAI.StronglyRationalVOA.SymmetricOperator.approximatingFlow_derivative line 14
  2. lemma OAI.StronglyRationalVOA.SymmetricOperator.approximatingFlow_continuous line 20
  3. lemma OAI.StronglyRationalVOA.SymmetricOperator.approximatingFlow_derivative_limit line 24
  4. lemma OAI.StronglyRationalVOA.SymmetricOperator.flow_integral line 38
  5. lemma OAI.StronglyRationalVOA.SymmetricOperator.flow_derivative line 59
  6. lemma OAI.StronglyRationalVOA.StrongLimit.apply_tendsto line 79
  7. lemma OAI.StronglyRationalVOA.StrongLimit.hasDerivAt_apply line 94
  8. lemma OAI.StronglyRationalVOA.SymmetricOperator.norm_le_exp_of_derivative_bound line 114
  9. lemma OAI.StronglyRationalVOA.SymmetricOperator.flow_opNorm line 140
  10. lemma OAI.StronglyRationalVOA.SymmetricOperator.flow_adjoint line 146
  11. lemma OAI.StronglyRationalVOA.SymmetricOperator.regularizer_flow_bound line 155
  12. lemma OAI.StronglyRationalVOA.SymmetricOperator.flow_regularizer_factor line 218
  13. lemma OAI.StronglyRationalVOA.HilbertScale.inverseEnergy_dense line 243
  14. lemma OAI.StronglyRationalVOA.HilbertScale.inverseEnergy_on_graph line 253
  15. lemma OAI.StronglyRationalVOA.HilbertScale.flow_energy_graph line 260
  16. lemma OAI.StronglyRationalVOA.CFTTypeVOA.UnitaryStructure.physicalMode_power_commutator_bound line 286
  17. lemma OAI.StronglyRationalVOA.CFTTypeVOA.UnitaryStructure.energyShift_pow_adjoint line 330
  18. def OAI.StronglyRationalVOA.CFTTypeVOA.UnitaryStructure.smearedPowerCommutator line 346
  19. lemma OAI.StronglyRationalVOA.CFTTypeVOA.UnitaryStructure.smearedPowerCommutator_apply line 351
  20. lemma OAI.StronglyRationalVOA.CFTTypeVOA.UnitaryStructure.smearedPowerCommutator_bound line 367
  21. lemma OAI.StronglyRationalVOA.CFTTypeVOA.UnitaryStructure.weightedSmearedMap_inner line 394
  22. lemma OAI.StronglyRationalVOA.CFTTypeVOA.UnitaryStructure.smearedPowerCommutator_pairing line 405
  23. lemma OAI.StronglyRationalVOA.StrongLimit.tendsto_of_denseRange line 422
  24. lemma OAI.StronglyRationalVOA.SymmetricOperator.selfAdjoint_injective_of_denseRange line 448
  25. lemma OAI.StronglyRationalVOA.SymmetricOperator.regularizer_factor_continuous_zero line 468