OAI/Geometry/EinsteinFour/JacobiPositivity.lean

GitHub source file

3 declarations, 0 contain sorry, 0 declared as axioms

1. theorem OAI.PositiveEinsteinFour.Jacobi.near_identity_ratio_neighborhood line 16

   Source documentation

   A single neighborhood controls every near-initial mesh ratio. The inverse is applied to the position divided by time, which tends to one.

   theorem near_identity_ratio_neighborhood
       {R : Type*} [NormedRing R] [HasSummableGeomSeries R] :
       ∃ δ : ℝ, 0 < δ ∧ ∀ B V : R,
         ‖B - 1‖ < δ → ‖V - 1‖ < δ →
         IsUnit B ∧ ‖V * Ring.inverse B - 1‖ < 1 := by
   …

2. theorem OAI.PositiveEinsteinFour.Jacobi.identity_add_ratio_quadratic_pos line 47

   Source documentation

   A positive multiple of a map within distance one of the identity can be added to the identity without losing strict positivity.

   theorem identity_add_ratio_quadratic_pos
       {F : Type*} [NormedAddCommGroup F] [InnerProductSpace ℝ F]
       {P : F →L[ℝ] F} {r : ℝ} (hr : 0 ≤ r)
       (hP : ‖P - ContinuousLinearMap.id ℝ F‖ < 1)
       {x : F} (hx : x ≠ 0) :
       0 < inner ℝ ((ContinuousLinearMap.id ℝ F + r • P) x) x := by
   …

3. theorem OAI.PositiveEinsteinFour.Jacobi.mesh_ratio_quadratic_pos line 64

   Source documentation

   Split the mesh into a neighborhood of zero and its complement. A uniform coefficient bound suffices on the complement, while closeness to the initial coefficient handles all of the first mesh nodes at once.

   theorem mesh_ratio_quadratic_pos
       {F : Type*} [NormedAddCommGroup F] [InnerProductSpace ℝ F]
       {P : F →L[ℝ] F} {h η K : ℝ} {i : ℕ}
       (hi : 0 < i) (hh : 0 < h) (hmesh : h * K < η)
       (hbound : ‖P‖ ≤ K)
       (hnear : (i : ℝ) * h ≤ η → ‖P - ContinuousLinearMap.id ℝ F‖ < 1)
       {x : F} (hx : x ≠ 0) :
       0 < inner ℝ ((ContinuousLinearMap.id ℝ F + ((1 : ℝ) / i) • P) x) x := by
   …