OAI/Geometry/EinsteinFour/Defect.lean

GitHub source file

12 declarations, 0 contain sorry, 0 declared as axioms

Exact scalar certificates controlling the energy defects in equation (19).

  1. def OAI.PositiveEinsteinFour.Defect.A0 line 11
  2. def OAI.PositiveEinsteinFour.Defect.L0 line 12
  3. def OAI.PositiveEinsteinFour.Defect.C0 line 13
  4. def OAI.PositiveEinsteinFour.Defect.discriminantNumerator line 14
  5. theorem OAI.PositiveEinsteinFour.Defect.C0_0 line 18
  6. theorem OAI.PositiveEinsteinFour.Defect.C0_1 line 33
  7. theorem OAI.PositiveEinsteinFour.Defect.disc_0 line 48
  8. theorem OAI.PositiveEinsteinFour.Defect.disc_1 line 66
  9. theorem OAI.PositiveEinsteinFour.Defect.C0_pos line 84
  10. theorem OAI.PositiveEinsteinFour.Defect.disc_pos line 89
  11. theorem OAI.PositiveEinsteinFour.Defect.negative_quadratic line 94
  12. theorem OAI.PositiveEinsteinFour.Defect.energy_defect_derivative_neg line 108

    Source documentation

    The exact upper bound for the derivative with respect to an energy defect is negative on the open spectral interval, for every real energy ratio.

    theorem energy_defect_derivative_neg {v : ℝ} (hv : 0 < v) (hv2 : v < 2) (u : ℝ) :
    A0 v * (1 + u) ^ 2 + L0 v * (1 + u) -
      (17 / 10) * (7 / 5 + (1 + 2 * v / (5 * (2 - v))) * u ^ 2) < 0 := by
…

    Mentions: OAI.PositiveEinsteinFour.Defect.A0, OAI.PositiveEinsteinFour.Defect.L0