OAI/Geometry/EinsteinFour/ScalarDirichlet.lean

GitHub source file

19 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.PositiveEinsteinFour.Jacobi.scalarDirichlet line 14
2. theorem OAI.PositiveEinsteinFour.Jacobi.scalarDirichlet_isHermitian line 18
3. theorem OAI.PositiveEinsteinFour.Jacobi.predecessor_sum line 24
4. theorem OAI.PositiveEinsteinFour.Jacobi.successor_sum line 42
5. theorem OAI.PositiveEinsteinFour.Jacobi.scalarDirichlet_apply_sequence line 59
6. theorem OAI.PositiveEinsteinFour.Jacobi.scalarDirichlet_sine_eigenvector line 68
7. theorem OAI.PositiveEinsteinFour.Jacobi.weighted_row_sum line 84
8. theorem OAI.PositiveEinsteinFour.Jacobi.scalar_ground_state_identity line 104

   Source documentation

   The scalar ground-state identity. It keeps the off-diagonal entries explicit, so its sign applies directly to the tridiagonal reference.

   theorem scalar_ground_state_identity {I : Type*} [Fintype I]
       (L : Matrix I I ℝ) (w y : I → ℝ) (lam : ℝ)
       (hsymm : L.IsHermitian) (heigen : L *ᵥ w = lam • w) :
       (∑ i, ∑ j, (-L i j * w i * w j) * (y i - y j) ^ 2) =
         2 * ((fun i => w i * y i) ⬝ᵥ (L *ᵥ fun i => w i * y i) -
           lam * ∑ i, w i ^ 2 * y i ^ 2) := by
   …

9. theorem OAI.PositiveEinsteinFour.Jacobi.scalar_posDef_of_positive_mode line 144

   Source documentation

   A positive first eigenvector with positive eigenvalue proves positivity of a symmetric scalar matrix with nonpositive off-diagonal entries.

   theorem scalar_posDef_of_positive_mode {I : Type*} [Fintype I] [DecidableEq I]
       (L : Matrix I I ℝ) (w : I → ℝ) (lam : ℝ)
       (hsymm : L.IsHermitian) (hoff : ∀ i j, i ≠ j → L i j ≤ 0)
       (hw : ∀ i, 0 < w i) (hlam : 0 < lam) (heigen : L *ᵥ w = lam • w) :
       L.PosDef := by
   …

10. def OAI.PositiveEinsteinFour.Jacobi.firstSineAngle line 180
11. def OAI.PositiveEinsteinFour.Jacobi.firstSineVector line 182
12. theorem OAI.PositiveEinsteinFour.Jacobi.firstSineVector_pos line 184
13. theorem OAI.PositiveEinsteinFour.Jacobi.firstSineVector_eigenvector line 193
14. theorem OAI.PositiveEinsteinFour.Jacobi.scalarDirichlet_posDef line 205

    Source documentation

    Positivity of the scalar reference follows from its first sine mode; no diagonalization of the other sine modes is needed.

    theorem scalarDirichlet_posDef (N : ℕ) (d : ℝ)
        (hfirst : 0 < d - 2 * Real.cos (firstSineAngle N)) :
        (scalarDirichlet N d).PosDef := by
    …

    Mentions: OAI.PositiveEinsteinFour.Jacobi.firstSineAngle, OAI.PositiveEinsteinFour.Jacobi.scalarDirichlet

15. def OAI.PositiveEinsteinFour.Jacobi.firstSineNormSq line 215
16. theorem OAI.PositiveEinsteinFour.Jacobi.firstSineNormSq_pos line 217
17. def OAI.PositiveEinsteinFour.Jacobi.unitFirstSineVector line 221
18. theorem OAI.PositiveEinsteinFour.Jacobi.unitFirstSineVector_norm line 224
19. theorem OAI.PositiveEinsteinFour.Jacobi.unitFirstSineVector_eigenvector line 233