OAI/Geometry/EinsteinFour/AngularGradient.lean

GitHub source file

8 declarations, 0 contain sorry, 0 declared as axioms

The directional-derivative part of the angular average.

  1. abbrev OAI.PositiveEinsteinFour.Angular.Gradient line 13
  2. def OAI.PositiveEinsteinFour.Angular.directional line 15
  3. def OAI.PositiveEinsteinFour.Angular.gradientSquareNorm line 18
  4. theorem OAI.PositiveEinsteinFour.Angular.integral_directional_entries line 20
  5. theorem OAI.PositiveEinsteinFour.Angular.integral_directional_squareNorm line 43
  6. theorem OAI.PositiveEinsteinFour.Angular.continuous_directional line 49
  7. def OAI.PositiveEinsteinFour.Angular.normalDerivative line 53
  8. theorem OAI.PositiveEinsteinFour.Angular.integral_normalDerivative_squareNorm line 58

    Source documentation

    The two individual terms are exact directional averages; the mixed term is retained explicitly.

    theorem integral_normalDerivative_squareNorm (h : FollandMoments) (Z W : Gradient) :
    (∫ q, squareNorm (normalDerivative Z W q) ∂sphereMeasure) =
      (gradientSquareNorm Z + gradientSquareNorm W) / 16 +
        (∫ q, pairing (directional Z q) (rotated (directional W q) q)
          ∂sphereMeasure) / 2 := by
…

    Mentions: OAI.PositiveEinsteinFour.Angular.FollandMoments, OAI.PositiveEinsteinFour.Angular.Gradient, OAI.PositiveEinsteinFour.Angular.squareNorm, OAI.PositiveEinsteinFour.Angular.normalDerivative, OAI.PositiveEinsteinFour.Angular.sphereMeasure, OAI.PositiveEinsteinFour.Angular.gradientSquareNorm, OAI.PositiveEinsteinFour.Angular.pairing, OAI.PositiveEinsteinFour.Angular.directional, OAI.PositiveEinsteinFour.Angular.rotated