OAI/Geometry/EinsteinFour/VolumeConstants.lean

GitHub source file

26 declarations, 0 contain sorry, 0 declared as axioms

Exact rational integrations for the two volume margins.

  1. def OAI.PositiveEinsteinFour.VolumeConstants.sineLower line 14
  2. def OAI.PositiveEinsteinFour.VolumeConstants.initialFactor line 18
  3. def OAI.PositiveEinsteinFour.VolumeConstants.upperIntegrand line 20
  4. def OAI.PositiveEinsteinFour.VolumeConstants.upperIntegrandMiddle line 23
  5. def OAI.PositiveEinsteinFour.VolumeConstants.upperIntegrandEnd line 26
  6. def OAI.PositiveEinsteinFour.VolumeConstants.lowerIntegrand line 29
  7. def OAI.PositiveEinsteinFour.VolumeConstants.lowerIntegrandEnd line 32
  8. def OAI.PositiveEinsteinFour.VolumeConstants.polynomial line 35
  9. theorem OAI.PositiveEinsteinFour.VolumeConstants.integral_polynomial line 38
  10. def OAI.PositiveEinsteinFour.VolumeConstants.coefficients0 line 48
  11. theorem OAI.PositiveEinsteinFour.VolumeConstants.expansion0 line 82
  12. theorem OAI.PositiveEinsteinFour.VolumeConstants.row1_lower line 90

    Source documentation

    Row 1 of the manuscript's rational integration table.

    theorem row1_lower : (11869 / 1000000 : ℝ) <
    ∫ u in 0..(1 / 2), upperIntegrand u := by
…

    Mentions: OAI.PositiveEinsteinFour.VolumeConstants.upperIntegrand

  13. def OAI.PositiveEinsteinFour.VolumeConstants.coefficients1 line 96
  14. theorem OAI.PositiveEinsteinFour.VolumeConstants.expansion1 line 130
  15. theorem OAI.PositiveEinsteinFour.VolumeConstants.row2_lower line 138

    Source documentation

    Row 2 of the manuscript's rational integration table.

    theorem row2_lower : (30175 / 1000000 : ℝ) <
    ∫ u in (1 / 2)..(5 / 8), upperIntegrandMiddle u := by
…

    Mentions: OAI.PositiveEinsteinFour.VolumeConstants.upperIntegrandMiddle

  16. def OAI.PositiveEinsteinFour.VolumeConstants.coefficients2 line 144
  17. theorem OAI.PositiveEinsteinFour.VolumeConstants.expansion2 line 170
  18. theorem OAI.PositiveEinsteinFour.VolumeConstants.row3_lower line 178

    Source documentation

    Row 3 of the manuscript's rational integration table.

    theorem row3_lower : (39518 / 1000000 : ℝ) <
    ∫ u in (5 / 8)..1, upperIntegrandEnd u := by
…

    Mentions: OAI.PositiveEinsteinFour.VolumeConstants.upperIntegrandEnd

  19. def OAI.PositiveEinsteinFour.VolumeConstants.coefficients3 line 184
  20. theorem OAI.PositiveEinsteinFour.VolumeConstants.expansion3 line 202
  21. theorem OAI.PositiveEinsteinFour.VolumeConstants.row4_lower line 210

    Source documentation

    Row 4 of the manuscript's rational integration table.

    theorem row4_lower : (698 / 1000000 : ℝ) <
    ∫ u in 0..(1 / 2), lowerIntegrand u := by
…

    Mentions: OAI.PositiveEinsteinFour.VolumeConstants.lowerIntegrand

  22. def OAI.PositiveEinsteinFour.VolumeConstants.coefficients4 line 216
  23. theorem OAI.PositiveEinsteinFour.VolumeConstants.expansion4 line 234
  24. theorem OAI.PositiveEinsteinFour.VolumeConstants.row5_lower line 242

    Source documentation

    Row 5 of the manuscript's rational integration table.

    theorem row5_lower : (40554 / 1000000 : ℝ) <
    ∫ u in (1 / 2)..1, lowerIntegrandEnd u := by
…

    Mentions: OAI.PositiveEinsteinFour.VolumeConstants.lowerIntegrandEnd

  25. theorem OAI.PositiveEinsteinFour.VolumeConstants.upper_margin line 248
  26. theorem OAI.PositiveEinsteinFour.VolumeConstants.lower_margin line 254