OAI/Geometry/EinsteinFour/AngularNormal.lean

GitHub source file

14 declarations, 0 contain sorry, 0 declared as axioms

1. abbrev OAI.PositiveEinsteinFour.Angular.Mat3 line 13
2. def OAI.PositiveEinsteinFour.Angular.squareNorm line 15
3. def OAI.PositiveEinsteinFour.Angular.pairing line 17
4. def OAI.PositiveEinsteinFour.Angular.rotated line 19
5. def OAI.PositiveEinsteinFour.Angular.normalDeviation line 23

   Source documentation

   The curvature deviation in the normal basis I_s q.

   def normalDeviation (T U : Mat3) (q : Directions) : Mat3 :=
   …

   Mentions: OAI.PositiveEinsteinFour.Angular.Mat3, OAI.PositiveEinsteinFour.Angular.Directions

6. theorem OAI.PositiveEinsteinFour.Angular.squareNorm_eq_trace line 26
7. theorem OAI.PositiveEinsteinFour.Angular.squareNorm_conjugate line 32
8. theorem OAI.PositiveEinsteinFour.Angular.squareNorm_rotated line 44
9. theorem OAI.PositiveEinsteinFour.Angular.norm_add_half line 48
10. theorem OAI.PositiveEinsteinFour.Angular.squareNorm_normalDeviation line 56
11. theorem OAI.PositiveEinsteinFour.Angular.pairing_delta_sum line 63
12. theorem OAI.PositiveEinsteinFour.Angular.integral_mixed_pairing line 70
13. theorem OAI.PositiveEinsteinFour.Angular.integral_squareNorm_normalDeviation line 99

    Source documentation

    The first identity in the manuscript's geodesic averages, on each individual unit tangent sphere.

    theorem integral_squareNorm_normalDeviation (h : FollandMoments) (T U : Mat3)
        (hT : T.trace = 0) (hU : U.trace = 0) :
        (∫ q, squareNorm (normalDeviation T U q) ∂sphereMeasure) =
          (squareNorm T + squareNorm U) / 4 := by
    …

    Mentions: OAI.PositiveEinsteinFour.Angular.FollandMoments, OAI.PositiveEinsteinFour.Angular.Mat3, OAI.PositiveEinsteinFour.Angular.squareNorm, OAI.PositiveEinsteinFour.Angular.normalDeviation, OAI.PositiveEinsteinFour.Angular.sphereMeasure

14. theorem OAI.PositiveEinsteinFour.Angular.integral_squareNorm_normalDeviation_normalized line 116