OAI/Analysis/LiebThirring/FlowContinuation.lean

GitHub source file

10 declarations, 0 contain sorry, 0 declared as axioms

  1. lemma OAI.SharpLiebThirring.ODEProof.scalar_stationary_unique line 21
  2. lemma OAI.SharpLiebThirring.ODEProof.upper_barrier line 47

    Source documentation

    An upper barrier needs the derivative sign only strictly outside the barrier.

    lemma upper_barrier {l r κ : ℝ} {h h' : ℝ → ℝ}
    (hd : ∀ t ∈ Icc l r, HasDerivWithinAt h (h' t) (Icc l r) t)
    (hi : h l ≤ κ)
    (hs : ∀ t ∈ Icc l r, κ < h t → h' t ≤ 0) :
    ∀ t ∈ Icc l r, h t ≤ κ := by
…
  3. lemma OAI.SharpLiebThirring.ODEProof.two_sided_barrier line 71
  4. lemma OAI.SharpLiebThirring.MatrixFlow.vanishing_row_stationary line 101
  5. lemma OAI.SharpLiebThirring.MatrixFlow.matching_nonzero_rows line 142
  6. lemma OAI.SharpLiebThirring.MatrixFlow.isClosed_lower line 168
  7. lemma OAI.SharpLiebThirring.MatrixFlow.compact_lower_box line 178
  8. lemma OAI.SharpLiebThirring.MatrixFlow.compact_matching_zeros line 190
  9. lemma OAI.SharpLiebThirring.MatrixFlow.terminal_zero_parameter line 204
  10. lemma OAI.SharpLiebThirring.MatrixFlow.terminal_matching line 223