OAI/Geometry/EinsteinFour/FrameFlow.lean

GitHub source file

9 declarations, 0 contain sorry, 0 declared as axioms

The frame-flow action on the actual normal-curvature fields. The measure-preserving continuous action is the precise part of Brin--Karcher, Section 1, used here; no ergodicity or curvature-energy bound is assumed.

  1. structure OAI.PositiveEinsteinFour.Geometry.FrameFlow line 23
  2. theorem OAI.PositiveEinsteinFour.Geometry.FrameFlow.continuous_slice line 28
  3. def OAI.PositiveEinsteinFour.Geometry.curvatureCurve line 32
  4. def OAI.PositiveEinsteinFour.Geometry.curvatureDerivativeCurve line 37
  5. theorem OAI.PositiveEinsteinFour.Geometry.curvatureCurve_hasDerivAt line 44

    Source documentation

    The ordinary derivative along each parallel frame implies the derivative of the full continuous field used in the radial averaging theorem.

    theorem curvatureCurve_hasDerivAt {g : SmoothMetric M} {μ : Measure (FrameBundle g)}
    [CompactSpace (FrameBundle g)] (φ : FrameFlow g μ)
    (hC : Continuous (frameCurvatureField g))
    (hH : Continuous (frameCurvatureDerivative g))
    (hpoint : ∀ t e, HasDerivAt
      (fun s => frameCurvatureField g (φ.map s e))
      (frameCurvatureDerivative g (φ.map t e)) t) (t : ℝ) :
    HasDerivAt (curvatureCurve φ hC) (curvatureDerivativeCurve φ hH t) t := by
…

    Mentions: OAI.PositiveEinsteinFour.Geometry.FrameBundle, OAI.PositiveEinsteinFour.Geometry.FrameFlow, OAI.PositiveEinsteinFour.Geometry.frameCurvatureField, OAI.PositiveEinsteinFour.Geometry.frameCurvatureDerivative, OAI.PositiveEinsteinFour.Geometry.curvatureCurve, OAI.PositiveEinsteinFour.Geometry.curvatureDerivativeCurve

  6. theorem OAI.PositiveEinsteinFour.Geometry.curvatureCurve_stationary line 56
  7. theorem OAI.PositiveEinsteinFour.Geometry.curvatureDerivativeCurve_stationary line 62
  8. theorem OAI.PositiveEinsteinFour.Geometry.curvatureCurve_energy line 69
  9. theorem OAI.PositiveEinsteinFour.Geometry.curvatureDerivativeCurve_energy line 76