OAI/Geometry/EinsteinFour/JacobiDensityMeasurability.lean

GitHub source file

11 declarations, 0 contain sorry, 0 declared as axioms

Measurability of the first-conjugate-point truncation. The apparently uncountable condition is a countable intersection of open conditions on compact time intervals. No stability theorem for conjugate points is used.

  1. theorem OAI.PositiveEinsteinFour.Jacobi.isOpen_forall_isUnit line 20
  2. def OAI.PositiveEinsteinFour.Jacobi.preconjugateSet line 35
  3. def OAI.PositiveEinsteinFour.Jacobi.compactPreconjugateSet line 38
  4. theorem OAI.PositiveEinsteinFour.Jacobi.measurableSet_preconjugate line 42
  5. def OAI.PositiveEinsteinFour.Jacobi.truncatedJacobiDensity line 77
  6. theorem OAI.PositiveEinsteinFour.Jacobi.truncatedJacobiDensity_rescale line 80
  7. theorem OAI.PositiveEinsteinFour.Jacobi.measurable_truncatedJacobiDensity line 95
  8. theorem OAI.PositiveEinsteinFour.Jacobi.norm_truncatedJacobiDensity_le line 102
  9. theorem OAI.PositiveEinsteinFour.Jacobi.integrable_truncatedJacobiDensity_slice line 112

    Source documentation

    Each fixed-radius density is integrable on a compact parameter space. Only joint continuity of the actual Jacobi matrix is needed.

    theorem integrable_truncatedJacobiDensity_slice {X : Type*} [TopologicalSpace X]
    [CompactSpace X] [MeasurableSpace X] [BorelSpace X] (μ : Measure X)
    [IsFiniteMeasure μ] (J : ℝ × X → NormalMatrix) (hJ : Continuous J) (t : ℝ) :
    Integrable (fun x => truncatedJacobiDensity J (t, x)) μ := by
…

    Mentions: OAI.PositiveEinsteinFour.Jacobi.NormalMatrix, OAI.PositiveEinsteinFour.Jacobi.truncatedJacobiDensity

  10. theorem OAI.PositiveEinsteinFour.Jacobi.integrable_truncatedJacobiDensity_product line 125
  11. theorem OAI.PositiveEinsteinFour.Jacobi.intervalIntegrable_truncatedJacobiDensity_average line 143

    Source documentation

    The averaged radial density is integrable on every bounded time interval.

    theorem intervalIntegrable_truncatedJacobiDensity_average {X : Type*} [TopologicalSpace X]
    [CompactSpace X] [MeasurableSpace X] [BorelSpace X] (μ : Measure X)
    [IsFiniteMeasure μ] (J : ℝ × X → NormalMatrix) (hJ : Continuous J) (a b : ℝ)
    (hab : a ≤ b) :
    IntervalIntegrable (fun t => ∫ x, truncatedJacobiDensity J (t, x) ∂μ) volume a b := by
…

    Mentions: OAI.PositiveEinsteinFour.Jacobi.NormalMatrix, OAI.PositiveEinsteinFour.Jacobi.truncatedJacobiDensity