InvariantGeodesic.lean`

1 declarations, 0 contain sorry, 0 declared as axioms

Invariance of the geodesic-flow measure supplies the stationarity needed by the mean-square averaging estimate. This is a direct change of variables in the actual field integrals.

theorem OAI.PositiveEinsteinFour.Averages.invariant_geodesic_mean_square_lower line 22

Source documentation

It suffices to bound the derivative energy at time zero: preservation of the field measure transports both energy identities to every time.

theorem invariant_geodesic_mean_square_lower
    (φ : ℝ → Ω ≃ᵐ Ω) (hφ : ∀ r, MeasurePreserving (φ r) μ μ)
    (C H : C(Ω, E)) {F G : ℝ → C(Ω, E)} {t : ℝ}
    (hfield : ∀ r x, F r x = C (φ r x))
    (hgradient : ∀ r x, G r x = H (φ r x))
    (hderiv : ∀ r, HasDerivAt F (G r) r)
    (henergy : (∫ x, ‖H x‖ ^ 2 ∂μ) ≤ (3 / 2) * (∫ x, ‖C x‖ ^ 2 ∂μ)) :
    (∫ x, ‖C x‖ ^ 2 ∂μ) * (1 - (t / Real.pi) ^ 2 / 2) ≤
      ∫ x, ‖∫ u, F (t * u) x ∂sineMeasure‖ ^ 2 ∂μ := by
…

Mentions: OAI.PositiveEinsteinFour.Averages.sineMeasure