OAI/Geometry/EinsteinFour/RadialCoefficient.lean

GitHub source file

4 declarations, 0 contain sorry, 0 declared as axioms

Comparison of the piecewise polynomial integration weight with the exact Jacobi determinant-loss coefficient. The variable is u = t / pi.

  1. def OAI.PositiveEinsteinFour.Jacobi.radialLower line 15
  2. theorem OAI.PositiveEinsteinFour.Jacobi.small_parameter_bound line 18
  3. theorem OAI.PositiveEinsteinFour.Jacobi.large_parameter_bound line 45
  4. theorem OAI.PositiveEinsteinFour.Jacobi.radialLower_le_lossFactor line 64

    Source documentation

    The full piecewise lower weight is valid on the preconjugate radial interval. Its jump at 5/8 is intentional and included in the proof.

    theorem radialLower_le_lossFactor {u : ℝ} (hu : 0 ≤ u) (hu1 : u < 1) :
    radialLower u ≤ lossFactor (u ^ 2 / (1 - u ^ 2)) := by
…

    Mentions: OAI.PositiveEinsteinFour.Jacobi.radialLower, OAI.PositiveEinsteinFour.Jacobi.lossFactor