OAI/Analysis/LiebThirring/CoerciveInverse.lean

GitHub source file

5 declarations, 0 contain sorry, 0 declared as axioms

  1. lemma OAI.SharpLiebThirring.OperatorProof.coercive_bijective line 13
  2. lemma OAI.SharpLiebThirring.OperatorProof.selfAdjoint_of_surjective_shift line 59

    Source documentation

    A densely defined symmetric operator whose real translate is onto is self-adjoint.

    lemma selfAdjoint_of_surjective_shift {E : Type u183} [NormedAddCommGroup E]
    [InnerProductSpace ℂ E] [CompleteSpace E] (A : E →ₗ.[ℂ] E)
    (hd : Dense (A.domain : Set E)) (hs : A.IsFormalAdjoint A) (c : ℝ)
    (hr : ∀ f : E, ∃ u : A.domain, A u+(c:ℂ) • (u:E) = f) : IsSelfAdjoint A := by
…
  3. def OAI.SharpLiebThirring.OperatorProof.inverseShift line 94

    Source documentation

    The inverse of an injective bounded symmetric map, translated by a real scalar.

    def inverseShift {E : Type u184} [NormedAddCommGroup E] [InnerProductSpace ℂ E]
    (R : E →L[ℂ] E) (hR : Function.Injective R) (c : ℝ) : E →ₗ.[ℂ] E where
…
  4. lemma OAI.SharpLiebThirring.OperatorProof.inverseShift_apply line 100
  5. lemma OAI.SharpLiebThirring.OperatorProof.inverseShift_selfAdjoint line 107