OAI/NumberTheory/TwoPoint/Bounds/SelfAdjointPath.lean

GitHub source file

8 declarations, 0 contain sorry, 0 declared as axioms

Positivity along an invertible self-adjoint path

The resolvent path in manuscript Lemma q:noncommuting starts at the identity and is self-adjoint and invertible throughout a real interval. Its positivity follows from continuity of the least Rayleigh quotient. The argument is carried out in finite dimension.

  1. def OAI.TwoPointCorrelations.leastRayleigh line 21
  2. lemma OAI.TwoPointCorrelations.rayleigh_bddBelow line 25
  3. lemma OAI.TwoPointCorrelations.leastRayleigh_le line 32
  4. lemma OAI.TwoPointCorrelations.leastRayleigh_le_add_norm line 36
  5. lemma OAI.TwoPointCorrelations.leastRayleigh_lipschitz line 52
  6. lemma OAI.TwoPointCorrelations.leastRayleigh_id line 61
  7. lemma OAI.TwoPointCorrelations.leastRayleigh_ne_zero line 74
  8. theorem OAI.TwoPointCorrelations.selfAdjoint_path_positive line 87

    Source documentation

    A finite-dimensional continuous self-adjoint path that starts at the identity and remains injective has strictly positive quadratic form.

    theorem selfAdjoint_path_positive [FiniteDimensional ℂ E]
    (F : ℝ → E →L[ℂ] E) (a b : ℝ) (hab : a ≤ b)
    (hcont : ContinuousOn F (Set.Icc a b)) (hstart : F a = ContinuousLinearMap.id ℂ E)
    (hself : ∀ t ∈ Set.Icc a b, (F t).IsSymmetric)
    (hinj : ∀ t ∈ Set.Icc a b, Function.Injective (F t)) :
    ∀ x : E, x ≠ 0 → 0 < (inner ℂ (F b x) x).re := by
…