FrameAverages.lean`

4 declarations, 0 contain sorry, 0 declared as axioms

Spherical disintegration of the actual frame-curvature energies.

The explicit published input BrinKarcherAveraging is the specialization of the Riemannian-base times Stiefel probability measure in Brin--Karcher (1984), Section 1, p.275, to functions depending only on the first frame direction. It is a generic integration statement and contains no curvature estimate. The angular curvature identities used below are proved separately.

def OAI.PositiveEinsteinFour.Geometry.DirectionInvariant line 26
structure OAI.PositiveEinsteinFour.Geometry.BrinKarcherAveraging line 30
Source documentation
Generic spherical disintegration, parameterized by the frame measure.
```
structure BrinKarcherAveraging (g : SmoothMetric M) (μ : Measure (FrameBundle g)) : Prop where
…
```
Mentions: OAI.PositiveEinsteinFour.Geometry.FrameBundle
theorem OAI.PositiveEinsteinFour.Geometry.frameCurvatureField_mean_square line 39
Source documentation
Derive the time-zero curvature energy from the published disintegration and the proved frame transformation and angular contraction.
```
theorem frameCurvatureField_mean_square
    (g : SmoothMetric M) {μ : Measure (FrameBundle g)} (hμ : BrinKarcherAveraging g μ)
    (h : FollandMoments) (S : M → ℝ)
    (hCi : Integrable (fun e => ‖frameCurvatureField g e‖ ^ 2) μ)
    (hSi : Integrable S (normalizedVolume g))
    (hInv : DirectionInvariant (fun e => ‖frameCurvatureField g e‖ ^ 2))
    (hdec : ∀ c (e : OrthonormalFrame g c), frameCurvature g c e =
      einsteinCurvatureTensor (plusWeyl g c e) (minusWeyl g c e))
    (htr : ∀ c (e : OrthonormalFrame g c),
      (plusWeyl g c e).trace = 0 ∧ (minusWeyl g c e).trace = 0)
    (hS : ∀ c (e : OrthonormalFrame g c),
      normalizedBlockNorm (plusWeyl g c e) ^ 2 +
…
```
Mentions: OAI.PositiveEinsteinFour.Geometry.FrameBundle, OAI.PositiveEinsteinFour.Geometry.BrinKarcherAveraging, OAI.PositiveEinsteinFour.Geometry.frameCurvatureField, OAI.PositiveEinsteinFour.Geometry.normalizedVolume, OAI.PositiveEinsteinFour.Geometry.DirectionInvariant, OAI.PositiveEinsteinFour.Geometry.OrthonormalFrame, OAI.PositiveEinsteinFour.Geometry.frameCurvature, OAI.PositiveEinsteinFour.Geometry.plusWeyl, OAI.PositiveEinsteinFour.Geometry.minusWeyl, OAI.PositiveEinsteinFour.Geometry.normalizedBlockNorm

theorem OAI.PositiveEinsteinFour.Geometry.frameCurvatureDerivative_mean_square line 63

Source documentation

The same disintegration yields the exact derivative energy. The gradient sum is a base scalar; its independence of orthonormal frame is explicit.

theorem frameCurvatureDerivative_mean_square
    (g : SmoothMetric M) {μ : Measure (FrameBundle g)} (hμ : BrinKarcherAveraging g μ)
    (h : FollandMoments) (E : M → ℝ)
    (hHi : Integrable (fun e => ‖frameCurvatureDerivative g e‖ ^ 2) μ)
    (hEi : Integrable E (normalizedVolume g))
    (hInv : DirectionInvariant (fun e => ‖frameCurvatureDerivative g e‖ ^ 2))
    (hturn : ∀ c (e : OrthonormalFrame g c) q,
      frameCurvatureDerivative g (frameTurn e q) = normalCurvatureDerivative g c e q)
    (hsym : ∀ c (e : OrthonormalFrame g c) a,
      (plusWeylGradient g c e a)ᵀ = plusWeylGradient g c e a)
    (htr : ∀ c (e : OrthonormalFrame g c) a, (plusWeylGradient g c e a).trace = 0)
    (hE : ∀ c (e : OrthonormalFrame g c),
…

Mentions: OAI.PositiveEinsteinFour.Geometry.FrameBundle, OAI.PositiveEinsteinFour.Geometry.BrinKarcherAveraging, OAI.PositiveEinsteinFour.Geometry.frameCurvatureDerivative, OAI.PositiveEinsteinFour.Geometry.normalizedVolume, OAI.PositiveEinsteinFour.Geometry.DirectionInvariant, OAI.PositiveEinsteinFour.Geometry.OrthonormalFrame, OAI.PositiveEinsteinFour.Geometry.frameTurn, OAI.PositiveEinsteinFour.Geometry.normalCurvatureDerivative, OAI.PositiveEinsteinFour.Geometry.plusWeylGradient