OAI/Geometry/EinsteinFour/JacobiAverage.lean

GitHub source file

9 declarations, 0 contain sorry, 0 declared as axioms

Trace and curvature bounds for the concrete sine-weighted average.

  1. instance OAI.PositiveEinsteinFour.Jacobi.matrixContinuousENorm line 18

    Also declared: OAI/Geometry/EinsteinFour/AveragedRadial.lean:19 (same declaration text), OAI/Geometry/EinsteinFour/JacobiTraceAverage.lean:13 (same declaration text), OAI/Geometry/EinsteinFour/MatrixGeodesicAverage.lean:20 (same declaration text).

  2. def OAI.PositiveEinsteinFour.Jacobi.entryCLM line 22
  3. theorem OAI.PositiveEinsteinFour.Jacobi.entryCLM_apply line 28
  4. def OAI.PositiveEinsteinFour.Jacobi.quadraticCLM line 31
  5. theorem OAI.PositiveEinsteinFour.Jacobi.quadraticCLM_apply line 34
  6. def OAI.PositiveEinsteinFour.Jacobi.traceCLM line 45
  7. theorem OAI.PositiveEinsteinFour.Jacobi.integral_sine_posSemidef line 48
  8. theorem OAI.PositiveEinsteinFour.Jacobi.sine_average_trace line 76
  9. theorem OAI.PositiveEinsteinFour.Jacobi.sine_average_add_one_posSemidef line 86

    Source documentation

    Averaging preserves the lower normal-curvature bound.

    theorem sine_average_add_one_posSemidef {A : ℝ → NormalMatrix} (hA : Continuous A)
    (hpos : ∀ s, (A s + 1).PosSemidef) :
    ((∫ s in (0 : ℝ)..1, Averages.sineWeight s • A s) + 1).PosSemidef := by
…

    Mentions: OAI.PositiveEinsteinFour.Jacobi.NormalMatrix, OAI.PositiveEinsteinFour.Averages.sineWeight