OAI/Geometry/EinsteinFour/ModeAverageLimit.lean

GitHub source file

7 declarations, 0 contain sorry, 0 declared as axioms

Convergence of the normalized scalar-mode curvature average.

  1. def OAI.PositiveEinsteinFour.Jacobi.interiorMean line 17
  2. theorem OAI.PositiveEinsteinFour.Jacobi.interiorMean_tendsto line 20
  3. theorem OAI.PositiveEinsteinFour.Jacobi.sineWeight_at_node line 38
  4. def OAI.PositiveEinsteinFour.Jacobi.modeAverage line 47
  5. theorem OAI.PositiveEinsteinFour.Jacobi.modeAverage_eq_ratio line 51
  6. theorem OAI.PositiveEinsteinFour.Jacobi.sineWeight_lipschitz line 79
  7. theorem OAI.PositiveEinsteinFour.Jacobi.modeAverage_tendsto line 93

    Source documentation

    The normalized discrete sine mode converges to the actual sine-weighted integral. Only regularity of the weighted curvature curve is used.

    theorem modeAverage_tendsto {A : ℝ → E} {L : ℝ}
    (hL : 0 ≤ L) (hc : Continuous (fun s => Averages.sineWeight s • A s))
    (hLip : ∀ s r, ‖Averages.sineWeight s • A s - Averages.sineWeight r • A r‖ ≤
      L * |s - r|) :
    Tendsto (modeAverage A) atTop
      (nhds (∫ s in (0 : ℝ)..1, Averages.sineWeight s • A s)) := by
…

    Mentions: OAI.PositiveEinsteinFour.Averages.sineWeight, OAI.PositiveEinsteinFour.Jacobi.modeAverage