OAI/Geometry/EinsteinFour/GeodesicJacobiIntegralCalculus.lean

GitHub source file

4 declarations, 0 contain sorry, 0 declared as axioms

Differentiating an interval integral twice on a compact parameter strip. Joint continuity supplies the uniform derivative bound, so no domination estimate is added to the geometric hypotheses.

  1. theorem OAI.PositiveEinsteinFour.Geometry.continuousOn_rectangle_slice line 17
  2. theorem OAI.PositiveEinsteinFour.Geometry.intervalIntegral_hasDerivAt_rectangle line 25
  3. theorem OAI.PositiveEinsteinFour.Geometry.intervalIntegral_secondDeriv_rectangle line 60
  4. theorem OAI.PositiveEinsteinFour.Geometry.finite_piece_boundary_cancellation line 83

    Source documentation

    Matching chart boundary values cancel without requiring a global chart.

    theorem finite_piece_boundary_cancellation (n : ℕ) (E I L R : ℕ → ℝ)
    (hE : ∀ i < n, E i = I i + R i - L i)
    (hjoin : ∀ i < n, R i = L (i + 1)) :
    (∑ i ∈ Finset.range n, E i) = (∑ i ∈ Finset.range n, I i) + L n - L 0 := by
…