OAI/Geometry/EinsteinFour/JacobiRiemann.lean

GitHub source file

3 declarations, 0 contain sorry, 0 declared as axioms

Quantitative Riemann sums for the smooth matrix curves in the radial comparison.

  1. theorem OAI.PositiveEinsteinFour.Jacobi.uniform_mesh_remainder line 16
  2. theorem OAI.PositiveEinsteinFour.Jacobi.uniform_mesh_tendsto_antiderivative line 44
  3. theorem OAI.PositiveEinsteinFour.Jacobi.uniform_mesh_tendsto_integral line 63

    Source documentation

    The left mesh sums converge to the actual interval integral.

    theorem uniform_mesh_tendsto_integral {f : ℝ → E} {t L : ℝ}
    (ht : 0 ≤ t) (hL : 0 ≤ L) (hc : Continuous f)
    (hf : ∀ s r, ‖f s - f r‖ ≤ L * |s - r|) :
    Tendsto (fun N : ℕ => (t / N) • (∑ i ∈ Finset.range N, f (i * (t / N))))
      atTop (nhds (∫ s in (0 : ℝ)..t, f s)) := by
…