Averages.lean`

6 declarations, 0 contain sorry, 0 declared as axioms

The Hilbert-space variance estimate for geodesic averages. Applying this to the Jacobi curvature matrix in the Hilbert space of square-integrable fields separates the averaging argument from the geometric flow identities.

theorem OAI.PositiveEinsteinFour.Averages.integrable_sq_distance line 23
theorem OAI.PositiveEinsteinFour.Averages.integral_sq_distance line 31
theorem OAI.PositiveEinsteinFour.Averages.integrable_mean_sq_distance line 44

theorem OAI.PositiveEinsteinFour.Averages.double_variance_identity line 55

Source documentation

The double-variance identity, with only the integrability needed by the application. The two integrals need not be interchanged.

theorem double_variance_identity (hf : Integrable f μ)
    (hf2 : Integrable (fun t => ‖f t‖ ^ 2) μ) :
    (∫ s, ∫ t, ‖f s - f t‖ ^ 2 ∂μ ∂μ) =
      2 * ((∫ t, ‖f t‖ ^ 2 ∂μ) - ‖∫ t, f t ∂μ‖ ^ 2) := by
…

theorem OAI.PositiveEinsteinFour.Averages.stationary_average_lower line 79

Source documentation

A stationary Hilbert-valued curve with a mean-square increment bound retains this much squared norm after averaging. In the geodesic application, L is the averaged squared norm of the directional derivative.

theorem stationary_average_lower {ν : Measure ℝ} [IsProbabilityMeasure ν]
    {A : ℝ → E} {q L : ℝ}
    (hA : Integrable A ν) (hA2 : Integrable (fun t => ‖A t‖ ^ 2) ν)
    (ht : Integrable (fun t : ℝ => t) ν)
    (ht2 : Integrable (fun t : ℝ => t ^ 2) ν)
    (hstationary : ∀ᵐ t ∂ν, ‖A t‖ ^ 2 = q)
    (hincrement : ∀ s t, ‖A s - A t‖ ^ 2 ≤ L * (s - t) ^ 2) :
    q - L * ((∫ t, t ^ 2 ∂ν) - (∫ t, t ∂ν) ^ 2) ≤ ‖∫ t, A t ∂ν‖ ^ 2 := by
…

theorem OAI.PositiveEinsteinFour.Averages.increment_bound_of_derivative line 111
Source documentation
An invariant averaged derivative bound controls increments of the Hilbert-valued curvature curve. This is also valid for an L² Hilbert space.
```
theorem increment_bound_of_derivative {A d : ℝ → E} {L : ℝ} (hL : 0 ≤ L)
    (hd : ∀ t, HasDerivAt A (d t) t) (hbound : ∀ t, ‖d t‖ ^ 2 ≤ L) (s t : ℝ) :
    ‖A s - A t‖ ^ 2 ≤ L * (s - t) ^ 2 := by
…
```