OAI/Geometry/EinsteinFour/WeightedCurve.lean

GitHub source file

2 declarations, 0 contain sorry, 0 declared as axioms

The regularity premise in the radial Riemann sums follows from ordinary bounded curvature and bounded curvature derivative along the frame flow.

  1. theorem OAI.PositiveEinsteinFour.Averages.sineWeight_abs_le_two line 15
  2. theorem OAI.PositiveEinsteinFour.Averages.sineWeighted_rescale_lipschitz line 22

    Source documentation

    A bounded differentiable curve with bounded derivative supplies the global Lipschitz estimate used by the sine-mode discretization.

    theorem sineWeighted_rescale_lipschitz {f f' : ℝ → E} {B D : ℝ}
    (hderiv : ∀ s, HasDerivAt f (f' s) s)
    (hbound : ∀ s, ‖f s‖ ≤ B) (hbound' : ∀ s, ‖f' s‖ ≤ D)
    (t a b : ℝ) :
    ‖sineWeight a • f (t * a) - sineWeight b • f (t * b)‖ ≤
      (2 * Real.pi * B + 2 * D * |t|) * |a - b| := by
…

    Mentions: OAI.PositiveEinsteinFour.Averages.sineWeight