OAI/Geometry/EinsteinFour/SineAverage.lean

GitHub source file

17 declarations, 0 contain sorry, 0 declared as axioms

The exact sine-squared probability weight in the first Dirichlet mode, its first two moments, and the resulting geodesic averaging coefficient.

  1. def OAI.PositiveEinsteinFour.Averages.sineWeight line 17
  2. theorem OAI.PositiveEinsteinFour.Averages.sineWeight_eq line 19
  3. theorem OAI.PositiveEinsteinFour.Averages.sineWeight_nonneg line 24
  4. theorem OAI.PositiveEinsteinFour.Averages.continuous_sineWeight line 28
  5. theorem OAI.PositiveEinsteinFour.Averages.integral_sineWeight line 32
  6. theorem OAI.PositiveEinsteinFour.Averages.integral_sineWeight_first line 42
  7. theorem OAI.PositiveEinsteinFour.Averages.integral_sineWeight_second line 57
  8. def OAI.PositiveEinsteinFour.Averages.sineMeasure line 79

    Source documentation

    The actual probability measure on the unit time interval, not a moment axiomatization of that measure.

    def sineMeasure : Measure ℝ :=
…
  9. theorem OAI.PositiveEinsteinFour.Averages.integral_sineMeasure line 82
  10. instance OAI.PositiveEinsteinFour.Averages.(instance at line 91) line 91
  11. theorem OAI.PositiveEinsteinFour.Averages.integrable_sineMeasure line 96
  12. theorem OAI.PositiveEinsteinFour.Averages.sineMeasure_first line 106
  13. theorem OAI.PositiveEinsteinFour.Averages.sineMeasure_second line 109
  14. theorem OAI.PositiveEinsteinFour.Averages.sineMeasure_variance line 113
  15. theorem OAI.PositiveEinsteinFour.Averages.sine_average_coefficient line 118
  16. theorem OAI.PositiveEinsteinFour.Averages.sine_average_lower line 132

    Source documentation

    The averaged squared norm retained by the first sine mode. For the curvature application the increment hypothesis comes from the invariant geodesic-flow measure and the integrated Weyl differential identity.

    theorem sine_average_lower {E : Type*} [NormedAddCommGroup E]
    [InnerProductSpace ℝ E] [CompleteSpace E]
    {A : ℝ → E} {q u : ℝ} (hq : 0 ≤ q)
    (hA : Integrable A sineMeasure)
    (hA2 : Integrable (fun t => ‖A t‖ ^ 2) sineMeasure)
    (hstationary : ∀ᵐ t ∂sineMeasure, ‖A t‖ ^ 2 = q)
    (hincrement : ∀ s t, ‖A s - A t‖ ^ 2 ≤
      ((3 / 2) * q * (Real.pi * u) ^ 2) * (s - t) ^ 2) :
    q * (1 - u ^ 2 / 2) ≤ ‖∫ t, A t ∂sineMeasure‖ ^ 2 := by
…

    Mentions: OAI.PositiveEinsteinFour.Averages.sineMeasure

  17. theorem OAI.PositiveEinsteinFour.Averages.sine_average_lower_of_derivative line 150

    Source documentation

    The differentiable-curve version supplies both integrability and the increment estimate. Its derivative hypothesis has exactly the geodesic curvature normalization after time is rescaled to the unit interval.

    theorem sine_average_lower_of_derivative {E : Type*} [NormedAddCommGroup E]
    [InnerProductSpace ℝ E] [CompleteSpace E]
    {A d : ℝ → E} {q u : ℝ} (hq : 0 ≤ q)
    (hd : ∀ t, HasDerivAt A (d t) t)
    (hstationary : ∀ᵐ t ∂sineMeasure, ‖A t‖ ^ 2 = q)
    (hbound : ∀ t, ‖d t‖ ^ 2 ≤ (3 / 2) * q * (Real.pi * u) ^ 2) :
    q * (1 - u ^ 2 / 2) ≤ ‖∫ t, A t ∂sineMeasure‖ ^ 2 := by
…

    Mentions: OAI.PositiveEinsteinFour.Averages.sineMeasure