OAI/Combinatorics/PolynomialVacuum/Separator/NormalFamily.lean

GitHub source file

11 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.PolynomialVacuumCylinder.separatorComplexExponent line 10
  2. def OAI.PolynomialVacuumCylinder.normalizedSeparatorFamily line 13
  3. def OAI.PolynomialVacuumCylinder.separatorNormalizationPoint line 17
  4. theorem OAI.PolynomialVacuumCylinder.separatorComplexExponent_re line 19
  5. theorem OAI.PolynomialVacuumCylinder.normalizationPoint_cosh line 26
  6. theorem OAI.PolynomialVacuumCylinder.normalizationPoint_exponent line 30
  7. theorem OAI.PolynomialVacuumCylinder.normalizedSeparatorFamily_normalized line 37
  8. theorem OAI.PolynomialVacuumCylinder.normalizedSeparatorFamily_analyticAt line 41
  9. theorem OAI.PolynomialVacuumCylinder.normalizedSeparatorFamily_norm line 51
  10. def OAI.PolynomialVacuumCylinder.SeparatorNormalFamilyBound line 66
  11. theorem OAI.PolynomialVacuumCylinder.normal_family_bound_iff line 72