GeodesicAverage.lean`

3 declarations, 0 contain sorry, 0 declared as axioms

The first-mode averaging estimate in the actual space of square-integrable fields. Stationarity is an integral over the space of initial geodesics; no pointwise constancy along a geodesic is assumed.

theorem OAI.PositiveEinsteinFour.Averages.continuous_toL2_norm_sq line 25
Source documentation
The Hilbert norm used for geodesic averaging is exactly the mean square of the continuous field, with respect to the chosen finite measure.
```
theorem continuous_toL2_norm_sq (f : C(Ω, E)) :
    ‖ContinuousMap.toLp 2 μ ℝ f‖ ^ 2 = ∫ x, ‖f x‖ ^ 2 ∂μ := by
…
```
theorem OAI.PositiveEinsteinFour.Averages.continuous_toL2_average_norm_sq line 38
Source documentation
Averaging a field first in time and then in space gives the same squared norm as the Bochner average in the actual L² space.
```
theorem continuous_toL2_average_norm_sq {F : ℝ → C(Ω, E)}
    (hF : Integrable F sineMeasure) :
    ‖∫ u, ContinuousMap.toLp 2 μ ℝ (F u) ∂sineMeasure‖ ^ 2 =
      ∫ x, ‖∫ u, F u x ∂sineMeasure‖ ^ 2 ∂μ := by
…
```
Mentions: OAI.PositiveEinsteinFour.Averages.sineMeasure
theorem OAI.PositiveEinsteinFour.Averages.geodesic_mean_square_lower line 53
Source documentation
The geodesic first-mode bound, obtained from stationarity of mean-square curvature and its mean-square derivative bound. The hypotheses are ordinary field identities and derivatives; the conclusion is the iterated integral needed in the radial determinant comparison.
```
theorem geodesic_mean_square_lower {F G : ℝ → C(Ω, E)} {q t : ℝ}
    (hq : 0 ≤ q)
    (hderiv : ∀ r, HasDerivAt F (G r) r)
    (hstationary : ∀ r, (∫ x, ‖F r x‖ ^ 2 ∂μ) = q)
    (henergy : ∀ r, (∫ x, ‖G r x‖ ^ 2 ∂μ) ≤ (3 / 2) * q) :
    q * (1 - (t / Real.pi) ^ 2 / 2) ≤
      ∫ x, ‖∫ u, F (t * u) x ∂sineMeasure‖ ^ 2 ∂μ := by
…
```
Mentions: OAI.PositiveEinsteinFour.Averages.sineMeasure